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