From 49cd9b1271c79bcb507ca52a95d9b03e26b099f1 Mon Sep 17 00:00:00 2001 From: gijs Date: Wed, 29 Jun 2005 12:42:25 +0000 Subject: [PATCH] - Use variable type SessionKey every where instead of a combination between Key and SessionKey - Make KSL working again --- spdl/SPORE/ksl.spdl | 49 +++++++++++++++++---------------- spdl/SPORE/tmn.spdl | 15 +++++----- spdl/SPORE/wmf-lowe.spdl | 14 +++++----- spdl/SPORE/wmf.spdl | 14 +++++----- spdl/SPORE/woo-lam.spdl | 12 ++++---- spdl/SPORE/yahalom-ban.spdl | 10 +++---- spdl/SPORE/yahalom-lowe.spdl | 8 +++--- spdl/SPORE/yahalom-paulson.spdl | 10 +++---- spdl/SPORE/yahalom.spdl | 10 +++---- 9 files changed, 71 insertions(+), 71 deletions(-) diff --git a/spdl/SPORE/ksl.spdl b/spdl/SPORE/ksl.spdl index 77b162f..e2cde56 100644 --- a/spdl/SPORE/ksl.spdl +++ b/spdl/SPORE/ksl.spdl @@ -12,14 +12,15 @@ usertype Server, SessionKey, GeneralizedTimestamp, TicketKey; secret k: Function; -const Alice, Bob, Simon, Eve: Agent; +const a, b, e: Agent; +const s: Server; const Fresh: Function; const Compromised: Function; const ne: Nonce; const kee: SessionKey; -untrusted Eve; -compromised k(Eve,Simon); +untrusted e; +compromised k(e,s); protocol kslSessionKeyCompromise(C) { @@ -36,7 +37,7 @@ protocol kslSessionKeyCompromise(C) send_C2(C,C, (Ni,I), (Ni,I,Nr,R), {Nr,I,Kir}k(R,S),{Ni,R,Kir}k(I,S), - {Tr,I,Kir}Kbb,Nc,{Ni}Kir, + {Tr,I,Kir}Kbb,Nc,{Ni}k(I,R), {Nc}Kir, Ma, Mb,{Ma}Kir, @@ -50,34 +51,34 @@ protocol kslSessionKeyCompromise(C) } -protocol ksl(I,R,S) +protocol ksl(A,B,S) { - role I + role A { - const Ni, Mi: Nonce; - var Nr2, Mr: Nonce; + const Na, Ma: Nonce; + var Nc, Mb: Nonce; var T: Ticket; - var Kir: SessionKey; + var Kab: SessionKey; - send_1(I,R, Ni, I); - read_4(R,I, {Ni,R,Kir}k(I,S), T, Nr2, {Ni}Kir); - send_5(I,R, {Nr2}Kir ); + send_1(A,B, Na, A); + read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab ); + send_5(A,B, { Nc }Kab ); - send_6(I,R, Mi,T ); - read_7(R,I, Mr,{Mi}Kir ); - send_8(I,R, {Mr}Kir ); + send_6(A,B, Ma,T ); + read_7(B,A, Mb,{Ma}Kab ); + send_8(A,B, {Mb}Kab ); - claim_A1(A,Secret, Kab); - claim_A2(A,Niagree); - claim_A3(A,Nisynch); - claim_A4(A,Empty, (Fresh, Kab)); + claim_I1(A,Secret, Kab); + claim_I2(A,Niagree); + claim_I3(A,Nisynch); + claim_I4(A,Empty, (Fresh, Kab)); } role B { var Na,Ma: Nonce; - const Nr,Nr2,Mr: Nonce; - var Kir: SessionKey; + const Nb,Nc,Mb: Nonce; + var Kab: SessionKey; const Kbb: TicketKey; const Tb: GeneralizedTimestamp; var T: Ticket; @@ -108,7 +109,7 @@ protocol ksl(I,R,S) } } -run ksl.A(Alice,Bob,Simon); -run ksl.B(Alice,Bob,Simon); -run ksl.S(Alice,Bob,Simon); +run ksl.A(a,b,s); +run ksl.B(a,b,s); +run ksl.S(a,b,s); diff --git a/spdl/SPORE/tmn.spdl b/spdl/SPORE/tmn.spdl index ceb0f97..ad6b610 100644 --- a/spdl/SPORE/tmn.spdl +++ b/spdl/SPORE/tmn.spdl @@ -6,8 +6,7 @@ # Note: # According to Boyd and Mathuria Kb is the session key this is not clear # from the description in SPORE - -usertype Key; +usertype SessionKey; const pk: Function; secret sk: Function; @@ -21,7 +20,7 @@ protocol tmnSessionKeyCompromise(C) // corresponding session key to simulate key compromise role C { const Ni,Nr: Nonce; - const Kr,Ki: Key; + const Kr,Ki: SessionKey; var I,R,S: Agent; read_C1(C,C, I,R,S); @@ -38,8 +37,8 @@ protocol tmn(I,R,S) { role I { - const Ki: Key; - var Kr: Key; + const Ki: SessionKey; + var Kr: SessionKey; send_1(I,S, R,{Ki}pk(S) ); read_4(S,I, R,{Kr}Ki ); @@ -51,7 +50,7 @@ protocol tmn(I,R,S) role R { - const Kr: Key; + const Kr: SessionKey; read_2(S,R, I ); send_3(R,S, I, { Kr }pk(S) ); @@ -63,7 +62,7 @@ protocol tmn(I,R,S) role S { - var Ki,Kr: Key; + var Ki,Kr: SessionKey; read_1(I,S, R,{Ki}pk(S) ); send_2(S,R, I ); @@ -73,7 +72,7 @@ protocol tmn(I,R,S) } const Alice,Bob,Eve,Simon: Agent; -const Ke: Key; +const Ke: SessionKey; untrusted Eve; diff --git a/spdl/SPORE/wmf-lowe.spdl b/spdl/SPORE/wmf-lowe.spdl index 7866319..3c65ec4 100644 --- a/spdl/SPORE/wmf-lowe.spdl +++ b/spdl/SPORE/wmf-lowe.spdl @@ -9,7 +9,7 @@ # agent can recognise and will reject to read messages that it has created # itself. -usertype Key; +usertype SessionKey; usertype TimeStamp; const succ,pred: Function; inversekeys (succ,pred); @@ -24,7 +24,7 @@ protocol wmfLoweSessionKeyCompromise(C) // corresponding session key to simulate key compromise role C { const Ni,Nr: Nonce; - const Kir: Key; + const Kir: SessionKey; const Ti,Ts: TimeStamp; var I,R,S: Agent; @@ -43,9 +43,9 @@ protocol wmfLowe(I,R,S) { role I { - const Kir: Key; + const Kir: SessionKey; const Ti: TimeStamp; - var Kr: Key; + var Kr: SessionKey; var Nr: Nonce; send_1(I,S, I, {Ti, R, Kir}k(I,S)); @@ -60,7 +60,7 @@ protocol wmfLowe(I,R,S) role R { var Ts: TimeStamp; - var Kir: Key; + var Kir: SessionKey; const Nr: Nonce; read_2(S,R, {Ts, I, Kir}k(R,S) ); @@ -74,7 +74,7 @@ protocol wmfLowe(I,R,S) role S { - var Kir: Key; + var Kir: SessionKey; const Ts: TimeStamp; var Ti: TimeStamp; @@ -84,7 +84,7 @@ protocol wmfLowe(I,R,S) } const Alice,Bob,Eve,Simon: Agent; -const Ke: Key; +const Ke: SessionKey; const Te: TimeStamp; diff --git a/spdl/SPORE/wmf.spdl b/spdl/SPORE/wmf.spdl index 6a56f5c..ce16afa 100644 --- a/spdl/SPORE/wmf.spdl +++ b/spdl/SPORE/wmf.spdl @@ -4,7 +4,7 @@ # http://www.lsv.ens-cachan.fr/spore/wideMouthedFrog.html # -usertype Key; +usertype SessionKey; usertype TimeStamp; secret k: Function; @@ -17,7 +17,7 @@ protocol wmfSessionKeyCompromise(C) // corresponding session key to simulate key compromise role C { const Ni,Nr: Nonce; - const Kir: Key; + const Kir: SessionKey; const Ti,Ts: TimeStamp; var I,R,S: Agent; @@ -34,9 +34,9 @@ protocol wmf(I,R,S) { role I { - const Kir: Key; + const Kir: SessionKey; const Ti: TimeStamp; - var Kr: Key; + var Kr: SessionKey; send_1(I,S, I, {Ti, R, Kir}k(I,S)); @@ -47,7 +47,7 @@ protocol wmf(I,R,S) role R { var Ts: TimeStamp; - var Kir: Key; + var Kir: SessionKey; read_2(S,R, {Ts, I, Kir}k(R,S) ); @@ -58,7 +58,7 @@ protocol wmf(I,R,S) role S { - var Kir: Key; + var Kir: SessionKey; const Ts: TimeStamp; var Ti: TimeStamp; @@ -68,7 +68,7 @@ protocol wmf(I,R,S) } const Alice,Bob,Eve,Simon: Agent; -const Ke: Key; +const Ke: SessionKey; const Te: TimeStamp; diff --git a/spdl/SPORE/woo-lam.spdl b/spdl/SPORE/woo-lam.spdl index 91ab8ed..d4d3b60 100644 --- a/spdl/SPORE/woo-lam.spdl +++ b/spdl/SPORE/woo-lam.spdl @@ -9,7 +9,7 @@ # -usertype Key; +usertype SessionKey; secret k: Function; const Fresh: Function; @@ -21,7 +21,7 @@ protocol woolamSessionKeyCompromise(C) // corresponding session key to simulate key compromise role C { const N1,N2: Nonce; - const Kir: Key; + const Kir: SessionKey; var I,R,S: Agent; read_C1(C,C, I,R,S); @@ -44,7 +44,7 @@ protocol woolam(I,R,S) role I { const N1: Nonce; - var Kir: Key; + var Kir: SessionKey; var N2: Nonce; send_1(I,R, I, N1); @@ -63,7 +63,7 @@ protocol woolam(I,R,S) { const N2: Nonce; var N1: Nonce; - var Kir: Key; + var Kir: SessionKey; var T1,T2: Ticket; read_1(I,R, I, N1); @@ -81,7 +81,7 @@ protocol woolam(I,R,S) role S { - const Kir: Key; + const Kir: SessionKey; var N1,N2: Nonce; read_4(R,S, {I, R, N1, N2}k(I,S), {I, R, N1, N2}k(R,S)); @@ -90,7 +90,7 @@ protocol woolam(I,R,S) } const Alice,Bob,Eve,Simon: Agent; -const Ke: Key; +const Ke: SessionKey; const Te: Ticket; const Ne: Nonce; diff --git a/spdl/SPORE/yahalom-ban.spdl b/spdl/SPORE/yahalom-ban.spdl index 3ea7cbe..98eefde 100644 --- a/spdl/SPORE/yahalom-ban.spdl +++ b/spdl/SPORE/yahalom-ban.spdl @@ -10,7 +10,7 @@ secret k : Function; -usertype Key; +usertype SessionKey; const Fresh: Function; const Compromised: Function; @@ -20,7 +20,7 @@ protocol yahalomBANSessionKeyCompromise(C) // corresponding session key to simulate key compromise role C { const Ni,Nr: Nonce; - const Kir: Key; + const Kir: SessionKey; var I,R,S: Agent; read_C1(C,C, I,R,S); @@ -44,7 +44,7 @@ protocol yahalomBAN(I,R,S) const Ni: Nonce; var Nr: Nonce; var T: Ticket; - var Kir: Key; + var Kir: SessionKey; send_1(I,R, I,Ni); read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T ); @@ -60,7 +60,7 @@ protocol yahalomBAN(I,R,S) const Nr: Nonce; var Ni: Nonce; var T: Ticket; - var Kir: Key; + var Kir: SessionKey; read_1(I,R, I,Ni); send_2(R,S, R, Nr, {I,Ni}k(R,S) ); @@ -73,7 +73,7 @@ protocol yahalomBAN(I,R,S) role S { - const Kir: Key; + const Kir: SessionKey; var Ni,Nr: Nonce; read_2(R,S, R, Nr, {I,Ni}k(R,S) ); diff --git a/spdl/SPORE/yahalom-lowe.spdl b/spdl/SPORE/yahalom-lowe.spdl index 65790f9..fe9341d 100644 --- a/spdl/SPORE/yahalom-lowe.spdl +++ b/spdl/SPORE/yahalom-lowe.spdl @@ -7,7 +7,7 @@ secret k : Function; -usertype Key; +usertype SessionKey; protocol yahalomLowe(I,R,S) @@ -16,7 +16,7 @@ protocol yahalomLowe(I,R,S) { const Ni: Nonce; var Nr: Nonce; - var Kir: Key; + var Kir: SessionKey; send_1(I,R, I,Ni); read_3(S,I, {R,Kir,Ni,Nr}k(I,S) ); @@ -30,7 +30,7 @@ protocol yahalomLowe(I,R,S) { const Nr: Nonce; var Ni: Nonce; - var Kir: Key; + var Kir: SessionKey; read_1(I,R, I,Ni); send_2(R,S, {I,Ni,Nr}k(R,S) ); @@ -43,7 +43,7 @@ protocol yahalomLowe(I,R,S) role S { - const Kir: Key; + const Kir: SessionKey; var Ni,Nr: Nonce; read_2(R,S, {I,Ni,Nr}k(R,S) ); diff --git a/spdl/SPORE/yahalom-paulson.spdl b/spdl/SPORE/yahalom-paulson.spdl index 0930891..5b122e0 100644 --- a/spdl/SPORE/yahalom-paulson.spdl +++ b/spdl/SPORE/yahalom-paulson.spdl @@ -12,7 +12,7 @@ secret k : Function; const Fresh: Function; const Compromised: Function; -usertype Key; +usertype SessionKey; protocol yahalomPaulsonSessionKeyCompromise(C) { @@ -20,7 +20,7 @@ protocol yahalomPaulsonSessionKeyCompromise(C) // corresponding session key to simulate key compromise role C { const Ni,Nr: Nonce; - const Kir: Key; + const Kir: SessionKey; var I,R,S: Agent; read_C1(C,C, I,R,S); @@ -43,7 +43,7 @@ protocol yahalomPaulson(I,R,S) const Ni: Nonce; var Nr: Nonce; var T: Ticket; - var Kir: Key; + var Kir: SessionKey; send_1(I,R, I,Ni); read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T ); @@ -59,7 +59,7 @@ protocol yahalomPaulson(I,R,S) const Nr: Nonce; var Ni: Nonce; var T: Ticket; - var Kir: Key; + var Kir: SessionKey; read_1(I,R, I,Ni); send_2(R,S, R, Nr, {I,Ni}k(R,S) ); @@ -72,7 +72,7 @@ protocol yahalomPaulson(I,R,S) role S { - const Kir: Key; + const Kir: SessionKey; var Ni,Nr: Nonce; read_2(R,S, R, Nr, {I,Ni}k(R,S) ); diff --git a/spdl/SPORE/yahalom.spdl b/spdl/SPORE/yahalom.spdl index 3a3d37e..1a181ed 100644 --- a/spdl/SPORE/yahalom.spdl +++ b/spdl/SPORE/yahalom.spdl @@ -10,7 +10,7 @@ secret k : Function; -usertype Key; +usertype SessionKey; const Fresh: Function; const Compromised: Function; @@ -20,7 +20,7 @@ protocol yahalomSessionKeyCompromise(C) // corresponding session key to simulate key compromise role C { const Ni,Nr: Nonce; - const Kir: Key; + const Kir: SessionKey; var I,R,S: Agent; read_C1(C,C, I,R,S); @@ -43,7 +43,7 @@ protocol yahalom(I,R,S) const Ni: Nonce; var Nr: Nonce; var T: Ticket; - var Kir: Key; + var Kir: SessionKey; send_1(I,R, I,Ni); read_3(S,I, {R,Kir,Ni,Nr}k(I,S), T ); @@ -59,7 +59,7 @@ protocol yahalom(I,R,S) const Nr: Nonce; var Ni: Nonce; var T: Ticket; - var Kir: Key; + var Kir: SessionKey; read_1(I,R, I,Ni); send_2(R,S, R, {I,Ni,Nr}k(R,S) ); @@ -72,7 +72,7 @@ protocol yahalom(I,R,S) role S { - const Kir: Key; + const Kir: SessionKey; var Ni,Nr: Nonce; read_2(R,S, R, {I,Ni,Nr}k(R,S) );