# 1 "sts-modified.cpp" # 1 "" # 1 "sts-modified.cpp" # 17 "sts-modified.cpp" # 1 "common.h" 1 hashfunction prf, KDF; hashfunction g, h; # 94 "common.h" hashfunction MAC; protocol @oracle (DH, SWAP) { role DH { var i, r: Nonce; recv_!DH1( DH, DH, h(g(r),i) ); send_!DH2( DH, DH, h(g(i),r) ); } role SWAP { var i, r, Ni, Nr: Nonce; # 150 "common.h" recv_!SWAP1( SWAP, SWAP, KDF(h(g(r),i)) ); send_!SWAP2( SWAP, SWAP, KDF(h(g(i),r)) ); } } # 18 "sts-modified.cpp" 2 protocol sts-modified(I, R) { role I { fresh i: Nonce; var Gr: Ticket; send_1( I, R, g(i) ); recv_2( R, I, Gr, {Gr, g(i), I}sk(R) ); send_3( I, R, {g(i), Gr, R}sk(I) ); claim( I, SKR, KDF(h(Gr,i)) ); claim( I, Alive ); claim( I, Weakagree ); } role R { fresh r: Nonce; var Gi: Ticket; recv_1( I, R, Gi ); send_2( R, I, g(r), {g(r), Gi, I}sk(R) ); recv_3( I, R, {Gi, g(r), R}sk(I) ); claim( R, SKR, KDF(h(Gi,r)) ); claim( R, Alive ); claim( R, Weakagree ); } }