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

Woo and Lam Authenticacion Protocols

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

  1. A -> B : A
  2. B -> A : Nb
  3. A -> B : E(Kas:Nb)
  4. B -> S : E(Kbs:A,E(Kas:Nb))
  5. S -> B : E(Kbs:Nb)
For this protocol we considered the following execution:
  1. A regular execution of the protocol (denoted by attack-state(0)).

After the analysis of this protocol in Maude-NPA, the tool found an initial state corresponding to attack-state(0). This initial state shows an authentication attack in which Bob completed his protocol execution believing he was communicating with Alice, but he was actually communicating with the intruder. Therefore, the protocol is insecure. The specification of this attack in "Alice-Bob" notation is as follows:

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

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