pred begin/1 block. pred c/1 elimVar,decompData. nounif c:x. fun pk/1. fun sign/2. fun sA/0. fun sB/0. fun na1/1. fun nb/4. fun na2/2. query end:x. reduc (* Initialization *) c:pk(sA()); c:pk(sB()); (* The attacker *) c:x -> c:pk(x); c:x & c:y -> c:sign(x,y); c:sign(x,y) -> c:y; ver:(sign(x,y),pk(x)); (* The protocol *) (* first message *) c:na1(i); c:n & c:pk(a) & c:pk(b) -> c:sign(b,(n,nb(i,pk(a),pk(b),n),pk(a))); c:na1(i) & c:sign(b,(na1(i),n,pk(a))) & begin:(pk(a),pk(b)) -> c:sign(a,(n,na2(i,sign(b,(na1(i),n,pk(a)))),pk(b))); c:n & c:sign(sA(),(nb(i,pk(sA()),pk(sB()),n),nn,pk(sB()))) -> end:(pk(sA()),pk(sB())).