From 44bc36edc5dff2f6791f5d0651337367449abd52 Mon Sep 17 00:00:00 2001 From: gijs Date: Fri, 12 Aug 2005 11:55:24 +0000 Subject: [PATCH] - Add @ to swapkey, to disable it in classification - Modify key Compromise for protocols that contain a timestamp to make the key compromise disclose a timestamp with a different type, namely ExpiredTimeStamp so that they will not be accepted as timestamps in a new session, thereby simulating that they are expired. --- spdl/SPORE/andrew-ban-concrete.spdl | 2 +- spdl/SPORE/denning-sacco-lowe.spdl | 3 ++- spdl/SPORE/denning-sacco.spdl | 3 ++- spdl/SPORE/kaochow-v3.spdl | 7 ++++--- spdl/SPORE/ksl-lowe.spdl | 7 ++++--- spdl/SPORE/ksl.spdl | 7 ++++--- spdl/SPORE/neumannstub-hwang.spdl | 3 ++- spdl/SPORE/neumannstub.spdl | 6 +++--- spdl/SPORE/wmf-lowe.spdl | 3 ++- 9 files changed, 24 insertions(+), 17 deletions(-) diff --git a/spdl/SPORE/andrew-ban-concrete.spdl b/spdl/SPORE/andrew-ban-concrete.spdl index 6f46a3a..da0c80b 100644 --- a/spdl/SPORE/andrew-ban-concrete.spdl +++ b/spdl/SPORE/andrew-ban-concrete.spdl @@ -21,7 +21,7 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol swapkey(X) +protocol @swapkey(X) { # Protocol added to work around the symmetry problems where k(I,R) != k(R,I) role X diff --git a/spdl/SPORE/denning-sacco-lowe.spdl b/spdl/SPORE/denning-sacco-lowe.spdl index 66c8875..7d4f2f4 100644 --- a/spdl/SPORE/denning-sacco-lowe.spdl +++ b/spdl/SPORE/denning-sacco-lowe.spdl @@ -14,6 +14,7 @@ usertype Key; usertype SessionKey; usertype TimeStamp; +usertype ExpiredTimeStamp; secret k: Function; usertype PseudoFunction; const dec: PseudoFunction; @@ -27,7 +28,7 @@ protocol denningSaccoLoweSessionKeyCompromise(C) role C { const Ni,Nr: Nonce; const Kir: SessionKey; - const T: TimeStamp; + const T: ExpiredTimeStamp; var I,R,S: Agent; read_C1(C,C, I,R,S); diff --git a/spdl/SPORE/denning-sacco.spdl b/spdl/SPORE/denning-sacco.spdl index 5aca4cd..8eabe4c 100644 --- a/spdl/SPORE/denning-sacco.spdl +++ b/spdl/SPORE/denning-sacco.spdl @@ -11,6 +11,7 @@ usertype Key; usertype SessionKey; usertype TimeStamp; +usertype ExpiredTimeStamp; secret k: Function; const Fresh: Function; const Compromised: Function; @@ -22,7 +23,7 @@ protocol denningSaccoSessionKeyCompromise(C) role C { const Ni,Nr: Nonce; const Kir: SessionKey; - const T: TimeStamp; + const T: ExpiredTimeStamp; var I,R,S: Agent; read_C1(C,C, I,R,S); diff --git a/spdl/SPORE/kaochow-v3.spdl b/spdl/SPORE/kaochow-v3.spdl index 640e214..285782a 100644 --- a/spdl/SPORE/kaochow-v3.spdl +++ b/spdl/SPORE/kaochow-v3.spdl @@ -9,7 +9,8 @@ # usertype SessionKey; -usertype Timestamp; +usertype ExpiredTimeStamp; +usertype TimeStamp; secret k: Function; const Fresh: Function; const Compromised: Function; @@ -21,7 +22,7 @@ protocol kaochow3SessionKeyCompromise(C) role C { const Ni,Nr: Nonce; const Kir,Kt: SessionKey; - const T2: Timestamp; + const T2: ExpiredTimeStamp; var I,R,S: Agent; read_C1(C,C, I,R,S); @@ -65,7 +66,7 @@ protocol kaochow3(I,R,S) const nr: Nonce; var kir,kt: SessionKey; var T: Ticket; - const tr: Timestamp; + const tr: TimeStamp; read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); send_3 (R,I, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) ); diff --git a/spdl/SPORE/ksl-lowe.spdl b/spdl/SPORE/ksl-lowe.spdl index 5aae028..c9aca4b 100644 --- a/spdl/SPORE/ksl-lowe.spdl +++ b/spdl/SPORE/ksl-lowe.spdl @@ -11,7 +11,8 @@ # According to SPORE there are no attacks on this protocol, scyther # finds one however. This has to be investigated further. -usertype Server, SessionKey, GeneralizedTimestamp, TicketKey; +usertype Server, SessionKey, TimeStamp, TicketKey; +usertype ExpiredTimeStamp; secret k: Function; const a, b, e: Agent; @@ -33,7 +34,7 @@ protocol kslLoweSessionKeyCompromise(C) const Ni,Nr,Nc,Ma,Mb: Nonce; const Kir: SessionKey; const Kbb: TicketKey; - const Tr: GeneralizedTimestamp; + const Tr: ExpiredTimeStamp; var I,R,S: Agent; read_C1(C,C, I,R,S); @@ -82,7 +83,7 @@ protocol kslLowe(A,B,S) const Nb,Nc,Mb: Nonce; var Kab: SessionKey; const Kbb: TicketKey; - const Tb: GeneralizedTimestamp; + const Tb: TimeStamp; var T: Ticket; read_1(A,B, Na, A); diff --git a/spdl/SPORE/ksl.spdl b/spdl/SPORE/ksl.spdl index e2cde56..9fa728a 100644 --- a/spdl/SPORE/ksl.spdl +++ b/spdl/SPORE/ksl.spdl @@ -9,7 +9,8 @@ # -usertype Server, SessionKey, GeneralizedTimestamp, TicketKey; +usertype Server, SessionKey, TimeStamp, TicketKey; +usertype ExpiredTimeStamp; secret k: Function; const a, b, e: Agent; @@ -30,7 +31,7 @@ protocol kslSessionKeyCompromise(C) const Ni,Nr,Nc,Ma,Mb: Nonce; const Kir: SessionKey; const Kbb: TicketKey; - const Tr: GeneralizedTimestamp; + const Tr: ExpiredTimeStamp; var I,R,S: Agent; read_C1(C,C, I,R,S); @@ -80,7 +81,7 @@ protocol ksl(A,B,S) const Nb,Nc,Mb: Nonce; var Kab: SessionKey; const Kbb: TicketKey; - const Tb: GeneralizedTimestamp; + const Tb: TimeStamp; var T: Ticket; read_1(A,B, Na, A); diff --git a/spdl/SPORE/neumannstub-hwang.spdl b/spdl/SPORE/neumannstub-hwang.spdl index 4685d36..030627f 100644 --- a/spdl/SPORE/neumannstub-hwang.spdl +++ b/spdl/SPORE/neumannstub-hwang.spdl @@ -13,6 +13,7 @@ usertype Server, SessionKey, TimeStamp, TicketKey; +usertype ExpiredTimeStamp; secret k: Function; const a, b, e: Agent; @@ -32,7 +33,7 @@ protocol neustubHwangSessionKeyCompromise(C) role C { const Ni,Nr,Mi,Mr: Nonce; const Kir: SessionKey; - const Tr: TimeStamp; + const Tr: ExpiredTimeStamp; var I,R,S: Agent; read_C1(C,C, I,R,S); diff --git a/spdl/SPORE/neumannstub.spdl b/spdl/SPORE/neumannstub.spdl index 86b92eb..cf92db7 100644 --- a/spdl/SPORE/neumannstub.spdl +++ b/spdl/SPORE/neumannstub.spdl @@ -12,8 +12,8 @@ # different protocols (the key establishment protocol and the repeated # authentication protocol) - usertype Server, SessionKey, TimeStamp, TicketKey; +usertype ExpiredTimeStamp; secret k: Function; const Alice, Bob, Simon, Eve: Agent; @@ -32,7 +32,7 @@ protocol neustubSessionKeyCompromise(C) role C { const Ni,Nr,Mi,Mr: Nonce; const Kir: SessionKey; - const Tr: TimeStamp; + const Tr: ExpiredTimeStamp; var I,R,S: Agent; read_C1(C,C, I,R,S); @@ -50,7 +50,7 @@ protocol neustubSessionKeyCompromise(C) } } -protocol neustubRepeat(I,R,S) +protocol @neustubRepeat(I,R,S) { const Kir: SessionKey; diff --git a/spdl/SPORE/wmf-lowe.spdl b/spdl/SPORE/wmf-lowe.spdl index 58bc0a5..b66a5f9 100644 --- a/spdl/SPORE/wmf-lowe.spdl +++ b/spdl/SPORE/wmf-lowe.spdl @@ -11,6 +11,7 @@ usertype SessionKey; usertype TimeStamp; +usertype ExpiredTimeStamp; const succ,pred: Function; inversekeys (succ,pred); const Fresh: Function; @@ -25,7 +26,7 @@ protocol wmfLoweSessionKeyCompromise(C) role C { const Ni,Nr: Nonce; const Kir: SessionKey; - const Ti,Ts: TimeStamp; + const Ti,Ts: ExpiredTimeStamp; var I,R,S: Agent; read_C1(C,C, I,R,S);