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

Kao-Chow Repeated Authentication Protocol with Handshake Key

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

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

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 attack in which the intruder obtains the session key (Kab) and, therefore, the protocol is insecure. The specification in "Alice-Bob" notation is as follows:

  1. I -> A : Kis
  2. A -> I : A , I , Na
  3. S -> B : E(Kas:A,B,Na,Kab,Kt) , E(Kbs:A,B,Kab,Kt)
  4. I -> A : E(Kis:A,I,Na,Kai,Kbs)
  5. I -> A : A , I , Na , Kai , Kbs
  6. I -> A : I,Nb,Kai,Kbs
  7. I -> A : Nb , Kai, Kbs
  8. I -> A : Kai , Kbs
  9. I -> A : Kbs
  10. I(A) -> B : E(Kt,Na,Kab)
  11. I(S) -> B : Kbs [Generated by intruder]
  12. A -> S : A , B , Na , Kab , Kt
  13. I(S) -> B : E(Kbs:A,B,Na,Kab,Kt)
  14. I(S) -> B : E(Kbs:A,B,Na,Kab,Kt) , E(Kbs:A,B,Na,Kab,Kt)
  15. B -> A : E(Kas:A,B,Na,Kab) , E(Kt:Na,Kab,Nb)
  16. A -> B : E(Kt:Na,Kab)
To download the complete protocol specification in Maude-NPA syntax and outputs, click HERE