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* :

In the traces model, we say that *P* is a refinement of *Q* (written
( if , and from this
definition it follows that

We use this message-oriented approach in defining authentication: a
set of messages 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

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

authenticates

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**

This follows from the fact that the process is
unable to perform any events from the set *R* . Thus to prove that

it is sufficient to prove that . 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 . 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 only when some event from *T* occurs
before some event from *R* .

Rule `auth.stop` is therefore sound because 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 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 whenever it is guaranteed for *P* .

Rule `auth.choice` states that if each branch of a choice
guarantees the authentication property , 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 ,and it is involved in all occurrences of events from *T* and *R* , then
that is enough to ensure that the entire parallel combination 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 , 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 is
preserved by recursive calls--if each variable then so does each function applied to the variables--then the processes defined by the mutual
recursion satisfy the property .