diff --git a/spdl/nsl3-niscynch-rep.spdl b/spdl/nsl3-niscynch-rep.spdl new file mode 100644 index 0000000..2baa020 --- /dev/null +++ b/spdl/nsl3-niscynch-rep.spdl @@ -0,0 +1,39 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol nsl3(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + read_2(R,I, {ni,nr,R}pk(I) ); + send_3(I,R, {nr}pk(R) ); + claim_4(I,Nisynch); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + + read_1(I,R, {I,ni}pk(R) ); + send_2(R,I, {ni,nr,R}pk(I) ); + read_3(I,R, {nr}pk(R) ); + claim_5(I,Nisynch); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const nc: Nonce; +compromised sk(Eve); + +run nsl3.I(Agent,Agent); +run nsl3.R(Agent,Agent); +run nsl3.I(Agent,Agent); +run nsl3.R(Agent,Agent);