CSP, PVS and a Recursive Authentication Protocol

Jeremy Bryans and Steve Schneider

Department of Computer Science

Royal Holloway and Bedford New College

Egham, Surrey, TW20 0EX

In this paper we consider the nature of proofs used in the verification of authentication protocols.In [Sch96], a general method is presented for the analysis and verification of authentication protocols using the process algebra CSP [Hoa85]. The CSP syntax provides a natural and precise way to describe such protocols in terms of the messages accepted and transmitted by the individual protocol participants. The CSP traces model provides a formal framework for reasoning about these protocols.

In this method, authentication is considered to be
*message-oriented*: *m1* **authenticates** *m2* if
the receipt of *m1* guarantees the previous transmission of
*m2*, even in a hostile environment. To facilitate proofs, a
notion of a * rank
function* is developed in [Sch96]. This is a function
from the message space to the integers, such that all messages which
could possibly circulate in the network have a rank greater than zero,
and the message which provides authentication (*m1* above) has a
rank of zero or below. It is then sufficient to prove that no
messages of rank zero or below are able to circulate when message
*m2* is blocked.

However, proving authentication is still an arduous task. The principal problem is the complexity of the message space, which gives rise to a mass of detail in proofs, requiring a significant amount of detailed housekeeping. For this reason, the CSP traces theory has been embedded within PVS [DS97a, SOR93], and this description has been successfully used to mechanise several proofs of authentication properties [DS97b, BS97]. However, even with mechanical support the construction of proofs is far from easy, because of the inherent complexity involved in modelling all the possibilities of malicious action.

In this paper, we consider a novel authentication protocol, proposed in [BO97]. The protocol can be used in various ways: we take the purpose to be that of establishing an uncompromised chain of session keys between adjacent pairs of agents involved in the protocol run.

This protocol provides an interesting extension to the work cited above, because very few aspects of an individual protocol run are fixed in advance. There may be an arbitrary number of agents, and consequently there may be an arbitrary number of messages, which may grow to arbitrary lengths.

Despite the extra complexity of the protocol, adapting the techniques developed in [DS97] to prove that the session keys are uncompromised turned out to be relatively straightforward, and the proofs of authentication were not significantly more complex. We present the rank function used, and show how PVS uses the rank function to prove the authentication property.

In [RS97], an attack is described on an implementation of this protocol and a correction is proposed. We go on to identify where the particular implementation decisions made compromised the protocol, and how the proof of authentication for the original definition of the protocol fails when applied to the faulty implementation. We also provide an analysis of the corrected protocol, and verify that the attack is no longer possible. Finally, we speculate on how failed proofs may lead us to discover attacks.

- [BO97]
J.Bull and D.J. Otway.
*The Authentication Protocol.*Technical Report DRA/CIS3/PROJ/CORBA/SC/1/CSM/436-04/03, DRA, Feb 1997. - [BS97]
J.W. Bryans and S.A. Schneider.
*Mechanical Verification of the full Needham-Schroeder Public-Key Protocol.*Technical Report CSD-TR-97-11, Royal Holloway, University of London, April 1997. - [DS97a]
B.Dutertre and S.A. Schneider.
*Embedding CSP in PVS. An application to Authentication Protocols.*Technical Report CSD-TR-97-12, Royal Holloway, University of London, April 1997. - [DS97b]
B.Dutertre and S.A. Schneider.
*Using a PVS Embedding of CSP to verify Authentication Protocols.*In*Proceedings of TPHOLS*, 1997. To appear. - [Hoa85]
C.A.R. Hoare.
*Communicating Sequential Processes*. Prentice-Hall, 1985. - [RS97]
P.Y.A. Ryan and S.A. Schneider.
*An Attack on a Recursive Authentication Protocol: A cautionary tale.*DRA report, May 1997. -
[Sch96]
S.A. Schneider.
*Using CSP for protocol analysis: the Needham-Schroeder Public-Key Protocol.*Technical Report CSD-TR-96-14, Royal Holloway, University of London, October 1996. - [SOR93]
N.Shankar, S.Owre, and J.M. Rushby.
*The PVS Proof Checker: A Reference Manual (Draft).*Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993.