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

Otway-Rees Protocol

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

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

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(2)).

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 : Na' , A , B , E(Kas:Na,Na',A,B)
  2. B -> Z(S) : Na', A, B , E(Kbs,Na,Na',A,B), E(Kbs,Nb,Na',A,B)
  3. Z(S) -> B : Na' , E(Kas,Na,Kab) , E(Kbs,Nb,Kab)
  4. B -> A : Na' , E(Kas,Na,Kab)

Maude-NPA also found an initial state for attack-state(2) and, therefore, the protocol is insecure. The specification of the attack in "Alice-Bob" notation is as follows:

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

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