Maude-NPA

Repository of protocol specifications in Maude-NPA

Home
Denning–Sacco Otway-Rees Amended Needham Schroeder Wide Mouthed Frog Yahalom Carlsen’s Secret Key Initiator ISO 5-pass Authentication Woo and Lam Authentication Kao-Chow Kao-Chow with handshake key Kao-Chow with tickets Secret 06 & 07 Diffie-Hellman
Needham Schroeder Lowe ECB
Needham Schroeder Lowe XOR TMN Wired Equivalent Privacy Smart Cards (SK3)
IBM CCA CCA 0 CCA 0 Küesters IBM’s recommendations to avoid CCA-0’s attack Yubikey
PKCS#11
Choice Protocols Distance-Bounding Protocols Hash Functions Vulnerabilities Contact and links

Wide Mouthed Frog Protocol

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

  1. A -> S : A,E(Kas:B,Kab)
  2. S -> B : E(Kbs:A,Kab)
  3. A -> B : A,E(Kab:M)

For this protocol we considered the following 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)).

After the analysis of this protocol in Maude-NPA, the tool found an initial state corresponding to attack-state(0), which shows an attack in which the intruder impersonates Alice and the server and, thus, the protocol is insecure. The specification of this attack in "Alice-Bob" notation is as follows:

  1. Z(A) -> Z(S) : A,E(Kas:B,Kab)
  2. Z(S) -> B : E(Kbs:A,Kab)
  3. Z(A) -> B : A,E(Kab:M)

After the analysis of this protocol in Maude-NPA, the tool also found an initial state corresponding to attack-state(1), which shows that the protocol has an attack and, therefore, it is insecure. The specification of this attack in "Alice-Bob" notation is as follows:

  1. Z(A) -> Z(S) : A,E(Kas:B,Kab)
  2. Z(S) -> B : E(Kbs:A,Kab)
  3. Z(A) -> B : A,E(Kab:M')

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