From 6fb6aa33dd17616cd7c510b014cd4f3cac817509 Mon Sep 17 00:00:00 2001 From: gijs Date: Fri, 24 Jun 2005 10:53:15 +0000 Subject: [PATCH] - Add session compromise to all protocols that establish a session key --- spdl/SPORE/andrew-ban-concrete.spdl | 23 ++++++++++++ spdl/SPORE/andrew-ban.spdl | 21 +++++++++++ spdl/SPORE/andrew-lowe-ban.spdl | 21 +++++++++++ spdl/SPORE/andrew.spdl | 21 +++++++++++ spdl/SPORE/denning-sacco-lowe.spdl | 23 ++++++++++++ spdl/SPORE/denning-sacco.spdl | 21 +++++++++++ spdl/SPORE/kaochow-v2.spdl | 34 +++++++++++++++--- spdl/SPORE/kaochow-v3.spdl | 41 ++++++++++++++++++---- spdl/SPORE/kaochow.spdl | 32 ++++++++++++++--- spdl/SPORE/ksl-lowe.spdl | 29 +++++++++++++++ spdl/SPORE/ksl.spdl | 30 ++++++++++++++++ spdl/SPORE/needham-schroeder-sk-amend.spdl | 24 +++++++++++++ spdl/SPORE/needham-schroeder-sk.spdl | 22 ++++++++++++ spdl/SPORE/neumannstub-hwang.spdl | 26 ++++++++++++++ spdl/SPORE/neumannstub.spdl | 26 ++++++++++++++ spdl/SPORE/otwayrees.spdl | 21 +++++++++++ spdl/SPORE/tmn.spdl | 20 +++++++++++ spdl/SPORE/wmf-lowe.spdl | 22 ++++++++++++ spdl/SPORE/wmf.spdl | 20 +++++++++++ spdl/SPORE/woo-lam.spdl | 25 +++++++++++++ spdl/SPORE/yahalom-ban.spdl | 23 ++++++++++++ spdl/SPORE/yahalom-paulson.spdl | 22 ++++++++++++ spdl/SPORE/yahalom.spdl | 22 ++++++++++++ 23 files changed, 552 insertions(+), 17 deletions(-) diff --git a/spdl/SPORE/andrew-ban-concrete.spdl b/spdl/SPORE/andrew-ban-concrete.spdl index 91f95ea..6f46a3a 100644 --- a/spdl/SPORE/andrew-ban-concrete.spdl +++ b/spdl/SPORE/andrew-ban-concrete.spdl @@ -19,6 +19,7 @@ usertype SessionKey; secret k: Function; const Fresh: Function; +const Compromised: Function; protocol swapkey(X) { @@ -31,6 +32,28 @@ protocol swapkey(X) send_X2(X,X,{T}k(R,I)); } } + +protocol andrewConcreteSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const ni,nr: Nonce; + const kir: SessionKey; + var I,R: Agent; + + read_C1(C,C, I,R); + send_C2(C,C, (I,ni), + {ni,kir}k(I,R), + {ni}kir, + nr, + kir + ); + claim_C3(C,Empty, (Compromised,kir)); + } +} + + protocol andrewConcrete(I,R) { diff --git a/spdl/SPORE/andrew-ban.spdl b/spdl/SPORE/andrew-ban.spdl index ad11d78..b1538ec 100644 --- a/spdl/SPORE/andrew-ban.spdl +++ b/spdl/SPORE/andrew-ban.spdl @@ -14,6 +14,27 @@ usertype SessionKey; secret k: Function; const Fresh: Function; +const Compromised: Function; + +protocol andrewBanSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const ni,nr,nr2: Nonce; + const kir: SessionKey; + var I,R: Agent; + + read_C1(C,C, I,R); + send_C2(C,C, (I,{ni}k(I,R)), + {ni,nr}k(I,R), + {nr}k(I,R), + {kir,nr2,ni}k(I,R), + kir + ); + claim_C3(C,Empty, (Compromised,kir)); + } +} protocol andrewBan(I,R) { diff --git a/spdl/SPORE/andrew-lowe-ban.spdl b/spdl/SPORE/andrew-lowe-ban.spdl index c183ef4..3e4fdb8 100644 --- a/spdl/SPORE/andrew-lowe-ban.spdl +++ b/spdl/SPORE/andrew-lowe-ban.spdl @@ -21,6 +21,27 @@ usertype SessionKey; secret k: Function; const Fresh: Function; +const Compromised: Function; + +protocol andrewLoweBanSessionKeyCompromise(C) +{ + // Read the names of 2 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const ni,nr: Nonce; + const kir: SessionKey; + var I,R: Agent; + + read_C1(C,C, I,R); + send_C2(C,C, (I,ni), + {ni,kir,R}k(I,R), + {ni}kir, + nr, + kir + ); + claim_C3(C,Empty, (Compromised,kir)); + } +} protocol andrewLoweBan(I,R) { diff --git a/spdl/SPORE/andrew.spdl b/spdl/SPORE/andrew.spdl index abaad45..0fd4191 100644 --- a/spdl/SPORE/andrew.spdl +++ b/spdl/SPORE/andrew.spdl @@ -13,6 +13,27 @@ usertype SessionKey; secret k: Function; const succ: Function; const Fresh: Function; +const Compromised: Function; + +protocol andrewSessionKeyCompromise(C) +{ + // Read the names of 2 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const ni,nr,nr2: Nonce; + const kir: SessionKey; + var I,R: Agent; + + read_C1(C,C, I,R); + send_C2(C,C, (I,{ni}k(I,R)), + {succ(ni),nr}k(I,R), + {succ(nr)}k(I,R), + {kir,nr2}k(I,R), + kir + ); + claim_C3(C,Empty, (Compromised,kir)); + } +} protocol andrew(I,R) { diff --git a/spdl/SPORE/denning-sacco-lowe.spdl b/spdl/SPORE/denning-sacco-lowe.spdl index ccd4181..66c8875 100644 --- a/spdl/SPORE/denning-sacco-lowe.spdl +++ b/spdl/SPORE/denning-sacco-lowe.spdl @@ -18,6 +18,29 @@ secret k: Function; usertype PseudoFunction; const dec: PseudoFunction; const Fresh: Function; +const Compromised: Function; + +protocol denningSaccoLoweSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + const T: TimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R), + {R,Kir,T,{Kir,I,T}k(R,S)}k(I,S), + {Kir,I,T}k(R,S), + {Nr}Kir, + {{Nr}dec}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} protocol denningSaccoLowe(I,R,S) { diff --git a/spdl/SPORE/denning-sacco.spdl b/spdl/SPORE/denning-sacco.spdl index c489434..de96c8a 100644 --- a/spdl/SPORE/denning-sacco.spdl +++ b/spdl/SPORE/denning-sacco.spdl @@ -13,6 +13,27 @@ usertype SessionKey; usertype TimeStamp; secret k: Function; const Fresh: Function; +const Compromised: Function; + +protocol denningSaccoSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + const T: Ticket; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R), + {R,Kir,T,{Kir,I,T}k(R,S)}k(I,S), + {Kir,I,T}k(R,S), + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} protocol denningSacco(I,R,S) { diff --git a/spdl/SPORE/kaochow-v2.spdl b/spdl/SPORE/kaochow-v2.spdl index cd44372..d81823d 100644 --- a/spdl/SPORE/kaochow-v2.spdl +++ b/spdl/SPORE/kaochow-v2.spdl @@ -8,9 +8,33 @@ # the protocol using the ARACHNE engine (-a) # -usertype Sessionkey; +usertype SessionKey; secret k: Function; const Fresh: Function; +const Compromised: Function; + +protocol kaochow2SessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir,Kt: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R,Ni), + {I,R,Ni,Kir,Kt}k(I,S), + {I,R,Ni,Kir,Kt}k(R,S), + R, Nr, + {Nr,Kir}Kt, + Kir, + Kt + ); + claim_C3(C,Empty, (Compromised,Kir)); + claim_C4(C,Empty, (Compromised,Kt)); + } +} protocol kaochow2(I,R,S) { @@ -18,7 +42,7 @@ protocol kaochow2(I,R,S) { const ni: Nonce; var nr: Nonce; - var kir,kt: Sessionkey; + var kir,kt: SessionKey; send_1 (I,S, I,R,ni); read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr ); @@ -34,7 +58,7 @@ protocol kaochow2(I,R,S) { var ni: Nonce; const nr: Nonce; - var kir,kt: Sessionkey; + var kir,kt: SessionKey; var T: Ticket; read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); @@ -50,7 +74,7 @@ protocol kaochow2(I,R,S) role S { var ni: Nonce; - const kir, kt: Sessionkey; + const kir, kt: SessionKey; read_1 (I,S, I,R,ni); send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); @@ -62,7 +86,7 @@ const Alice,Bob,Simon,Eve: Agent; untrusted Eve; const ne: Nonce; const te: Ticket; -const ke: Sessionkey; +const ke: SessionKey; compromised k(Eve,Eve); compromised k(Eve,Alice); compromised k(Eve,Bob); diff --git a/spdl/SPORE/kaochow-v3.spdl b/spdl/SPORE/kaochow-v3.spdl index ef2329e..7fd50b9 100644 --- a/spdl/SPORE/kaochow-v3.spdl +++ b/spdl/SPORE/kaochow-v3.spdl @@ -8,10 +8,37 @@ # the protocol using the ARACHNE engine (-a) # -usertype Sessionkey; +usertype SessionKey; usertype Timestamp; secret k: Function; const Fresh: Function; +const Compromised: Function; + +protocol kaochow3SessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir,Kt: SessionKey; + const T2: Timestamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R,Ni), + {I,R,Ni,Kir,Kt}k(I,S), + {I,R,Ni,Kir,Kt}k(R,S), + {Ni,Kir}Kt, + Nr, + {I,R,T2,Kir}k(R,S), + {Nr,Kir}Kt, + Kir, + Kt + ); + claim_C3(C,Empty, (Compromised,Kir)); + claim_C4(C,Empty, (Compromised,Kt)); + } +} protocol kaochow3(I,R,S) { @@ -19,11 +46,11 @@ protocol kaochow3(I,R,S) { const ni: Nonce; var nr: Nonce; - var kir,kt: Sessionkey; + var kir,kt: SessionKey; var T2: Ticket; send_1 (I,S, I,R,ni); - read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 ); + read_3 (R,I, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 ); send_4 (I,R, {nr,kir}kt, T2 ); claim_I1 (I, Nisynch); @@ -36,12 +63,12 @@ protocol kaochow3(I,R,S) { var ni: Nonce; const nr: Nonce; - var kir,kt: Sessionkey; + var kir,kt: SessionKey; var T: Ticket; const tr: Timestamp; read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); - send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) ); + send_3 (R,I, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) ); read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) ); claim_R1 (R, Nisynch); @@ -53,7 +80,7 @@ protocol kaochow3(I,R,S) role S { var ni: Nonce; - const kir, kt: Sessionkey; + const kir, kt: SessionKey; read_1 (I,S, I,R,ni); send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); @@ -65,7 +92,7 @@ const Alice,Bob,Simon,Eve: Agent; untrusted Eve; const ne: Nonce; const te: Ticket; -const ke: Sessionkey; +const ke: SessionKey; compromised k(Eve,Eve); compromised k(Eve,Alice); compromised k(Eve,Bob); diff --git a/spdl/SPORE/kaochow.spdl b/spdl/SPORE/kaochow.spdl index c50147e..2822d5e 100644 --- a/spdl/SPORE/kaochow.spdl +++ b/spdl/SPORE/kaochow.spdl @@ -8,9 +8,31 @@ # the protocol using the ARACHNE engine (-a) # -usertype Sessionkey; +usertype SessionKey; secret k: Function; const Fresh: Function; +const Compromised: Function; + +protocol kaochowSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R,Ni), + {I,R,Ni,Kir}k(I,S), + {I,R,Ni,Kir}k(R,S), + {Ni}Kir, Nr, + {Nr}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} protocol kaochow(I,R,S) { @@ -18,7 +40,7 @@ protocol kaochow(I,R,S) { const ni: Nonce; var nr: Nonce; - var kir: Sessionkey; + var kir: SessionKey; send_1 (I,S, I,R,ni); read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr ); @@ -34,7 +56,7 @@ protocol kaochow(I,R,S) { var ni: Nonce; const nr: Nonce; - var kir: Sessionkey; + var kir: SessionKey; var T; read_2 (S,R, T, { I,R,ni,kir }k(R,S) ); @@ -50,7 +72,7 @@ protocol kaochow(I,R,S) role S { var ni: Nonce; - const kir: Sessionkey; + const kir: SessionKey; read_1 (I,S, I,R,ni); send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) ); @@ -62,7 +84,7 @@ const Alice,Bob,Simon,Eve: Agent; untrusted Eve; const ne: Nonce; const te: Ticket; -const ke: Sessionkey; +const ke: SessionKey; compromised k(Eve,Eve); compromised k(Eve,Alice); compromised k(Eve,Bob); diff --git a/spdl/SPORE/ksl-lowe.spdl b/spdl/SPORE/ksl-lowe.spdl index 463f79e..5aae028 100644 --- a/spdl/SPORE/ksl-lowe.spdl +++ b/spdl/SPORE/ksl-lowe.spdl @@ -17,6 +17,7 @@ secret k: Function; const a, b, e: Agent; const s: Server; const Fresh: Function; +const Compromised: Function; const ne: Nonce; @@ -24,6 +25,34 @@ const kee: SessionKey; untrusted e; compromised k(e,s); +protocol kslLoweSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr,Nc,Ma,Mb: Nonce; + const Kir: SessionKey; + const Kbb: TicketKey; + const Tr: GeneralizedTimestamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (Ni,I), + (Ni,I,Nr,R), + {I,Nr,Kir}k(R,S),{Ni,R,Kir}k(I,S), + {Tr,I,Kir}Kbb,Nc,{R,Ni}k(I,R), + {Nc}Kir, + Ma, + Mb,{Ma,R}Kir, + {I,Mb}Kir, + Kir, + Kbb + ); + claim_C3(C,Empty, (Compromised,Kir)); + claim_C4(C,Empty, (Compromised,Kbb)); + } +} + protocol kslLowe(A,B,S) { role A diff --git a/spdl/SPORE/ksl.spdl b/spdl/SPORE/ksl.spdl index dbd73cc..e15be0b 100644 --- a/spdl/SPORE/ksl.spdl +++ b/spdl/SPORE/ksl.spdl @@ -15,12 +15,42 @@ secret k: Function; const a, b, e: Agent; const s: Server; const Fresh: Function; +const Compromised: Function; const ne: Nonce; const kee: SessionKey; untrusted e; compromised k(e,s); +protocol kslSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr,Nc,Ma,Mb: Nonce; + const Kir: SessionKey; + const Kbb: TicketKey; + const Tr: GeneralizedTimestamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + 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}k(I,R), + {Nc}Kir, + Ma, + Mb,{Ma}Kir, + {Mb}Kir, + Kir, + Kbb + ); + claim_C3(C,Empty, (Compromised,Kir)); + claim_C4(C,Empty, (Compromised,Kbb)); + } +} + + protocol ksl(A,B,S) { role A diff --git a/spdl/SPORE/needham-schroeder-sk-amend.spdl b/spdl/SPORE/needham-schroeder-sk-amend.spdl index d18d0f1..808e31a 100644 --- a/spdl/SPORE/needham-schroeder-sk-amend.spdl +++ b/spdl/SPORE/needham-schroeder-sk-amend.spdl @@ -20,6 +20,30 @@ const dec,inc: Function; inversekeys(dec,inc); usertype SessionKey; const Fresh: Function; +const Compromised: Function; + +protocol needhamschroederskamendSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I, + {I,Nr}k(R,S), + I,R,Ni,{I,Nr}k(R,S), + {Ni,R,Kir,{Kir,Nr,I}k(R,S)}k(I,S), + {Kir,Nr,I}k(R,S), + {Nr}Kir, + {{Nr}dec}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} protocol needhamschroederskamend(I,R,S) { diff --git a/spdl/SPORE/needham-schroeder-sk.spdl b/spdl/SPORE/needham-schroeder-sk.spdl index 08288ed..d648798 100644 --- a/spdl/SPORE/needham-schroeder-sk.spdl +++ b/spdl/SPORE/needham-schroeder-sk.spdl @@ -16,6 +16,28 @@ const dec,inc: Function; inversekeys(dec,inc); usertype SessionKey; const Fresh: Function; +const Compromised: Function; + +protocol needhamschroederSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R,Ni), + {Ni,R,Kir,{Kir,I}k(R,S)}k(I,S), + {Kir,I}k(R,S), + {Nr}Kir, + {{Nr}dec}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} protocol needhamschroedersk(I,R,S) { diff --git a/spdl/SPORE/neumannstub-hwang.spdl b/spdl/SPORE/neumannstub-hwang.spdl index 8b44c7c..4685d36 100644 --- a/spdl/SPORE/neumannstub-hwang.spdl +++ b/spdl/SPORE/neumannstub-hwang.spdl @@ -18,12 +18,38 @@ secret k: Function; const a, b, e: Agent; const s: Server; const Fresh: Function; +const Compromised: Function; const ne: Nonce; const kee: SessionKey; untrusted e; compromised k(e,s); +protocol neustubHwangSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr,Mi,Mr: Nonce; + const Kir: SessionKey; + const Tr: TimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I,Ni, + R,{I,Ni,Tr,Nr}k(R,S), + {R,Ni,Kir,Tr}k(I,S), + {I,Kir,Tr}k(R,S), Nr, + {Nr}Kir, + Mi,{I,Kir,Tr}k(R,S), + Mr,{Mr}Kir, + {Mr}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + protocol neustubHwang(I,R,S) { role I diff --git a/spdl/SPORE/neumannstub.spdl b/spdl/SPORE/neumannstub.spdl index fd810b2..997f740 100644 --- a/spdl/SPORE/neumannstub.spdl +++ b/spdl/SPORE/neumannstub.spdl @@ -15,12 +15,38 @@ secret k: Function; const a, b, e: Agent; const s: Server; const Fresh: Function; +const Compromised: Function; const ne: Nonce; const kee: SessionKey; untrusted e; compromised k(e,s); +protocol neustubSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr,Mi,Mr: Nonce; + const Kir: SessionKey; + const Tr: TimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I,Ni, + R,{I,Ni,Tr}k(R,S),Nr, + {R,Ni,Kir,Tr}k(I,S), + {I,Kir,Tr}k(R,S), Nr, + {Nr}Kir, + Mi,{I,Kir,Tr}k(R,S), + Mr,{Mi}Kir, + {Mr}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + protocol neustub(I,R,S) { role I diff --git a/spdl/SPORE/otwayrees.spdl b/spdl/SPORE/otwayrees.spdl index b32455f..0ddc5db 100644 --- a/spdl/SPORE/otwayrees.spdl +++ b/spdl/SPORE/otwayrees.spdl @@ -12,9 +12,30 @@ secret const k : Function; const Fresh: Function; +const Compromised: Function; usertype String,SessionKey; +protocol otwayReesSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const M: String; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, M,I,R,{Ni,M,I,R}k(I,S), + {Nr,M,I,R}k(R,S), + {Ni,Kir}k(I,S), {Nr,Kir}k(R,S), + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + protocol otwayrees(I,R,S) { role I diff --git a/spdl/SPORE/tmn.spdl b/spdl/SPORE/tmn.spdl index 1109925..ceb0f97 100644 --- a/spdl/SPORE/tmn.spdl +++ b/spdl/SPORE/tmn.spdl @@ -13,6 +13,26 @@ const pk: Function; secret sk: Function; inversekeys(pk,sk); const Fresh: Function; +const Compromised: Function; + +protocol tmnSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kr,Ki: Key; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, R,{Ki}pk(S), + I, {Kr}pk(S), + {Kr}Ki, + Kr + ); + claim_C3(C,Empty, (Compromised,Kr)); + } +} protocol tmn(I,R,S) { diff --git a/spdl/SPORE/wmf-lowe.spdl b/spdl/SPORE/wmf-lowe.spdl index b902ec2..7866319 100644 --- a/spdl/SPORE/wmf-lowe.spdl +++ b/spdl/SPORE/wmf-lowe.spdl @@ -14,9 +14,31 @@ usertype TimeStamp; const succ,pred: Function; inversekeys (succ,pred); const Fresh: Function; +const Compromised: Function; secret k: Function; +protocol wmfLoweSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: Key; + const Ti,Ts: TimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I, {Ti,R,Kir}k(I,S), + {Ts,I,Kir}k(R,S), + {Nr}k(I,S), + {{Nr}succ}k(I,S), + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + protocol wmfLowe(I,R,S) { role I diff --git a/spdl/SPORE/wmf.spdl b/spdl/SPORE/wmf.spdl index b9ed62b..6a56f5c 100644 --- a/spdl/SPORE/wmf.spdl +++ b/spdl/SPORE/wmf.spdl @@ -9,6 +9,26 @@ usertype TimeStamp; secret k: Function; const Fresh: Function; +const Compromised: Function; + +protocol wmfSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: Key; + const Ti,Ts: TimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I, {Ti,R,Kir}k(I,S), + {Ts,I,Kir}k(R,S), + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} protocol wmf(I,R,S) { diff --git a/spdl/SPORE/woo-lam.spdl b/spdl/SPORE/woo-lam.spdl index 4fdfe9e..91ab8ed 100644 --- a/spdl/SPORE/woo-lam.spdl +++ b/spdl/SPORE/woo-lam.spdl @@ -13,6 +13,31 @@ usertype Key; secret k: Function; const Fresh: Function; +const Compromised: Function; + +protocol woolamSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const N1,N2: Nonce; + const Kir: Key; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I,N1, + R,N2, + {I,R,N1,N2}k(I,S), + {I,R,N1,N2}k(R,S), + {R,N1,N2,Kir}k(I,S), + {I,N1,N2,Kir}k(R,S), + {N1,N2}Kir, + {N2}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} protocol woolam(I,R,S) { diff --git a/spdl/SPORE/yahalom-ban.spdl b/spdl/SPORE/yahalom-ban.spdl index 27a7137..3ea7cbe 100644 --- a/spdl/SPORE/yahalom-ban.spdl +++ b/spdl/SPORE/yahalom-ban.spdl @@ -12,6 +12,29 @@ secret k : Function; usertype Key; const Fresh: Function; +const Compromised: Function; + +protocol yahalomBANSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: Key; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I,Ni, + R,Nr,{I,Ni}k(R,S), + Nr,{R,Kir,Ni}k(I,S), + {I,Kir,Nr}k(R,S), + {Nr}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + protocol yahalomBAN(I,R,S) diff --git a/spdl/SPORE/yahalom-paulson.spdl b/spdl/SPORE/yahalom-paulson.spdl index cc852db..0930891 100644 --- a/spdl/SPORE/yahalom-paulson.spdl +++ b/spdl/SPORE/yahalom-paulson.spdl @@ -10,9 +10,31 @@ secret k : Function; const Fresh: Function; +const Compromised: Function; usertype Key; +protocol yahalomPaulsonSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: Key; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I,Ni, + R,Nr,{I,Ni}k(R,S), + Nr,{R,Kir,Ni}k(I,S), + {I,R,Kir,Nr}k(R,S), + {Nr}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + protocol yahalomPaulson(I,R,S) { diff --git a/spdl/SPORE/yahalom.spdl b/spdl/SPORE/yahalom.spdl index 5cb6f6d..3a3d37e 100644 --- a/spdl/SPORE/yahalom.spdl +++ b/spdl/SPORE/yahalom.spdl @@ -12,6 +12,28 @@ secret k : Function; usertype Key; const Fresh: Function; +const Compromised: Function; + +protocol yahalomSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: Key; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I,Ni, + R,{I,Ni,Nr}k(R,S), + {R,Kir,Ni,Nr}k(I,S), + {I,Kir}k(R,S), + {Nr}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} protocol yahalom(I,R,S)