The protocol specification in "Alice-Bob" notation is as follows.

1. A -> B : A,Na
2. B -> S : A,Na,B,Nb'
3. S -> B : E(Kbs:Nb',Kab,A), E(Kas:Na,Kab,B)
4. B -> A : E(Kas:Na,Kab,B),E(Kab:Nb,Na)
5. A -> B : E(Kab:Na,Nb)

For this protocol we considered the following three executions:

1. A regular execution of the protocol (denoted by attack-state(0)).
2. An execution in which the intruder finds out the Session key generated by the server (denoted by attack-state(1)).
3. An execution where Bob completed his protocol execution believing he was communicating with Alice, but it actually was not so (denoted attack-state (2)).

After the analysis of this protocol in Maude-NPA, the tool found an initial state corresponding to attack-state(0), which shows a completed regular execution of the protocol. However, the tool did not find any initial state for attack-state(1) and attack-state(2) which proves, respectively, that the protocol is secure against an attack to obtain the session key and against an authentication attack.

To download the complete protocol specification in Maude-NPA syntax click HERE