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

For this protocol we will consider 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.

When analyzing attack-state(1) the tool did not find any initial state and, thus, the protocol is secure against an attack to obtain the session key.

After the analysis of attack-state(2) the tool found an initial state which shows that the protocol has an authentication attack, and therefore, is insecure. The specification of this attack in "Alice-Bob" notation is as follows:

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