(* Channel *)
free c.

free error1,error2,GetC.

fun vk/1.
fun sign/2.
reduc checksign(sign(m,k),vk(k))=m.
reduc getmess(sign(m,k))=m.

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=checksign(cert,vk(km)) in
        let (nr,=nt,kr)=sdec(x,ke) in
            new kt;
            out(c,sign(senc((nt,nr,kt),ke),km))
        else
            out(c,error2)
    else
        out(c,error1);
    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)])
        )
    )