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

Secret 06 & 07

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

  1. (1) S -> A : Ns
  2. (2) A -> B : sk(A,Ns ; S)
  3. (3) A -> B : sk(A,B ; Na ; S)

Where Na, Ns, and Nb are nonces, and sk(x,y) means message y encripted using private key x.

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

  1. (1) A -> B : A
  2. (2) A -> B : B
  3. (3) A -> B : exp(g,Na)
  4. (4) B -> A : B
  5. (5) B -> A : A
  6. (6) B -> A : exp(g,Nb)
To download the complete protocol specification in Maude-NPA syntax and the outputs, click Secret 06 and Secret 07