(* Public-key encryption *) type pkey. type skey. fun pk(skey):pkey. fun aenc(bitstring,pkey):bitstring. reduc forall x:bitstring, sk:skey; adec(aenc(x,pk(sk)),sk) = x. (* Symmetric encryption *) fun senc(bitstring,bitstring):bitstring. reduc forall x:bitstring, k:bitstring; sdec(senc(x,k),k) = x. free c : channel. (* Secrets for expressing the secrecy of established nonces * at various points of the protocol. *) free secretIna : bitstring [private]. free secretInb : bitstring [private]. free secretRna : bitstring [private]. free secretRnb : bitstring [private]. (* Secret keys of honest agents: secrecy of nonces and * authentication queries can only be asked for those. *) free ska:skey [private]. free skb:skey [private]. (* The initiator engages with an agent whose public key * is given (by the attacker) in a first input. *) let initiator(ska:skey) = let pka = pk(ska) in in(c,pkb:pkey); new na:bitstring; out(c,aenc((pka,na),pkb)); in(c,x:bitstring); (* The next line is equivalent to a "let" * for decryption, followed by projections, * and an equality test against na. *) let (=na,nb:bitstring,=pkb) = adec(x,ska) in out(c,aenc(nb,pkb)); if pkb = pk(skb) then out(c,senc(secretIna,na)); out(c,senc(secretInb,nb)). (* The responder is willing to engage with any agent. *) let responder(skb:skey) = let pkb = pk(skb) in in(c,x:bitstring); new nb:bitstring; let (pka:pkey,na:bitstring) = adec(x,skb) in out(c,aenc((na,nb,pkb),pka)); in(c,y:bitstring); if nb = adec(y,skb) then if pka = pk(ska) then out(c,senc(secretRnb,na)); out(c,senc(secretRna,nb)). query attacker(secretRna). query attacker(secretRnb). query attacker(secretIna). query attacker(secretInb). set verboseClauses = short. process out(c,pk(ska)); out(c,pk(skb)); !initiator(ska) | !responder(skb)