diff --git a/spdl/tmn.spdl b/spdl/tmn.spdl index b2eb3e1..fb14a7a 100644 --- a/spdl/tmn.spdl +++ b/spdl/tmn.spdl @@ -1,3 +1,5 @@ +usertype Key; + const pk: Function; secret sk: Function; inversekeys(pk,sk); @@ -12,7 +14,7 @@ protocol tmn(A,B,S) send_1(A,S, B,{Ka}pk(S) ); read_4(S,A, B,{Kb}Ka ); - claim(A,Secret,Ka,Kb); + claim_5(A,Secret,Ka,Kb); } role B @@ -22,7 +24,7 @@ protocol tmn(A,B,S) read_2(S,B, A ); send_3(B,S, A, { Kb }pk(S) ); - claim(B,Secret,Kb); + claim_6(B,Secret,Kb); } role S @@ -34,12 +36,11 @@ protocol tmn(A,B,S) read_3(B,S, A, { Kb }pk(S) ); send_4(S,A, B,{Kb}Ka ); - //claim(S,Secret,Ka); + claim_7(S,Secret,Ka); } } -const Alice,Bob,Eve: Agent; -const Simon: Server; +const Alice,Bob,Eve,Simon: Agent; untrusted Eve; compromised sk(Eve);