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 Tickets

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 , E(Kbs:A,B,Ta,Kab)
  4. A -> B : E(Kt:Na,Kab),E(Kbs:A,B,Ta,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(1)).
  3. An execution where Bob completed his protocol execution believing he was communicating with Alice, but it actually was not so (denoted 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 Alice in a communication with the server and, therefore, the protocol is insecure. The specification of this attack in "Alice-Bob" notation is as follows:

  1. I(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 , E(Kbs:A,B,Ta,Kab)
  4. A -> B : E(Kt:Na,Kab) , E(Kbs:A,B,Ta,Kab)

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

  1. I(A) -> S : G , Z , Ng
  2. S -> I(A) : E(Kgs:G,Z,Ng,Kgz,Kt) , E(Kzs:G,Z,Ng,Kgz,Kt)
  3. I(S) -> B : E(Kgs:G,Z,Ng,Kgz,Kt), E(Kbs,A,B,Na,Kgz,Kt)
  4. B -> I(A) : E(Kt:Ng,Kgz) , E(Kbs:A,B,Kt,Kgz) , E(Kt:Ng,Kgz)Nb , E(Kbs:A,B,Kt,Kgz)
  5. I(A) ->B : E(Kt:Ng,Kgz) , E(Kbs:A,B,Kt:Kgz)

Finally, when analyzing this protocol in Maude-NPA, the tool found also two initial states corresponding to attack-state(2), which proves that this protocol is vulnerable to an authentication attack and, therfore, it is insecure. The specification in "Alice-Bob" notation of the first attack is as follows:

  1. I(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 , E(Kbs:A,B,Ta,Kab)
  4. A -> B : E(Kt:Na,Kab) , E(Kbs:A,B,Ta,Kab)

The specification of the second attack in "Alice-Bob" notation is as follows:

  1. I(A) -> S : G , Z , Ng
  2. S -> I(A) : E(Kgs:G,Z,Ng,Kgz,Kt) , E(Kzs:G,Z,Ng,Kgz,Kt)
  3. I(S) -> B : E(Kgs:G,Z,Ng,Kgz,Kt) , E(Kbs,a,b,Na,Kgz,Kt)
  4. B -> I(A) : E(Kt:Ng,Kgz) , (Kbs:a,b,Kt,Kgz) , E(Kt:Ng,Kgz) , Nb , E(Kbs:a,b,Kt,Kgz)
  5. I(A) -> B : E(Kt:Ng,Kgz) , E(Kbs:a,b,Kt:Kgz)

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