diff --git a/spdl/speedtest.spdl b/spdl/speedtest.spdl new file mode 100644 index 0000000..bc8158f --- /dev/null +++ b/spdl/speedtest.spdl @@ -0,0 +1,49 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol ns3(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + read_2(R,I, {ni,nr}pk(I) ); + send_3(I,R, {nr}pk(R) ); + claim(I,nr); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + + read_1(I,R, {I,ni}pk(R) ); + send_2(R,I, {ni,nr}pk(I) ); + read_3(I,R, {nr}pk(R) ); + claim(I,ni); + } +} + +const Alice,Bob,Eve : Agent; + +/* something like this will later on all be implied by 'untrusted Eve' */ + +untrusted Eve; +const nc: Nonce; +compromised sk(Eve); + +/* pre-defined 10 runs, limit using --max-runs parameters */ + +run ns3.I(Alice,Bob); + run ns3.R(Alice,Bob); +run ns3.I(Alice,Eve); + run ns3.R(Eve,Bob); +run ns3.I(Bob,Alice); + run ns3.R(Bob,Alice); +run ns3.I(Bob,Eve); + run ns3.R(Eve,Alice); +run ns3.I(Alice,Alice); + run ns3.R(Bob,Bob);