(*
 
 WEP Shared Key Authentication protocol

    WD = Wireless Device
    AP = Access Point

    WD and AP are supposed to share a secret key k.
   
    WD -> AP : Request
    AP -> WD : Challenge
    WD -> AP : {Challenge}k

    Here {m}k = xor(m,k)

 *)

(* Types and functions *)

set ignoreTypes = attacker.

type host.
type key.
type challenge.

fun encrypt(challenge,key):bitstring.
reduc forall c:challenge, k:key; decrypt(encrypt(c,k),k) = c.

fun genchall(bitstring):challenge [private].
reduc forall s:bitstring; checkchall(genchall(s)) = true [private].

(* Simulate xor *)
reduc forall c:challenge, k:key; xor(encrypt(c,k),c) = k.

(* variables *)
free net:channel.
free k:key [private].

(* events *)
event requestsAuth(challenge).
event confirmsAuth(challenge).

(* queries *)
query c:challenge; inj-event(confirmsAuth(c))==>inj-event(requestsAuth(c)).

let wdprocess(wd:host) =
    out(net,wd);
    in(net,(chal:challenge));
    if checkchall(chal) = true then
    event requestsAuth(chal);
    out(net,encrypt(chal,k));
    0.

let approcess(ap:host) =
    in(net,h:host);
    new s:bitstring;
    let chal = genchall(s) in
    out(net,chal);
    in(net,cc:bitstring);
    let (=chal) = decrypt(cc,k) in
    event confirmsAuth(chal);
    0.

let launchwd =
    new wd:host;
    wdprocess(wd).

process
    new ap:host;
    ( (!launchwd) | (!approcess(ap)) )