Authentication

In the CSP traces model, properties are given as predicates on traces, and a process P satisfies a specification S if all of its traces satisfy S :

$$P \mbox{ \bf sat }S \iff \forall tr \in traces(P).S$$

In the traces model, we say that P is a refinement of Q (written ($Q \sqsubseteq P)$ if $traces(Q) \subseteq traces(P)$, and from this definition it follows that

$$P \sqsubseteq Q \land P \mbox{ \bf sat }S \Rightarrow Q \mbox{ \bf sat }S$$

We use this message-oriented approach in defining authentication: a set of messages $T~~{\mathrel{\mathsf{authenticates}}}~~$ a set of messages R if the receipt of a message in set T guarantees the previous transmission of a message in set R . As a predicate on traces, this is defined

$T \mathrel{\mathsf{authenticates}}R ~~~=~~~ tr$ $\mbox{$\mid$\hspace{-.037in}\small\`{}}$ $R = \langle \rangle\Rightarrow tr$ $\mbox{$\mid$\hspace{-.037in}\small\`{}}$ $T = \langle \rangle$

If it is not possible for a trace tr to contain a message from the set T without also containing a message from the set R , then we can be sure that a message from set R was transmitted onto the network before T could be received.

In this paper, the property we choose to prove is that the message

$$rec(b, i, crypto(longterm(lt(b)), conc3(S, Ia, Nb)))$$

authenticates

$$\{ trans(s, j, x.crypto(longterm(lt(b)), conc3(S, Ia, Nb)).y) \}$$

where S is an arbitrary session key. That is, if agent B receives, from anywhere, a message encrypted with his long-term key, and containing a session key S , a neighbour's identity and his original nonce challenge, he can be sure that that message originated from the server.

The following lemma is an immediate consequence of the definition.

Lemma 1

 $P \mbox{ \bf sat }T \mathrel{\mathsf{authenticates}}R \iff P \parallel[R] \mbox{ \em Stop }\mbox{ \bf sat }tr$ $\mbox{$\mid$\hspace{-.037in}\small\`{}}$ $T = \langle \rangle$

This follows from the fact that the process $P \parallel[R] \mbox{ \em Stop }$ is unable to perform any events from the set R . Thus to prove that

$$P \mbox{ \bf sat }T \mathrel{\mathsf{authenticates}}R$$

it is sufficient to prove that $P \parallel[R] \mbox{ \em Stop }\mbox{ \bf sat }tr$ $\mbox{$\mid$\hspace{-.037in}\small\`{}}$$T = \langle \rangle$. This is the approach we will use in paper.

The CSP traces model has a sound and complete set of rules for proving that processes satisfy specifications, which could be used here, but we prefer to develop a set of rules specific to our application, which will enable us to reason at a more appropriate level of abstraction. Those used in this paper are given in Figure 2.

   Figure 2: Proof rules for authentication

The soundness of the rules follows from the trace semantics of the operators, and the formal definition of $T \mathrel{\mathsf{authenticates}}R$. They have been proven in PVS [DS97a]. We may give informal justification of their soundness by considering that occurrence of an event from T is intended to provide evidence that some event from R previously occurred. Hence a process fails to satisfy $T \mathrel{\mathsf{authenticates}}R$ only when some event from T occurs before some event from R .

Rule auth.stop is therefore sound because $\mbox{ \em Stop }$ cannot perform any events at all, and so cannot perform some T before some R .

Rule auth.prefix.1 is sound because if the very first event a performed by $a \rightarrow P$ is an event from R , then it is not possible for an event from T to occur before an event from R . This is independent of the nature of the subsequent process P , which therefore has no restrictions placed on it by the rule--the rule is applicable for any process P .

Rule auth.prefix.2 is most useful when the event a is not in R , since otherwise auth.prefix.1 is applicable. In this case it states that if the first event is not in T , then occurrence of a is irrelevant to authentication of R by T , and such authentication is guaranteed for $a \rightarrow P$ whenever it is guaranteed for P .

Rule auth.choice states that if each branch of a choice guarantees the authentication property $T \mathrel{\mathsf{authenticates}}R$, then so does the entire choice--since whenever some event from T occurs, it must have been performed by one of the arms of the choice, and that choice must previously have performed some event from R .

Rule auth.parallel states that if a single component P of a parallel combination is able to guarantee that $T \mathrel{\mathsf{authenticates}}R$,and it is involved in all occurrences of events from T and R , then that is enough to ensure that the entire parallel combination $P \parallel[A] Q$ guarantees it: since P will not allow any event from T to occur before an event from R occurs. There are no restrictions on the rest of the system Q , so the rule holds for any process description Q .

Rule auth.interleaves states that if both components of an interleaved combination can guarantee $T \mathrel{\mathsf{authenticates}}R$, then the combination itself can. This follows from the fact that if some event from T occurs, then it must have been performed by one of the component processes, which must have previously performed an event from R .

Finally, the rule auth.recursion for mutually recursive processes states that if the property $T \mathrel{\mathsf{authenticates}}R$ is preserved by recursive calls--if each variable $X_k \mbox{ \bf sat }T \mathrel{\mathsf{authenticates}}R$ then so does each function $F_k(\underline{X})$applied to the variables--then the processes defined by the mutual recursion satisfy the property $T \mathrel{\mathsf{authenticates}}R$.