(* A public channel. *)
free net.

(* the CA keypair *)
private free caKeyPair.

(* the empty session id *)
free emptyId.

(* The name of a compromised agent. *)
free spy.

(* Private channels for agent initalization. *)
private free initialInitiatorData, initialResponderData,initiatorSids,responderSids.

(* The cryptographic constructors. *)
fun pencrypt/2.       (* public key encryption *)
fun encrypt/2.		  (* symmetric encryption *)
fun hash/1.			  (*hash function*)
fun sign/2.           (* digital signing *)
fun enc/1.            (* extracts encryption key from a key-pair *)
fun dec/1.            (* extracts decryption key from a key-pair *)
fun prf/3.			  (* the pseudo random function to create M*)
fun clientK/3.		  (* the function to create the client key *)
fun serverK/3. 		  (* the function to create the server key *)

(* The cryptographic destructors. *)
(* pdecrypt/2. *)      
reduc pdecrypt(pencrypt(x,enc(y)),dec(y)) = x.
reduc decrypt(encrypt(x,y),y) = x.
(* unsign/2. *)
reduc unsign(sign(x,enc(y)),dec(y)) = x.

(* A constructor that maps agents to their secret keypairs. *)
private fun pubkeypair/1.
private fun signkeypair/1.

(* Lookup function for public keys. *)
(* pubkey/1. *)
reduc pubkey(agent) = enc(pubkeypair(agent)).
(* unsignkey/1. *)
reduc unsignkey(agent) = dec(signkeypair(agent)).

(* The queries. *)
private free pmsFlag.
query attacker: pmsFlag.
private free prfFlag.
query attacker: prfFlag.

private free pmsFlag2.
query attacker: pmsFlag2.
private free prfFlag2.
query attacker: prfFlag2.

(* Correspondence arrestions *)

query evinj : endServerAuth(b,pms) ==> evinj : startServerAuth(b,pms).
query evinj : endServerAuth2(b,pms2) ==> evinj : startServerAuth2(b,pms2).
query evinj : endClientAuth(a,pms2) ==> evinj : startClientAuth(a,pms2).
(* The initiator process. *)
let initiator = 
  (* ProVerif doesn't have parameterized processes. So agents need to get 
     their initial data as input over a trusted channel. *)
  (* Begin getting initial agent data. *)
  in(initialInitiatorData, (a, sa, certA, caDecKey));   
  (* End getting initial agent data. *)  
  !               (* replicate to model arbitrary no. of sessions *)
  new na;
  out(net, (a, na, emptyId));
  in(net, (nb, sid));
  in(net, certb);
  let (b, pb) = unsign(certb, caDecKey) in 
  new pms;
  out(net, pencrypt(pms, pb));
  let m = prf(pms, na, nb) in 
	(if b<>spy then 
	out(pms,pmsFlag);(* Flag for  querying pms' secrecy *)
	out(m,prfFlag) (* Flag for  querying m's secrecy *) 
	)| 
  let finished = hash((sid, m, na, nb, b)) in
  out(net, encrypt(finished, clientK(na,nb,m)));
  in(net, finishedB);
  let =finished = decrypt(finishedB, serverK(na,nb,m)) in 
  (if b<>spy then
	event endServerAuth(b,pms))|   out(initiatorSids,(sid,pms,b))
  .

  
(* The responder process. *)
let responder =
  (* Begin getting initial agent data. *)
  in(initialResponderData, (b,db, cert, caDecKey));
  in(net, (a, na, =emptyId));
  new nb;
	(* New session, follow the complete protocol *)
	new sid;
	out(net, (nb, sid));
	out(net, cert);
	in(net, cpms);
	let pms = pdecrypt(cpms, db) in	
	event startServerAuth(b,pms);
	let m = prf(pms, na, nb) in  

	let finished = hash((sid, m, na, nb, b)) in 
	in(net, finishedA);
	let =finished = decrypt(finishedA, clientK(na,nb,m)) in
	out(net, encrypt(finished, serverK(na,nb,m)));
	  out(responderSids,(sid,pms,a))
	.  

 (* The initiator process. *)
let initiatorExt = 
  (* ProVerif doesn't have parameterized processes. So agents need to get 
     their initial data as input over a trusted channel. *)
  (* Begin getting initial agent data. *)
  in(initialInitiatorData, (a, sa, certA, caDecKey));  
  (* End getting initial agent data. *)  
  !               (* replicate to model arbitrary no. of sessions *)
  new na;
  out(net, (a, na, emptyId));
  in(net, (nb, sid));
  in(net, certb);
  let (b, pb) = unsign(certb, caDecKey) in 
  (* ============= send certificate for a ===================*)
  out(net, certA);
  new pms2;
	event startClientAuth(a,pms2);
  out(net, pencrypt(pms2, pb));
  out(net, sign(hash((nb,b,pms2)), sa));
  let m = prf(pms2, na, nb) in 
  (if b<>spy then 
	out(pms2,pmsFlag);(* Flag for  querying pms' secrecy *)
	out(m,prfFlag) (* Flag for  querying m's secrecy *) 
	)| 
  let finished = hash((sid, m, na, nb, b, a)) in
  out(net, encrypt(finished, clientK(na,nb,m)));
  in(net, finishedB);
  let =finished = decrypt(finishedB, serverK(na,nb,m)) in 
   (if b<>spy then
	event endServerAuth2(b,pms2))|   out(initiatorSids,(sid,pms2,b)).	
 
 (* The responder process. *)
let responderExt =
  (* Begin getting initial agent data. *)
  in(initialResponderData, (b,db, cert, caDecKey));
  in(net, (a, na, =emptyId));
  new nb;
  new sid;
  out(net, (nb, sid));
  out(net, cert);
  in(net, certA);
  let (=a, pa) = unsign(certA, caDecKey) in 
  in(net, cpms);
  let pms2 = pdecrypt(cpms, db) in
	event startServerAuth2(b,pms2);
  (* =============== verify certificate from a =========================*)
  in(net, signA);
  let hashA = unsign(signA, pa) in 
  let =hashA = hash((nb, b, pms2)) in 
  (if a<> spy  then
	event endClientAuth(a,pms2))|
  let m = prf(pms2, na, nb) in  
  (if a<>spy then 
	out(pms2,pmsFlag2);(* Flag for  querying pms' secrecy *)
	out(m,prfFlag2) (* Flag for  querying m's secrecy *) 
	)| 
  let finished = hash((sid, m, na, nb, b, a)) in 
  in(net, finishedA);
  let =finished = decrypt(finishedA, clientK(na,nb,m)) in
  out(net, encrypt(finished, serverK(na,nb,m)));
  out(responderSids,(sid,pms2,a))
 .
 
 let initiatorResume = 
  (* Begin getting initial agent data. *)
  in(initialInitiatorData, (a, sa, certA, caDecKey));   
  (* End getting initial agent data. *)  
  !               (* replicate to model arbitrary no. of sessions *)
  new na;
  in(initiatorSids, (sid, pms,b));
  out(net, (a, na, sid));
  in(net, (nb, =sid));
  let m = prf(pms, na, nb) in 
    (if b<>spy then 
	out(pms,pmsFlag);(* Flag for  querying pms' secrecy *)
	out(m,prfFlag) (* Flag for  querying m's secrecy *) 
	)| 
  let finished = hash((sid, m, na, nb)) in
  out(net, encrypt(finished, clientK(na,nb,m)));
  in(net, finishedB);
  let =finished = decrypt(finishedB, serverK(na,nb,m)) in 
  0
  .
 
 let responderResume =
  (* Begin getting initial agent data. *)
  in(initialResponderData, (b,db, cert, caDecKey));
  in(net, (a, na, csid));
  new nb;
  (* Resumed session, lookup in the database and continue session *)
if csid <> emptyId then
  in(responderSids,(=csid,pms));

	out(net,(nb,csid));
	let m = prf(pms, na, nb) in  
	(if a<>spy then 
	out(pms,pmsFlag2);
	out(m,prfFlag2) 
	)| 
	let finished = hash((csid, m, na, nb, b)) in 
	in(net, finishedA);
	let =finished = decrypt(finishedA, clientK(na,nb,m)) in
	out(net, encrypt(finished, serverK(na,nb,m)))
else
	0
	.


(* The initializer process. *)
let initializer = 
  new agent;                            (* generate agent name *)
  let pkp = pubkeypair(agent) in        (* compute public encryption keypair *)
  let skp = signkeypair(agent) in		(* compute signing keypair *)
  out(initialInitiatorData, (agent, enc(skp), sign((agent,dec(skp)), enc(caKeyPair)), dec(caKeyPair)));    (* launch initiator role *)
  out(initialResponderData, (agent, dec(pkp), sign((agent,enc(pkp)), enc(caKeyPair)), dec(caKeyPair)));    (* launch responder role *)
  out(net, (agent, dec(caKeyPair), sign((agent,dec(skp)), enc(caKeyPair)), sign((agent,enc(pkp)), enc(caKeyPair)))).(* publish the public data *)

(* The compromised agent. *)
let compromised =
  let pkp = pubkeypair(spy) in  (* compute public encryption keypair *)
  let skp = signkeypair(spy) in
  out(net, (pkp, skp)).          (* publish the keypairs to model compromise *)

(* The system. *)  
process 
  !initiator                    (* initiators *) 
| !responder                    (* responders *)
| !initiatorExt
| !responderExt
| !initiatorResume
| !responderResume
| compromised                    (* the spy *)
| !initializer                  (* launch the system *)