(* 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: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 *)


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

(* events *)
	(* declare events here *)


(* queries *)
	(* fill in queries here *)



(* initiator process *)
let Pi(ski:skey, pkr:pkey) = 
	 new na:bitstring; 
	 out(c, aenc((pk(ski),na), pkr));
	 in(c, x:bitstring);
	 let (=na, nr:bitstring) = adec(x, ski) in 
	 	 (* '=na' checks that the value is equal to na, else behaves as 0 *)
		 (* one could have used an if statement as well  *)
	 out(c, aenc(nr,pkr)).
	 

(* responder process *)
let Pr (sk:skey)= (* fill in the process *) 0.


(* main process *)
process  ( Pi(ska, pk(skb)) | Pr(skb) | out(c, pk(ska)) | out(c, pk(skb)))