pred c/1 elimVar,decompData. nounif c:x. fun pk/1. fun encrypt/2. fun sencrypt/2. fun secret/0. fun cname/0. fun sA/0. fun sB/0. fun k/3. fun n1/3. fun n2/4. fun fst/0. fun snd/0. query c:secret(). reduc (* Initialization *) c:cname(); c:pk(sA()); c:pk(sB()); c:fst(); c:snd(); (* The attacker *) c:x & c:encrypt(pk(x),m) -> c:m; c:x -> c:pk(x); c:x & c:y -> c:encrypt(x,y); c:x & c:sencrypt(x,m) -> c:m; c:x & c:y -> c:sencrypt(x,y); (* The protocol *) (* first message *) c:pk(a) & c:pk(b) -> c:encrypt(pk(b),(pk(a),n1(pk(a),pk(b),i),k(pk(a),pk(b),i),fst())); (* second message *) c:encrypt(pk(b),(pk(a),n,kk,fst())) -> c:encrypt(pk(a),(n,n2(pk(a),pk(b),i,encrypt(pk(b),(pk(a),n,kk,fst()))),pk(b),snd())); (* third message *) c:encrypt(pk(a),(n1(pk(a),pk(b),i),nn,pk(b),snd())) -> c:encrypt(pk(b),(n1(pk(a),pk(b),i),nn)); (* fourth message *) c:encrypt(pk(sB()),(pk(sA),n,kk,fst())) & c:encrypt(pk(sB()),(n,n2(pk(sA()),pk(sB()),i,encrypt(pk(sB()),(pk(sA),n,kk,fst()))))) -> c:sencrypt(kk,secret()).