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

Wired Equivalent Privacy Protocol

Wired Equivalent Privacy (WEP) is a security algorithm for IEEE 802.11 wireless networks. Introduced as part of the original 802.11 standard ratified in 1997, its intention was to provide data confidentiality comparable to that of a traditional wired network. WEP, recognizable by its key of 10 or 26 hexadecimal digits (40 or 104 bits), was at one time widely in use and was often the first security choice presented to users by router configuration tools.

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

  1. (1) A -> X : v,([M1,C(M1)] ⊕ RC4(v,KAX))
  2. (2) A -> B : v,([M2,C(M2)] ⊕ RC4(v,KAB))

The property to be verified was the secrecy of M2 between A and B. There is an attack:

  1. (0.1) A -> B : v,([M1,C(M1)] ⊕ RC4(v,KAB))
  2. (0.2) A -> I : v,([M1,C(M1)] ⊕ RC4(v,KAI))
  3. (1) A -> I : v,([M2,C(M2)] ⊕ RC4(v,KAB))

A fix is to send a different 'v' with every message. We have defined 2 separate strands, one just sending a single message as in the actual protocol, the other sending the same payload twice but under different keys, which is legal in this protocol and will be used to break it.

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