prot.pv

(* declaring a free channel name *)
free c:channel.

(* declaring additional types; type bitstring is a default type *)
type pkey.
type skey.


(* declaring private names *)
free ska, skb, skc:skey [private]. 


(* Public key cryptography *)
fun pk(skey):pkey.		        (* public key*)
fun aenc(bitstring, pkey):bitstring. 	(* asymmetric encryption *)
fun adec(bitstring, skey):bitstring.	(* asymmetric decryption *)
fun h(bitstring):bitstring. (* hash function *)


(* equational theory for pk encryption *)
equation forall x:bitstring, y:skey; adec(aenc(x,pk(y)),y) = x.


(* events *)
event acceptI(pkey, pkey, bitstring, bitstring).
event startR(pkey, pkey, bitstring, bitstring).
event acceptR(pkey, pkey, bitstring, bitstring).
event startI(pkey, pkey, bitstring, bitstring).


(* queries *)
(*query attacker(new ki).*)
query x1:pkey, x2:pkey, x3:bitstring, x4:bitstring; event(acceptI(x1,x2,x3,x4)) ==> event(startR(x1,x2,x3,x4)).
query x1:pkey, x2:pkey, x3:bitstring, x4:bitstring; event(acceptR(x1,x2,x3,x4)) ==> event(startI(x1,x2,x3,x4)).


(* initiator process *)
let Pi(ski:skey, pkr:pkey) = 
  new ki:bitstring;

  (* Send the first message *)
  out(c, (h((pk(ski),ki)), aenc(ki, pkr)));

  (* Receive the second message *)
  in(c, (x1:bitstring, x2:bitstring));
  let (W:bitstring) = adec(x2, ski) in
  (* Check the hash *)
  let (=h((pkr, ki, W)), nr:bitstring) = x1 in

  (* Send the last message*)
  event startI(pk(ski),pkr,ki,W);
  out(c, h(W));
  if pkr <> pk(skc) then
    event acceptI(pk(ski),pkr,ki,W). 

(* responder process *)
let Pr(skr:skey, pki:pkey)=
  (* Receive the first message *)
  in(c, (y1:bitstring, y2:bitstring));
  let (V:bitstring) = adec(y2, skr) in
  let (=h((pki,V))) = y1 in

  (* Send the second message *)
  new nr:bitstring;
  event startR(pki,pk(skr),V,nr);
  out(c, (h((pk(skr), V, nr)), aenc(nr, pki)));

  (* Receive the last message *)
  in(c, y3:bitstring);
  if h(nr) = y3 && pki <> pk(skc) then
    event acceptR(pki,pk(skr),V,nr).
			
(* main process *)
(* Check for secrercy of K *)   
(*process  ( ! Pi(ska, pk(skb)) | ! Pr(skb, pk(ska))
         | out(c, pk(ska)) | out(c, pk(skb)) | out(c,skc))*)

(* Check authentication *)
process  ( ! Pi(ska, pk(ska)) | ! Pi(ska, pk(skb)) | ! Pi(ska, pk(skc))
         | ! Pi(skb, pk(ska)) | ! Pi(skb, pk(skb)) | ! Pi(skb, pk(skc))
         | ! Pr(ska, pk(ska)) | ! Pr(ska, pk(skb)) | ! Pr(ska, pk(skc))
         | ! Pr(skb, pk(ska)) | ! Pr(skb, pk(skb)) | ! Pr(skb, pk(skc))
         | out(c, pk(ska)) | out(c, pk(skb)) | out(c,skc))