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

Carlsen's Secret Key Initiator Protocol

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

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

For this protocol we will consider the following three 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 a completed regular execution of the protocol.

When analyzing attack-state(1) the tool did not find any initial state and, thus, the protocol is secure against an attack to obtain the session key.

After the analysis of the attack-state(2) Maude-NPA did not find any inital state and, thus the protocol is secure against an authentication attack.

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