Introduction

In this paper we consider the nature of machine proofs used in the CSP approach to 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 the CSP method, authentication is considered to be message-oriented: $m2~~{\mathrel{\mathsf{authenticates}}}~~ m1$ if the receipt of m2 guarantees the previous transmission of m1 , even in a hostile environment. To facilitate proofs, a notion of a rank function is developed in [Sch96]. This is an integer-valued function on the message space, such that all messages apart from m1 which could possibly circulate in the network have a rank greater than zero, and the message which provides authentication (m2 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 m1 is blocked.

However, proving authentication is still an arduous task. The principal problem is in 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 [DS97a] 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.