(* Channel *)
free c.

free error1,GetC.

fun vk/1.
fun sign/2.
fun true/0.
fun false/0.

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

reduc verify(sign(m,k),vk(k))=true
      otherwise verify(sign(m,k),x)=false.

reduc eq(x,x)=true
    otherwise eq(x,y)=false.

reduc and(true,true)=true
    otherwise and(x,y)=false.

fun senc/2.
reduc sdec(senc(m,k),k)=m.

let passport =
    in(d,(ke,km));
    in(c,=GetC);
    new nt;
    out(c,nt);
    in(c,cert);
    let x=getmess(cert) in
        let (nr,nt2,kr)=sdec(y,ke) in
            if and(verify(cert,vk(km)),eq(nt,nt2))=false then
                out(c,error1)
            else
                new kt;
                out(c,sign(senc((nt,nr,kt),ke),km));
    0.


let reader =
    in(d,(ke,km));
    out(c,GetC);
    in(c,nt);
    new nr;
    new kr;
    out(c,sign(senc((nr,nt,kr),ke),km));
    in(c,cert);
    let x=checksign(cert,vk(km)) in
        let (=nt,=nr,kt)=sdec(x,ke) in
    0.


process
    new ke1;
    new km1;
    new ke2;
    new km2;
    new d;
    (
        ! reader                (* Start the reader *)
        | out(d,(ke1,km1))      (* Send out first key pair *)
        | out(d,(ke2,km2))      (* Send out second key pair *)
        | passport              (* Start first passport *)
        | passport              (* Start second passport *)
        (* Attacker records the signatures sent by reader *)
        | phase 1;
        (
            (* Start process again with either first or second key pair *)
            passport
            | out(d,choice[(ke1,km1),(ke2,km2)])
        )
    )