/* * Secrecy protocol * * Uses symmetric encryption */ // The protocol description protocol protocol0symm(I,R) { role I { fresh ni: Nonce; send_1(I,R, {I,ni}k(I,R) ); claim_i(I,Secret,ni); } role R { var ni: Nonce; recv_1(I,R, {I,ni}k(I,R) ); claim_r(R,Secret,ni); } }