In this section, we show how to combine roles and inference rules so as to perform the verification of a given cryptographic authentication protocol. To keep the presentation simple, we will confine ourselves to the analysis of authentication properties. We will show further how to easily extend our verification algorithm to deal with security properties.
A principal A wishing to prove his identity to a principal B , has to answer all the challenges uttered by B . Hence, the intruder can impersonate the principal A if he can answer all those challenges uttered by B to A . Thus, the verification principal consists in checking whether the intruder, with all its computation abilities, can answer such challenges.
Actually, the intruder computation abilities consist of:
Now we come to the explanation of the verification procedure. Starting from the protocol description, we extract the roles. Now, for each role, the intruder will attempt to answer all the challenges uttered so as to perform a masquerade. The intruder will progressively follow the role in a stepwise way. For a given step, if the role sends a message, the intruder will merely store it and hence will extend his knowledge. If the role is waiting for receiving some particular message, the intruder will attempt to generate it using his current computation abilities. In other words, the intruder will try to synthesize the required message using his current knowledge modulo some composition/decomposition and encryption/decryption steps, and also up to the use of the deductive proof system.
Now, let us see how this applies to the unidirectional Woo and Lam authentication protocol of Table 1. Notice that the only concerned role is B . The corresponding role is:
Actually, before starting to take up the various challenges uttered by B , we have first to proceed to what we call the generalization of the role B . This operation aims to replace some messages by message variables as done in the deductive proof system. The rationale underlying such substitutions is that these messages could not be verified from the content, structure, freshness and type standpoint. This operation will be formally defined in the next section. The role B is rewritten into:
Here, we replace the message by a message variable X since B does not know the key , hence he could accept any other information.
First of all, let us initialize the knowledge of the intruder, noted KI , with the intruder initial knowledge. In other words, KI is set to . This means that the intruder initially knows the identity of the server S , his shared key with S , the role A and the role B .
Now the verification amounts to a constraint satisfaction problem. In fact, we are going to collect constraints that reflect the requirements that makes the intruder take up successfully all the challenges uttered by a particular role.
In the first step of the role B , the principal is waiting
for a message identifier, say A . To take up this challenge,
the intruder has to generate such an identifier from KI
modulo some composition/decomposition and
encryption/decryption steps, and also up to the use of the
deductive proof system. Such a constraint is written as:
where R stands for the set of the rules of Table 3 together with the usual composition/decomposition and encryption/decryption rules.
At the second step, B sends the nonce over the network. Hence, the message becomes available to the intruder who extends his current knowledge to become .
At the third step, the intruder must supply B with X .
Notice that the current knowledge of the intruder at this step
is . Accordingly, this second constraint will be written
At the fourth step, B offers the message to the intruder. The latter updates his knowledge to become .
Finally, the intruder has to supply the role B with in order to achieve the masquerade. This last
constraint will be written as:
At this level, we are ready to check whether the intruder can or cannot impersonate the role A . This amounts to check the existence of solutions to the constraint set which is the following system:
In fact, we use the resolution as a decision procedure for the simultaneous resolution of these constraints. The decision procedure yields a set of substitutions each of which denotes a potential flaw. Furthermore, the inference rules of the proof system are annotated by the associated scenarios. Thus, the application of these inference rules propagates these scenarios. Such a propagation yields also complete attack scenarios. To sum up, we extract automatically flaws and attack scenarios from protocol specifications.
In the case of the constraint set , the algorithm produces many flaws and attack scenarios. Most of these attacks are new and completely different from those known up to now. In what follows, we present in Table 4 one among the many elegant attacks yielded by our algorithm.
Table 4: An Attack of the Woo and Lam Authentication Protocol
The reader should notice that the attack reported in Table 4 is both elegant and sophisticated. The elegance of the attack stems from three facts:
Here is the way the attack of Table 4 could be carried out: In the communication step ``1.1.'', the intruder begins a session with B in order to claim that his identity is A . In the step ``1.2.'', the intruder I intercepts the nonce generated by B and send it to A . In the step ``1.3.'', I replies by a message anything which means any message since B cannot do any verification. In the step ``1.4.'', B must react according to the protocol by sending the message . This message will be intercepted by the intruder. To finish this protocol run, the intruder ultimately needs to synthesize the message in order to send it to B at the step ``1.5.''. To get this last required message, the intruder will open the sessions 2, 3 and 4. Notice that such a message could be get in a simpler way but for the sake of elegance we use all these sessions.
At the session 2, the intruder I waits for a principal C to initiate a session with another principal D . Then, he intercepts the message C and replies by the nonce in order to get the message at the step 3 of this session. This message will be used to generate the message . Indeed, the intruder has to wait that the same principal C initiates another session with another principal E as shown in Table 4. At the session 4, the intruder wants to obtain the message which makes easy getting the message . For instance, the intruder replies by the message as the C 's answer which is supposed to be . At the session 5, the intruder gets easily the message by sending the message obtained at the session 4 to the server S .
Finally, the intruder terminates the first session, step ``1.5.'', with B , by sending the message as an S 's response. Hence, from now on B is convinced that the initiator of the session one is A .