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

Smart Cards (SK3)

The Symmetric Key distribution using Smart Cards (SK3) protocol is a key distribution protocol for smart cards, which uses the XOR operator The informal description of the protocol assumes that the communication between smart cards and participants Alice and Bob is secure and therefore the attacker can not extract anything from that communication.

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

  1. (1) A -> S : A,B
  2. (2) S -> A : Pab,{Pab,B,2}Ka
  3. (3) A -> B : A,Na
  4. (4) B -> A : Nb,{Na,Nb,1}Kab
  5. (5) B -> A : {Sk}Kab
  6. (6) A -> B : {Nb,0,1}Kab

Where A, B denote principal names, Na and Nb denote nonces generated by participants, {M}K denotes encryption of message M using key K, ⊕ is the exclusive-or operator and 0 and 1 denote a sortarbitrary padding constants, known by all principals.

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