/* * Broken protocol */ // The protocol description protocol protocol1(I,R) { role I { fresh ni: Nonce; var nr: Nonce; send_1(I,R, {R,ni}pk(R) ); recv_2(R,I, {ni,nr,R}pk(I) ); send_3(I,R, {nr}pk(R) ); claim_i1(I,Secret,ni); claim_i2(I,Secret,nr); claim_i3(I,Nisynch); } role R { var ni: Nonce; fresh nr: Nonce; recv_1(I,R, {R,ni}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); recv_3(I,R, {nr}pk(R) ); claim_r1(R,Secret,ni); claim_r2(R,Secret,nr); claim_r3(R,Nisynch); } }