diff --git a/spdl/ns3-brutus.spdl b/spdl/ns3-brutus.spdl index 9e48b00..2021fc0 100644 --- a/spdl/ns3-brutus.spdl +++ b/spdl/ns3-brutus.spdl @@ -12,7 +12,7 @@ protocol ns3(I,R) 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); + claim(I,Secret,nr); } role R @@ -23,7 +23,7 @@ protocol ns3(I,R) 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); + claim(I,Secret,ni); } } diff --git a/spdl/ns3-extreme.spdl b/spdl/ns3-extreme.spdl index bc8158f..1d760f9 100644 --- a/spdl/ns3-extreme.spdl +++ b/spdl/ns3-extreme.spdl @@ -12,7 +12,7 @@ protocol ns3(I,R) 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); + claim(I,Secret,nr); } role R @@ -23,7 +23,7 @@ protocol ns3(I,R) 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); + claim(I,Secret,ni); } } diff --git a/spdl/ns3-var.spdl b/spdl/ns3-var.spdl index 6fab576..1db4f8f 100644 --- a/spdl/ns3-var.spdl +++ b/spdl/ns3-var.spdl @@ -12,7 +12,7 @@ protocol ns3(I,R) 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,ni,nr); + claim(I,Secret,ni,nr); } role R @@ -23,7 +23,7 @@ protocol ns3(I,R) read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr}pk(I) ); read_3(I,R, {nr}pk(R) ); - claim(R,ni,nr); + claim(R,Secret,ni,nr); } } diff --git a/spdl/ns3.spdl b/spdl/ns3.spdl index fa77dd7..272d968 100644 --- a/spdl/ns3.spdl +++ b/spdl/ns3.spdl @@ -12,7 +12,7 @@ protocol ns3(I,R) 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,ni,nr); + claim(I,Secret,ni,nr); } role R @@ -23,7 +23,7 @@ protocol ns3(I,R) read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr}pk(I) ); read_3(I,R, {nr}pk(R) ); - claim(R,ni,nr); + claim(R,Secret,ni,nr); } } diff --git a/spdl/nsl3-var.spdl b/spdl/nsl3-var.spdl index 81b011f..e586431 100644 --- a/spdl/nsl3-var.spdl +++ b/spdl/nsl3-var.spdl @@ -12,7 +12,7 @@ protocol nsl3(I,R) 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(I,ni,nr); + claim(I,Secret,ni,nr); } role R @@ -23,7 +23,7 @@ protocol nsl3(I,R) 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(I,ni,nr); + claim(I,Secret,ni,nr); } } diff --git a/spdl/nsl3.spdl b/spdl/nsl3.spdl index 9178473..5176a4a 100644 --- a/spdl/nsl3.spdl +++ b/spdl/nsl3.spdl @@ -12,7 +12,7 @@ protocol nsl3(I,R) 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(I,ni,nr); + claim(I,Secret,ni,nr); } role R @@ -23,7 +23,7 @@ protocol nsl3(I,R) 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(I,ni,nr); + claim(I,Secret,ni,nr); } } diff --git a/spdl/nsl7.spdl b/spdl/nsl7.spdl index 3e74a72..3609e23 100644 --- a/spdl/nsl7.spdl +++ b/spdl/nsl7.spdl @@ -12,7 +12,7 @@ protocol nsl7(I,R) 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(I,nr,ni); + claim(I,Secret,nr,ni); } } diff --git a/spdl/otwayrees.spdl b/spdl/otwayrees.spdl index c5d8cbe..c91d277 100644 --- a/spdl/otwayrees.spdl +++ b/spdl/otwayrees.spdl @@ -16,7 +16,7 @@ protocol otwayrees(A,B,S) send_1(A,B, M,A,B, { na,M,A,B }k(A,S) ); read_4(B,A, M, { na,kab }k(A,S) ); - claim(A, kab); + claim(A, Secret,kab); } role B @@ -32,7 +32,7 @@ protocol otwayrees(A,B,S) read_3(S,B, M, t2, { nb,kab }k(B,S) ); send_4(B,A, M, t2 ); - claim(B, kab); + claim(B, Secret,kab); } role S diff --git a/spdl/tls-paulson.spdl b/spdl/tls-paulson.spdl index fe896b6..24064d1 100644 --- a/spdl/tls-paulson.spdl +++ b/spdl/tls-paulson.spdl @@ -34,7 +34,7 @@ protocol tlspaulson(a,b) send_7( a,b, { F }CLIENTK ); read_8( b,a, { F }SERVERK ); - claim(a, CLIENTK, SERVERK); + claim(a, Secret,CLIENTK, SERVERK); } @@ -55,7 +55,7 @@ protocol tlspaulson(a,b) read_7( a,b, { F }CLIENTK ); send_8( b,a, { F }SERVERK ); - claim(a, CLIENTK, SERVERK); + claim(a, Secret,CLIENTK, SERVERK); } } diff --git a/spdl/tmn.spdl b/spdl/tmn.spdl index 6e3c0d1..b2eb3e1 100644 --- a/spdl/tmn.spdl +++ b/spdl/tmn.spdl @@ -12,7 +12,7 @@ protocol tmn(A,B,S) send_1(A,S, B,{Ka}pk(S) ); read_4(S,A, B,{Kb}Ka ); - claim(A,Ka,Kb); + claim(A,Secret,Ka,Kb); } role B @@ -22,7 +22,7 @@ protocol tmn(A,B,S) read_2(S,B, A ); send_3(B,S, A, { Kb }pk(S) ); - claim(B,Kb); + claim(B,Secret,Kb); } role S @@ -34,7 +34,7 @@ protocol tmn(A,B,S) read_3(B,S, A, { Kb }pk(S) ); send_4(S,A, B,{Kb}Ka ); - //claim(S,Ka); + //claim(S,Secret,Ka); } } diff --git a/spdl/wmf-brutus.spdl b/spdl/wmf-brutus.spdl index 0b4f5ab..10f13fb 100644 --- a/spdl/wmf-brutus.spdl +++ b/spdl/wmf-brutus.spdl @@ -18,7 +18,7 @@ protocol wmfbrutus(A,B,S) read_2(S,B, { A, kab }k(B,S) ); - claim(B, kab); + claim(B, Secret,kab); } role S diff --git a/spdl/woolam-ce.spdl b/spdl/woolam-ce.spdl index a1c347a..1eb4dbe 100644 --- a/spdl/woolam-ce.spdl +++ b/spdl/woolam-ce.spdl @@ -28,7 +28,7 @@ protocol woolamce(A,B,S) send_6(B,A, { B,(Na,(Nb,Kab)) }Kas, { Na,Nb }Kab ); read_7(A,B, { Nb }Kab ); - claim(B,authToken); + claim(B,Secret,authToken); } } diff --git a/spdl/woolam-cmv.spdl b/spdl/woolam-cmv.spdl index 310bfe4..15fbec9 100644 --- a/spdl/woolam-cmv.spdl +++ b/spdl/woolam-cmv.spdl @@ -28,7 +28,7 @@ protocol woolamcmv(A,B,S) send_6(B,A, t2, { Na,Nb }Kab ); read_7(A,B, { Nb }Kab ); - claim(B,Kab,Nb,authToken); + claim(B,Secret,Kab,Nb,authToken); } } diff --git a/spdl/yahalom-ban.spdl b/spdl/yahalom-ban.spdl index 4e10602..17d407a 100644 --- a/spdl/yahalom-ban.spdl +++ b/spdl/yahalom-ban.spdl @@ -19,7 +19,7 @@ protocol yahalomBan(A,B,S) send_1(A,B, A,na); read_3(S,A, nb, {B,kab,na}k(A,S), ticket ); send_4(A,B, ticket, {nb}kab ); - claim(A, kab); + claim(A, Secret,kab); } role B @@ -32,7 +32,7 @@ protocol yahalomBan(A,B,S) read_1(A,B, A,na); send_2(B,S, B,nb, {A,na}k(B,S) ); read_4(A,B, {A,kab,nb}k(B,S) , {nb}kab ); - claim(B, kab); + claim(B, Secret,kab); } role S diff --git a/spdl/yahalom-lowe.spdl b/spdl/yahalom-lowe.spdl index 4dccd52..4590210 100644 --- a/spdl/yahalom-lowe.spdl +++ b/spdl/yahalom-lowe.spdl @@ -17,7 +17,7 @@ protocol yahalomlowe(A,B,S) send_1(A,B, A,na); read_3(S,A, {B,kab,na,nb}k(A,S) ); send_5(A,B, {A,B,S,nb}kab ); - claim(A, kab); + claim(A, Secret,kab); } role B @@ -30,7 +30,7 @@ protocol yahalomlowe(A,B,S) send_2(B,S, {A,na,nb}k(B,S) ); read_4(S,B, {A,kab}k(B,S) ); read_5(A,B, {A,B,S,nb}kab ); - claim(B, kab); + claim(B, Secret,kab); } role S diff --git a/spdl/yahalom.spdl b/spdl/yahalom.spdl index f7fd1fd..40bd3fb 100644 --- a/spdl/yahalom.spdl +++ b/spdl/yahalom.spdl @@ -16,7 +16,7 @@ protocol yahalom(A,B,S) send_1(A,B, A,na); read_3(S,A, nb, {B,kab,na,nb}k(A,S), ticket ); send_4(A,B, ticket, {nb}kab ); - claim(A, kab); + claim(A, Secret,kab); } role B @@ -29,7 +29,7 @@ protocol yahalom(A,B,S) read_1(A,B, A,na); send_2(B,S, B,nb, {A,na,nb}k(B,S) ); read_4(A,B, {A,kab}k(B,S) , {nb}kab ); - claim(B, kab); + claim(B, Secret,kab); } role S