Aldebaran has discovered that the property P4 was not satisfied. The behaviour of
the registration protocol cannot be simulated by the graph of the property
regarding the relevant special events. It has found a sequence where a
USER_REG_FAILED occurs before a TTP_REG_SUCCEEDED. The TTP
successfully registers the user after the user has learned that his
registration failed. We use the Exhibitor tool to produce a diagnostic sequence that
immediately shows us how the intruder has built his attack. The scenario is
exhibited in figure 6.
When the intruder receives a registration request message from the user, he fowards it to the TTP and makes the first challenge fail with a fake response to obtain a negative acknowledgement from the TTP. Then the intruder follows on by replaying the registration request message previously recorded. Upon reception, the TTP starts a second registration with the user and sends a second challenge. This time, the intruder forwards the challenge to the user who is still waiting for his first challenge. The user replies with a valid message and waits for an acknowledgement. The intruder replays the negative one previously received. This acknowledgement is valid and thus the user declares that the registration failed. Meanwhile the intruder fowards the valid response of the user to the TTP who declares the registration successful. Both parties have finished their exchange but they do not have the same point of view of the situation.
For this attack to succeed, the intruder only needs to create a fake response to the first challenge. The strengh of our technique is that the analysis of the diagnostic sequence immediately brings us the reason of the failure. The acknowledgement of the TTP is too general because it can be considered valid in two distinct registrations.
