In this section, we illustrate the application of our algorithm to the corrected version of the Woo and Lam protocol of Table 2. We will see that new flaws have been automatically discovered. First of all, here is the roles as extracted by the algorithms:
Their associated generalized roles are respectively:
The generalized roles are used by the function RoleRules(GRole,KI,Fresh) to generate the inference system. This step yields the rules shown in Table 7. Since the protocol is a one way authentication, the intruder try only to convince a principal playing a role B that it is a principal A. Let IS be the inference system and KI the intruder initial knowledge,according to the B 's generalized role the constraint set is:
Table 7:
The Deductive Proof System Associated
with the Corrected Version of Woo and
Lam Protocol
The resolution step yields the two following attacks:
In this attack, the intruder uses two sessions in order to
convince a principal playing B 's role that he is the
principal A. Here, the intruder meets no difficulties to
supply B with the required messages except the last one,
. For that reason, the intruder waits for
B to begin a session with some principal, say C . For
instance, I intercepts the B 's message and replies by
as a C nonce. Hence, it obtains the message
at step 2.3 by which it completes the
masquerade in session one.
In this scenario, the main session is session 1 where I is
trying to convince B that he is the agent A . The intruder
I sends the identity of A to the principal B which
replies by sending a nonce . As explained previously, at
step 1.3, I can send any arbitrary value X because B is
unable to perform any verification on the received message. At
step 1.4, B sends (A, B, X) to S . At this step, one can
imagine that S refuses the received message, but this is not
important for the rest of the attack scenario. After this step
I needs
in order to progress in the
protocol's steps. That explains why a parallel session with
A is initiated.