Basics

As defined in [50,51], a protocol is a precisely defined sequence of communication and computation steps. A communication step transfers messages from one principal (sender) to another (receiver), while a computation step updates a principal's internal state. A protocol with a security objective is called a cryptographic protocol. Cryptographic functions are used to achieve such an objective. Authentication protocols are a special kind of cryptographic protocols where the primary aim is to allow principals to identify themselves to each other.

In the sequel, the statement $A\longrightarrow B:M$ will be used to denote the transmission of a message M from the principal A to the principal B . A message is composed of one or several primitive words. A message encrypted with key k is written $\{M\}_k$ and forms a word by itself. Concatenated messages are separated by commas. Message contents (words) follow naming conventions: Encryption keys and nonces are respectively written k and N . Principals are written A , B , S and I , where A and B stand for principals, S for a server and I for a potential intruder. Subscripts will be used to denote principal association, thus for example $N_a$ is a nonce that belongs to A and $k_{as}$ is a shared key between A and S .

In the sequel, we recall the one-way Woo and Lam authentication protocol as presented in [50,51]. This protocol relies on symmetric-key cryptography. The protocol runs as follows when the principal A wants to prove his identity to the principal B :

  Table 1:   The Woo and Lam Authentication Protocol

Here $N_b$ is a nonce, a random number generated by B specially for this protocol run, S is a server and $k_{as}$ and $k_{bs}$ are keys that A and B initially share with S . The description of the protocol can be read as follows: (1) A initiates the protocol and claims his identity to B ; (2) B replies by sending the nonce $N_b$ and asking A to encrypt it under $k_{as}$ in order to prove what he claimed; (3) A returns the nonce $N_b$ encrypted under $k_{as}$; (4) B forwards the response encrypted, together with A 's identity, under $k_{bs}$ for verification; (5) S decrypts the received message using B 's key, extracts the encrypted component and decrypts it using A 's key and re-encrypts under B 's key. If S replies $\{N_b\}_{k_{bs}}$, then B will find $N_b$ after decrypting it and he should be convinced that A is really running this session with him. The protocol is given in Table 1.

Woo and Lam stated that the protocol is correct if: ``whenever a responder finishes the execution of the protocol, the initiator is in fact the principal claimed in the initial message''. Nevertheless, the protocol is known to be flawed. In particular, Abadi and Needham presented an attack to the protocol in [4]. They noticed that an attack is possible because there is no connection between B 's request and S 's reply. The authors discussed again the protocol in their paper and finally suggested the new corrected version given in Table 2.

  Table 2:   The Corrected Version of the Woo and Lam Authentication Protocol

The next section is devoted to an informal presentation of our verification algorithm. The latter will be illustrated over the Woo and Lam authentication protocol described above.