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 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
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
is a nonce that belongs to
A and
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 is a nonce, a random number generated by B
specially for this protocol run, S is a server and
and
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
and asking A to
encrypt it under
in order to prove what he
claimed; (3) A returns the nonce
encrypted
under
; (4) B forwards the response encrypted,
together with A 's identity, under
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
, then B will find
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.