/* A key exchange protocol */ // Hash function: nobody knows the inverse hashfunction hash; // User type declaration usertype Key; // Protocol description protocol protocol2(I,R) { role I { fresh ni: Nonce; var nr: Nonce; var kir: Key; send_1 (I,R, { ni,I }pk(R) ); recv_2 (R,I, { hash(kir,ni,R),nr,kir }pk(I) ); send_3 (I,R, { hash(nr,ni) }kir ); claim_i1 (I, Secret, kir ); claim_i2 (I, Nisynch ); } role R { var ni: Nonce; fresh nr: Nonce; fresh kir: Key; recv_1 (I,R, { ni,I }pk(R) ); send_2 (R,I, { hash(kir,ni,R),nr,kir }pk(I) ); recv_3 (I,R, { hash(nr,ni) }kir ); claim_r1 (R, Secret, kir ); claim_r2 (R, Nisynch ); } }