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/3. query c:secret(). reduc (* Initialization *) c:cname(); c:pk(sA()); c:pk(sB()); (* 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))); (* second message *) c:encrypt(pk(b),(pk(a),n,kk)) -> c:encrypt(pk(a),(n,n2(pk(a),pk(b),i),pk(b))); (* third message *) c:encrypt(pk(a),(n1(pk(a),pk(b),i),nn,pk(b))) -> c:encrypt(pk(b),(n1(pk(a),pk(b),i),nn)); (* fourth message *) c:encrypt(pk(sB()),(pk(sA()),n,kk)) & c:encrypt(pk(sB()),(n,n2(pk(sA()),pk(sB()),i))) -> c:sencrypt(kk,secret()).