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

Amended Needham Schroeder

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

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

For this protocol we considereded the following executions:

  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), which shows an attack in which the intruder impersonates the server and, thus, the protocol is insecure. The specification of this attack in "Alice-Bob" notation is as follows:

  1. A -> B : A
  2. B -> A : E(Kbs:A,Nb0)
  3. A -> Z(S) : A,B,Na,E(Kbs:A,Nb0)
  4. Z(S) -> A : E(Kas:Na,B,Kab,E(Kbs:Kab,Nb0,A))
  5. A -> B : E(Kbs:Kab,Nb0,A)
  6. B -> A : E(Kab:Nb)
  7. A -> B : E(Kab:Nb-1)
To download the specification of the protocol in Maude-NPA syntax and outputs, click HERE.