From 8fe754f4ecdd496581dc874c90397628dd3adb31 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Fri, 16 Nov 2007 09:00:23 +0100 Subject: [PATCH] Moved key-compromise models into their own directory and removed key-compromise models from base protocols. --- gui/Protocols/README.txt | 6 ++++ gui/Protocols/andrew-ban-concrete.spdl | 21 -------------- gui/Protocols/andrew-ban.spdl | 20 ------------- gui/Protocols/andrew-lowe-ban.spdl | 20 ------------- gui/Protocols/andrew.spdl | 20 ------------- gui/Protocols/denning-sacco-lowe.spdl | 22 --------------- gui/Protocols/denning-sacco.spdl | 20 ------------- gui/Protocols/kaochow-v2.spdl | 23 --------------- gui/Protocols/kaochow-v3.spdl | 26 ----------------- gui/Protocols/kaochow.spdl | 21 -------------- gui/Protocols/ksl-lowe.spdl | 28 ------------------- gui/Protocols/needham-schroeder-sk-amend.spdl | 23 --------------- gui/Protocols/needham-schroeder-sk.spdl | 21 -------------- gui/Protocols/neumannstub-hwang.spdl | 25 ----------------- gui/Protocols/neumannstub-keycompromise.spdl | 25 ----------------- gui/Protocols/otwayrees.spdl | 20 ------------- gui/Protocols/tmn.spdl | 19 ------------- gui/Protocols/wmf-lowe.spdl | 21 -------------- gui/Protocols/wmf.spdl | 19 ------------- gui/Protocols/woo-lam.spdl | 24 ---------------- gui/Protocols/yahalom-ban.spdl | 23 --------------- gui/Protocols/yahalom-paulson.spdl | 22 --------------- 22 files changed, 6 insertions(+), 463 deletions(-) create mode 100644 gui/Protocols/README.txt diff --git a/gui/Protocols/README.txt b/gui/Protocols/README.txt new file mode 100644 index 0000000..83e5864 --- /dev/null +++ b/gui/Protocols/README.txt @@ -0,0 +1,6 @@ +The protocols here are modeled according to their description in the +SPORE library. + +In the 'key-compromise' directory one can find the same protocols, but +modified to model the compromise of earlier sessions and the leakage of +the corresponding local values. diff --git a/gui/Protocols/andrew-ban-concrete.spdl b/gui/Protocols/andrew-ban-concrete.spdl index 2fbab12..dd2c417 100644 --- a/gui/Protocols/andrew-ban-concrete.spdl +++ b/gui/Protocols/andrew-ban-concrete.spdl @@ -33,27 +33,6 @@ protocol @swapkey(X) } } -protocol andrew-Concrete^KeyCompromise(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 andrew-Concrete(I,R) { diff --git a/gui/Protocols/andrew-ban.spdl b/gui/Protocols/andrew-ban.spdl index 8fb918d..653ad87 100644 --- a/gui/Protocols/andrew-ban.spdl +++ b/gui/Protocols/andrew-ban.spdl @@ -16,26 +16,6 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol andrew-Ban^KeyCompromise(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 andrew-Ban(I,R) { role I diff --git a/gui/Protocols/andrew-lowe-ban.spdl b/gui/Protocols/andrew-lowe-ban.spdl index 57785be..1f24904 100644 --- a/gui/Protocols/andrew-lowe-ban.spdl +++ b/gui/Protocols/andrew-lowe-ban.spdl @@ -23,26 +23,6 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol andrew-LoweBan^KeyCompromise(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 andrew-LoweBan(I,R) { role I diff --git a/gui/Protocols/andrew.spdl b/gui/Protocols/andrew.spdl index d7b006f..ded8fec 100644 --- a/gui/Protocols/andrew.spdl +++ b/gui/Protocols/andrew.spdl @@ -15,26 +15,6 @@ const succ: Function; const Fresh: Function; const Compromised: Function; -protocol andrew^KeyCompromise(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) { role I diff --git a/gui/Protocols/denning-sacco-lowe.spdl b/gui/Protocols/denning-sacco-lowe.spdl index e5cbd1b..1365e6c 100644 --- a/gui/Protocols/denning-sacco-lowe.spdl +++ b/gui/Protocols/denning-sacco-lowe.spdl @@ -17,28 +17,6 @@ const dec: PseudoFunction; const Fresh: Function; const Compromised: Function; -protocol denningSacco-Lowe^KeyCompromise(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: ExpiredTimeStamp; - 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 denningSacco-Lowe(I,R,S) { role I diff --git a/gui/Protocols/denning-sacco.spdl b/gui/Protocols/denning-sacco.spdl index 52f2f45..329c69c 100644 --- a/gui/Protocols/denning-sacco.spdl +++ b/gui/Protocols/denning-sacco.spdl @@ -12,26 +12,6 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol denningSacco^KeyCompromise(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: ExpiredTimeStamp; - 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) { role I diff --git a/gui/Protocols/kaochow-v2.spdl b/gui/Protocols/kaochow-v2.spdl index 2ce4f02..b19a94e 100644 --- a/gui/Protocols/kaochow-v2.spdl +++ b/gui/Protocols/kaochow-v2.spdl @@ -9,29 +9,6 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol kaochow-2^KeyCompromise(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 kaochow-2(I,R,S) { role I diff --git a/gui/Protocols/kaochow-v3.spdl b/gui/Protocols/kaochow-v3.spdl index 18d4d3d..1afe57e 100644 --- a/gui/Protocols/kaochow-v3.spdl +++ b/gui/Protocols/kaochow-v3.spdl @@ -11,32 +11,6 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol kaochow-3^KeyCompromise(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: ExpiredTimeStamp; - 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 kaochow-3(I,R,S) { role I diff --git a/gui/Protocols/kaochow.spdl b/gui/Protocols/kaochow.spdl index 1e2e91e..01b378d 100644 --- a/gui/Protocols/kaochow.spdl +++ b/gui/Protocols/kaochow.spdl @@ -9,27 +9,6 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol kaochow^KeyCompromise(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) { role I diff --git a/gui/Protocols/ksl-lowe.spdl b/gui/Protocols/ksl-lowe.spdl index 226899c..948d8da 100644 --- a/gui/Protocols/ksl-lowe.spdl +++ b/gui/Protocols/ksl-lowe.spdl @@ -22,34 +22,6 @@ const kee: SessionKey; untrusted e; compromised k(e,s); -protocol ksl-Lowe^KeyCompromise(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: ExpiredTimeStamp; - 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 ksl-Lowe(I,R,S) { role I diff --git a/gui/Protocols/needham-schroeder-sk-amend.spdl b/gui/Protocols/needham-schroeder-sk-amend.spdl index 739d4ce..7554dc7 100644 --- a/gui/Protocols/needham-schroeder-sk-amend.spdl +++ b/gui/Protocols/needham-schroeder-sk-amend.spdl @@ -18,29 +18,6 @@ usertype SessionKey; const Fresh: Function; const Compromised: Function; -protocol needhamschroedersk-amend^KeyCompromise(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 needhamschroedersk-amend(I,R,S) { role I diff --git a/gui/Protocols/needham-schroeder-sk.spdl b/gui/Protocols/needham-schroeder-sk.spdl index 8beed6a..38b9919 100644 --- a/gui/Protocols/needham-schroeder-sk.spdl +++ b/gui/Protocols/needham-schroeder-sk.spdl @@ -14,27 +14,6 @@ usertype SessionKey; const Fresh: Function; const Compromised: Function; -protocol needhamschroedersk^KeyCompromise(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) { role I diff --git a/gui/Protocols/neumannstub-hwang.spdl b/gui/Protocols/neumannstub-hwang.spdl index 1f402db..bbaff4e 100644 --- a/gui/Protocols/neumannstub-hwang.spdl +++ b/gui/Protocols/neumannstub-hwang.spdl @@ -22,31 +22,6 @@ const kee: SessionKey; untrusted e; compromised k(e,s); -protocol neustub-Hwang^KeyCompromise(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: ExpiredTimeStamp; - 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,{Mi}Kir, - {Mr}Kir, - Kir - ); - claim_C3(C,Empty, (Compromised,Kir)); - } -} - protocol neustub-Hwang(I,R,S) { role I diff --git a/gui/Protocols/neumannstub-keycompromise.spdl b/gui/Protocols/neumannstub-keycompromise.spdl index d1e4784..c4ccb60 100644 --- a/gui/Protocols/neumannstub-keycompromise.spdl +++ b/gui/Protocols/neumannstub-keycompromise.spdl @@ -21,31 +21,6 @@ const kee: SessionKey; untrusted Eve; compromised k(Eve,Simon); -protocol neustub^KeyCompromise(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: ExpiredTimeStamp; - 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^Repeat(I,R,S) { const Kir: SessionKey; diff --git a/gui/Protocols/otwayrees.spdl b/gui/Protocols/otwayrees.spdl index 5aa87df..4b112c1 100644 --- a/gui/Protocols/otwayrees.spdl +++ b/gui/Protocols/otwayrees.spdl @@ -11,26 +11,6 @@ const Compromised: Function; usertype String,SessionKey; -protocol otwayRees^KeyCompromise(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/gui/Protocols/tmn.spdl b/gui/Protocols/tmn.spdl index 51e5b7f..ce6a7e3 100644 --- a/gui/Protocols/tmn.spdl +++ b/gui/Protocols/tmn.spdl @@ -14,25 +14,6 @@ inversekeys(pk,sk); const Fresh: Function; const Compromised: Function; -protocol tmn^KeyCompromise(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: SessionKey; - 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) { role I diff --git a/gui/Protocols/wmf-lowe.spdl b/gui/Protocols/wmf-lowe.spdl index 58cf2f8..17f183f 100644 --- a/gui/Protocols/wmf-lowe.spdl +++ b/gui/Protocols/wmf-lowe.spdl @@ -19,27 +19,6 @@ const Compromised: Function; secret k: Function; -protocol wmf-Lowe^KeyCompromise(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 Ti,Ts: ExpiredTimeStamp; - var I,R,S: Agent; - - read_!C1(C,C, I,R,S); - send_!C2(C,C, I, {I,Ti,R,Kir}k(I,S), - {S,Ts,I,Kir}k(R,S), - {R,Nr}Kir, - {I,{Nr}succ}Kir, - Kir - ); - claim_C3(C,Empty, (Compromised,Kir)); - } -} - protocol wmf-Lowe(I,R,S) { role I diff --git a/gui/Protocols/wmf.spdl b/gui/Protocols/wmf.spdl index 1c6ad7d..aa2f10d 100644 --- a/gui/Protocols/wmf.spdl +++ b/gui/Protocols/wmf.spdl @@ -16,25 +16,6 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol wmf^KeyCompromise(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 Ti,Ts: ExpiredTimeStamp; - var I,R,S: Agent; - - read_!C1(C,C, I,R,S); - send_!C2(C,C, I, {I,Ti,R,Kir}k(I,S), - {S,Ts,I,Kir}k(R,S), - Kir - ); - claim_C3(C,Empty, (Compromised,Kir)); - } -} - protocol wmf(I,R,S) { role I diff --git a/gui/Protocols/woo-lam.spdl b/gui/Protocols/woo-lam.spdl index 685d95e..abf2e2a 100644 --- a/gui/Protocols/woo-lam.spdl +++ b/gui/Protocols/woo-lam.spdl @@ -11,30 +11,6 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol woolam^KeyCompromise(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: SessionKey; - 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) { role I diff --git a/gui/Protocols/yahalom-ban.spdl b/gui/Protocols/yahalom-ban.spdl index d2047ef..63ae5b7 100644 --- a/gui/Protocols/yahalom-ban.spdl +++ b/gui/Protocols/yahalom-ban.spdl @@ -10,29 +10,6 @@ usertype SessionKey; const Fresh: Function; const Compromised: Function; -protocol yahalom-BAN^KeyCompromise(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,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 yahalom-BAN(I,R,S) { role I diff --git a/gui/Protocols/yahalom-paulson.spdl b/gui/Protocols/yahalom-paulson.spdl index 0295038..1b6a10d 100644 --- a/gui/Protocols/yahalom-paulson.spdl +++ b/gui/Protocols/yahalom-paulson.spdl @@ -11,28 +11,6 @@ const Compromised: Function; usertype SessionKey; -//protocol yahalom-Paulson^KeyCompromise(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,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 yahalom-Paulson(I,R,S) { role I