Motivations and Background

In secure distributed systems it is essential that principals (persons, hosts, computers, etc.) could prove their identities to each other. The mechanism of proving the identity over networked systems is called authentication. Typically, cryptographic protocols are used to ensure authentication and related purposes. A cryptographic protocol is a precisely defined sequence of communication and computation steps that use cryptographic mechanisms such as message encryption and decryption. We assume that the reader is familiar with cryptography basics and the associated concepts.

It is well known that the design of authentication cryptographic protocols is error prone. Several protocols have been shown flawed in computer security literature. Consequently, a surge of interest has been expressed in the development of formal methods and tools for the specification, design and analysis of cryptographic protocols. A complete bibliography and a comparative study of these methods can be found in [13,31,30,36,39,24,43,44,14]. These methods can be classified as follows: logical methods, general purpose formal methods and process algebra methods.

Typically, logical methods rest on the use of modal (epistemic, temporal and/or doxatic) logics. The logic is used to specify the protocol (idealization) as well as the security properties. In 1989, Burrows, Abadi and Needham devised BAN, a modal logic of belief for the specification and verification of cryptographic protocols [11,12]. BAN is the most known and famous logic dedicated to cryptographic protocols. Since then, plenty of derived logics have been advanced [1,20,15,29,19]. In 1990, Bieber [5] developed CKT5, a modal logic of knowledge which has been revised and extended by Carlsen in [13] and Snekkenes in [42]. Concurrently, many other logics attempted to combine several aspects of modal logic such as belief, knowledge and trust [18,35,37,45]. These methods have been successfully used to detect many flaws in cryptographic protocols and they are very expressive while specifying security properties. Nevertheless, they are not very suitable to specify the protocols themselves. In fact, the protocols are often translated into a set of logical formulas. The translation process, often referred to as idealization, is error prone since it aims to translate an operational description into a logical one. Furthermore, the idealization is not systematic. Moreover, most of the proposed logics while proved sound with respect to some semantics are generally incomplete. In addition, the verification of the protocol is always manual and semi-formal.

Another trend in formal cryptographic development consists in the accommodation of some well known general purpose formal methods. Representative specification languages that have been used in such accommodations are LOTOS [48,49,47,10], B, VDM [7,46,6], HOL [42], Ina Jo [22,23], Z [9,41] and Coq [8]. Although these formal methods are now firmly established and known to be of great use in specification and verification, it remains that these methods are not dedicated to cryptographic protocols. In addition, these methods need much of expert assistance during the verification process. Actually, they rely on manual or interactive theorem proving techniques.

Lately, the use of process algebra for cryptographic protocol specification and verification has been explored. In 1995, Gavin Lowe [25,28,27,26] was the first to use CSP [21] and model-checking techniques for cryptographic protocol analysis. The protocol is specified as a set of communicating sequential processes that are running in parallel and interacting with their surroundings. The verification is performed by extracting a model (usually a finite state transition system) from the specification and checking that model against a logical specification (a formula over a modal temporal logic) or a behavioral specification (a process term). A similar approach was developed by Bill Roscoe, Paul Gardiner, Dave Jackson and Janson Hulance in [38,16,17] and Steve Schneider in [40]. Recently, Abadi and Gordon [2,3] advanced Spi, a calculus for cryptographic protocols. Spi is built on top of the $\pi$-calculus [32,33,34], a mobile process algebra. It has been devised for the description and analysis of security protocols. The process algebra-based methods have been successfully used in the detection of several flaws in well known cryptographic protocols. The approach seems to be very promising and useful. However, it is well known that the underlying verification techniques, mainly those based on model-checking are problematic in the presence of processes that exhibit infinite behaviors. Accordingly, the infinite aspects of cryptographic protocols are usually not supported in the verification process. Notice also that the specification of security properties in terms of process agents or modal formulae is neither straightforward nor systematic (except in the case of Spi).

In this paper, we present a new formal approach for the analysis of authentication cryptographic protocols. This approach is fully automatic, formal and does not necessitate any specification of any protocol property or invariant. The analysis of a given cryptographic protocol is structured in three main steps:

• First, starting from a classical protocol description, we extract what we call protocol roles. Actually, a role is a protocol abstraction where the emphasis is put on only one principal. Such an abstraction allows us to point out, for each principal, his interpretation of the exchanged protocol messages.
• Second, the intruder abilities are automatically extracted. Apart from the well known abilities such as the complete control of the network, encryption and decryption, we consider all the computational abilities provided by the protocol itself. Generally, the intruder can initiate one or more sessions of the protocol so as to get or reconstruct a particular information to be used into an attack. In our approach, such computation abilities are captured as a finite proof system in which the inference is based on rewriting modulo syntactic unification.
• Third, the roles together with the proof system are combined to perform the protocol verification. The latter consists in checking whether one can instrument a particular role by answering all the challenges uttered by this role. The answers are merely theorems established in the deductive proof system.

The main contributions of this work are:

• A new approach for the analysis of cryptographic protocols. This approach is formal, fully automatic and does not necessitate any specification of any protocol property or invariant. It takes as a parameter the protocol specification and generates the set of flaws, if any, as well as the corresponding attack scenarios.
• An illustration of the usefulness and efficiency of our approach, on the analysis of the Woo and Lam authentication protocol. Abadi and Needham have shown that the protocol is insecure and they proposed a new corrected version. In this paper, we discover new unknown flaws in the Woo and Lam protocol and in the corrected version of Abadi and Needham.

We consider here a subclass of authentication cryptographic protocols. The approach deals with protocols that use symmetric-key cryptography, at most one server and where the only exchanged messages are constructed over nonces, principal identities and symmetric-keys. Moreover, we assume that principals recognize the use of their keys.

The rest of this paper is structured as follows: In Section 2 we recall briefly some basic notions of cryptographic protocols. Section 3 is devoted to an informal presentation of the verification algorithm. In Section 4, we present the formal description of the algorithm and we show how the proof system is generated. In Section 5, we illustrate our approach on the analysis of the corrected version of the Woo and Lam authentication protocol. A few concluding remarks and a discussion of further research are ultimately sketched as a conclusion in Section 6.