diff --git a/spdl/tmn-Gijs.spdl b/spdl/tmn-Gijs.spdl new file mode 100644 index 0000000..b9179cf --- /dev/null +++ b/spdl/tmn-Gijs.spdl @@ -0,0 +1,56 @@ + +usertype Key; + +const pk: Function; +secret sk: Function; +inversekeys(pk,sk); + +protocol tmn(A,B,S) +{ + role A + { + const Ka: Key; + var Kb: Key; + + send_1(A,S, B,{Ka}pk(S) ); + read_4(S,A, B,{Kb}Ka ); + + #claim_5(A,Secret,Ka); + #claim_8(A,Secret,Kb); + } + + role B + { + const Kb: Key; + + read_2(S,B, A ); + send_3(B,S, A, { Kb }pk(S) ); + + claim_6(B,Secret,Kb); + } + + role S + { + var Ka,Kb: Key; + + read_1(A,S, B,{Ka}pk(S) ); + send_2(S,B, A ); + read_3(B,S, A, { Kb }pk(S) ); + send_4(S,A, B,{Kb}Ka ); + + #claim_7(S,Secret,Ka); + } +} + +const Alice,Bob,Eve,Simon: Agent; +const Ke: Key; + + +untrusted Eve; +compromised sk(Eve); + +# Scenario to recreate an attack in SPORE +run tmn.B (Alice,Bob,Simon); +run tmn.S (Alice,Bob,Simon); + +