(* Honest Hosts (kS = trusted server) *)
free A,B,kS.

(* Channel for A - B communication *)
free c.
(* Channel for id sharing *)
free d.
(* Channels for cert sharing *)
free e,f.

(* Private keys of initiator and responder *)
private free kI, kR.

(* Function for verification key (public), takes private key as param *)
fun vk/1.

fun sign/2.

reduc getmess(sign(m,k)) = m.
reduc checksign(sign(m,k),vk(k)) = m.

free text1,text2,text3.

query ev:end(id1,id2,nb) ==> ev:begin(id1,id2,nb).
query evinj:end(id1,id2,nb) ==> evinj:begin(id1,id2,nb).

query ev:end(id2,id1,na) ==> ev:begin(id2,id1,na).
query evinj:end(id2,id1,na) ==> evinj:begin(id2,id1,na).

let initiator =
    in(d,(idI,idR));
    new nb;
    out(c,(nb,text1));
    in(c,(certR,x));    (* Receive signed cert from server *)
    let (vkR,=idR)=checksign(certR,vk(kS)) in         (* Check server sig *)
    let (na,=nb,=idI,text2)=checksign(x,vk(kR)) in   (* Check responder sig *)
        event end(idR,idI,nb);
    event begin(idI,idR,na);
    in(f,(certI));
    out(c,(certI,sign((nb,na,idR,text3),kI)));
    0.


let responder =
    in(d,(idI,idR));
    in(c,(nb,text1));
    event begin(idR,idI,nb);
    in(e,(certR));      (* Receive signed cert from server *)
    new na;
    out(c,(certR,sign((na,nb,idI,text2),kR)));
    in(c,(certI,x));
    let (vkI,=idI)=checksign(certI,vk(kS)) in         (* Check server sig *)
    let (=nb,=na,=idR,text3)=checksign(x,vk(kI)) in   (* Check initiator sig *)
        event end(idI,idR,na);
    0.

let server =
    in(d,(idI,idR));
    new kS;
    out(e,sign((vk(kR),idR),kS));
    out(f,sign((vk(kI),idI),kS));
    0.

process
    new d;
    ! out(c,vk(kI)) | ! out(c,vk(kR)) | ! out(c,vk(kS)) |   (* Output verification keys *)
    ! initiator | ! responder | ! out(d,(A,B)) | ! out(d,(B,A))