From 0f54f2ed23cd81ec158008c38221902d1113d677 Mon Sep 17 00:00:00 2001 From: gijs Date: Mon, 15 Aug 2005 13:31:48 +0000 Subject: [PATCH] - Update modeling of needham schroeder to better reflect the modelling in SPORE: - pk is not known to all agents, only pk(Simon) is known - Use new naming convention: - Protocol name starting with an @ means internal protocol - For non internal protocols naming is as follows: protocolname-variant^subprotocol For example: yahalom-Lowe^KeyCompromise meaning the key compromise sub protocol of the Lowe variant of the Yahalom protocol. --- spdl/SPORE/andrew-ban-concrete.spdl | 12 ++++++------ spdl/SPORE/andrew-ban.spdl | 12 ++++++------ spdl/SPORE/andrew-lowe-ban.spdl | 12 ++++++------ spdl/SPORE/andrew.spdl | 2 +- spdl/SPORE/ccitt509-1.spdl | 10 +++++----- spdl/SPORE/ccitt509-1c.spdl | 10 +++++----- spdl/SPORE/ccitt509-3.spdl | 10 +++++----- spdl/SPORE/ccitt509-ban3.spdl | 10 +++++----- spdl/SPORE/denning-sacco-lowe.spdl | 18 +++++++++--------- spdl/SPORE/denning-sacco.spdl | 2 +- spdl/SPORE/kaochow-v2.spdl | 16 ++++++++-------- spdl/SPORE/kaochow-v3.spdl | 16 ++++++++-------- spdl/SPORE/kaochow.spdl | 2 +- spdl/SPORE/ksl-lowe.spdl | 10 +++++----- spdl/SPORE/ksl.spdl | 2 +- spdl/SPORE/needham-schroeder-lowe.spdl | 21 +++++++++++++-------- spdl/SPORE/needham-schroeder-sk-amend.spdl | 16 ++++++++-------- spdl/SPORE/needham-schroeder-sk.spdl | 2 +- spdl/SPORE/needham-schroeder.spdl | 8 +++++++- spdl/SPORE/neumannstub-hwang.spdl | 10 +++++----- spdl/SPORE/neumannstub.spdl | 4 ++-- spdl/SPORE/otwayrees.spdl | 2 +- spdl/SPORE/splice-as-cj.spdl | 8 ++++---- spdl/SPORE/splice-as-hc.spdl | 8 ++++---- spdl/SPORE/tmn.spdl | 2 +- spdl/SPORE/wmf-lowe.spdl | 10 +++++----- spdl/SPORE/wmf.spdl | 2 +- spdl/SPORE/woo-lam-pi-1.spdl | 8 ++++---- spdl/SPORE/woo-lam-pi-2.spdl | 8 ++++---- spdl/SPORE/woo-lam-pi-3.spdl | 8 ++++---- spdl/SPORE/woo-lam-pi-f.spdl | 8 ++++---- spdl/SPORE/woo-lam.spdl | 2 +- spdl/SPORE/yahalom-ban.spdl | 10 +++++----- spdl/SPORE/yahalom-lowe.spdl | 8 ++++---- spdl/SPORE/yahalom-paulson.spdl | 10 +++++----- spdl/SPORE/yahalom.spdl | 2 +- 36 files changed, 156 insertions(+), 145 deletions(-) diff --git a/spdl/SPORE/andrew-ban-concrete.spdl b/spdl/SPORE/andrew-ban-concrete.spdl index da0c80b..8c75bfe 100644 --- a/spdl/SPORE/andrew-ban-concrete.spdl +++ b/spdl/SPORE/andrew-ban-concrete.spdl @@ -33,7 +33,7 @@ protocol @swapkey(X) } } -protocol andrewConcreteSessionKeyCompromise(C) +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 @@ -54,7 +54,7 @@ protocol andrewConcreteSessionKeyCompromise(C) } -protocol andrewConcrete(I,R) +protocol andrew-Concrete(I,R) { role I @@ -99,7 +99,7 @@ const kee: SessionKey; # run andrewConcrete.R(Bob,Alice); # This is the original scenario -run andrewConcrete.I(Agent,Agent); -run andrewConcrete.R(Agent,Agent); -run andrewConcrete.I(Agent,Agent); -run andrewConcrete.R(Agent,Agent); +run andrew-Concrete.I(Agent,Agent); +run andrew-Concrete.R(Agent,Agent); +run andrew-Concrete.I(Agent,Agent); +run andrew-Concrete.R(Agent,Agent); diff --git a/spdl/SPORE/andrew-ban.spdl b/spdl/SPORE/andrew-ban.spdl index b1538ec..eb6b2cd 100644 --- a/spdl/SPORE/andrew-ban.spdl +++ b/spdl/SPORE/andrew-ban.spdl @@ -16,7 +16,7 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol andrewBanSessionKeyCompromise(C) +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 @@ -36,7 +36,7 @@ protocol andrewBanSessionKeyCompromise(C) } } -protocol andrewBan(I,R) +protocol andrew-Ban(I,R) { role I { @@ -84,7 +84,7 @@ compromised k(Eve,Bob); compromised k(Alice,Eve); compromised k(Bob,Eve); -run andrewBan.I(Agent,Agent); -run andrewBan.R(Agent,Agent); -run andrewBan.I(Agent,Agent); -run andrewBan.R(Agent,Agent); +run andrew-Ban.I(Agent,Agent); +run andrew-Ban.R(Agent,Agent); +run andrew-Ban.I(Agent,Agent); +run andrew-Ban.R(Agent,Agent); diff --git a/spdl/SPORE/andrew-lowe-ban.spdl b/spdl/SPORE/andrew-lowe-ban.spdl index 3e4fdb8..ef1ef3f 100644 --- a/spdl/SPORE/andrew-lowe-ban.spdl +++ b/spdl/SPORE/andrew-lowe-ban.spdl @@ -23,7 +23,7 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol andrewLoweBanSessionKeyCompromise(C) +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 @@ -43,7 +43,7 @@ protocol andrewLoweBanSessionKeyCompromise(C) } } -protocol andrewLoweBan(I,R) +protocol andrew-LoweBan(I,R) { role I { @@ -89,7 +89,7 @@ compromised k(Bob,Eve); -run andrewLoweBan.I(Agent,Agent); -run andrewLoweBan.R(Agent,Agent); -run andrewLoweBan.I(Agent,Agent); -run andrewLoweBan.R(Agent,Agent); +run andrew-LoweBan.I(Agent,Agent); +run andrew-LoweBan.R(Agent,Agent); +run andrew-LoweBan.I(Agent,Agent); +run andrew-LoweBan.R(Agent,Agent); diff --git a/spdl/SPORE/andrew.spdl b/spdl/SPORE/andrew.spdl index 0fd4191..8df6028 100644 --- a/spdl/SPORE/andrew.spdl +++ b/spdl/SPORE/andrew.spdl @@ -15,7 +15,7 @@ const succ: Function; const Fresh: Function; const Compromised: Function; -protocol andrewSessionKeyCompromise(C) +protocol andrew^KeyCompromise(C) { // Read the names of 2 agents and disclose a session between them including // corresponding session key to simulate key compromise diff --git a/spdl/SPORE/ccitt509-1.spdl b/spdl/SPORE/ccitt509-1.spdl index 8cd3354..1db5821 100644 --- a/spdl/SPORE/ccitt509-1.spdl +++ b/spdl/SPORE/ccitt509-1.spdl @@ -14,7 +14,7 @@ secret sk: Function; inversekeys(pk,sk); usertype Timestamp; -protocol ccitt5091(I,R) +protocol ccitt509-1(I,R) { role I { @@ -45,7 +45,7 @@ compromised sk(Eve); # General scenario, 2 parallel runs of the protocol -run ccitt5091.I(Agent,Agent); -run ccitt5091.R(Agent,Agent); -run ccitt5091.I(Agent,Agent); -run ccitt5091.R(Agent,Agent); +run ccitt509-1.I(Agent,Agent); +run ccitt509-1.R(Agent,Agent); +run ccitt509-1.I(Agent,Agent); +run ccitt509-1.R(Agent,Agent); diff --git a/spdl/SPORE/ccitt509-1c.spdl b/spdl/SPORE/ccitt509-1c.spdl index a8b8560..e6b7dbb 100644 --- a/spdl/SPORE/ccitt509-1c.spdl +++ b/spdl/SPORE/ccitt509-1c.spdl @@ -13,7 +13,7 @@ inversekeys (hash,unhash); inversekeys(pk,sk); usertype Timestamp; -protocol ccitt5091c(I,R) +protocol ccitt509-1c(I,R) { role I { @@ -44,7 +44,7 @@ compromised sk(Eve); # General scenario, 2 parallel runs of the protocol -run ccitt5091c.I(Agent,Agent); -run ccitt5091c.R(Agent,Agent); -run ccitt5091c.I(Agent,Agent); -run ccitt5091c.R(Agent,Agent); +run ccitt509-1c.I(Agent,Agent); +run ccitt509-1c.R(Agent,Agent); +run ccitt509-1c.I(Agent,Agent); +run ccitt509-1c.R(Agent,Agent); diff --git a/spdl/SPORE/ccitt509-3.spdl b/spdl/SPORE/ccitt509-3.spdl index dbb9e87..4c23aa0 100644 --- a/spdl/SPORE/ccitt509-3.spdl +++ b/spdl/SPORE/ccitt509-3.spdl @@ -13,7 +13,7 @@ secret sk: Function; inversekeys(pk,sk); usertype Timestamp; -protocol ccitt5093(I,R) +protocol ccitt509-3(I,R) { role I { @@ -56,7 +56,7 @@ compromised sk(Eve); # General scenario, 2 parallel runs of the protocol -run ccitt5093.I(Agent,Agent); -run ccitt5093.R(Agent,Agent); -run ccitt5093.I(Agent,Agent); -run ccitt5093.R(Agent,Agent); +run ccitt509-3.I(Agent,Agent); +run ccitt509-3.R(Agent,Agent); +run ccitt509-3.I(Agent,Agent); +run ccitt509-3.R(Agent,Agent); diff --git a/spdl/SPORE/ccitt509-ban3.spdl b/spdl/SPORE/ccitt509-ban3.spdl index b69c34b..bc2e7c8 100644 --- a/spdl/SPORE/ccitt509-ban3.spdl +++ b/spdl/SPORE/ccitt509-ban3.spdl @@ -15,7 +15,7 @@ const pk: Function; secret sk: Function; inversekeys(pk,sk); -protocol ccitt509ban3(I,R) +protocol ccitt509-ban3(I,R) { role I { @@ -49,7 +49,7 @@ compromised sk(Eve); # General scenario, 2 parallel runs of the protocol -run ccitt509ban3.I(Agent,Agent); -run ccitt509ban3.R(Agent,Agent); -run ccitt509ban3.I(Agent,Agent); -run ccitt509ban3.R(Agent,Agent); +run ccitt509-ban3.I(Agent,Agent); +run ccitt509-ban3.R(Agent,Agent); +run ccitt509-ban3.I(Agent,Agent); +run ccitt509-ban3.R(Agent,Agent); diff --git a/spdl/SPORE/denning-sacco-lowe.spdl b/spdl/SPORE/denning-sacco-lowe.spdl index 7d4f2f4..0e16ead 100644 --- a/spdl/SPORE/denning-sacco-lowe.spdl +++ b/spdl/SPORE/denning-sacco-lowe.spdl @@ -21,14 +21,14 @@ const dec: PseudoFunction; const Fresh: Function; const Compromised: Function; -protocol denningSaccoLoweSessionKeyCompromise(C) +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; + const T: TimeStamp; var I,R,S: Agent; read_C1(C,C, I,R,S); @@ -43,7 +43,7 @@ protocol denningSaccoLoweSessionKeyCompromise(C) } } -protocol denningSaccoLowe(I,R,S) +protocol denningSacco-Lowe(I,R,S) { role I { @@ -102,9 +102,9 @@ compromised k(Eve,Simon); # Note because the modelchecker does not support tickets this might not # be very useful -run denningSaccoLowe.I(Agent,Agent,Simon); -run denningSaccoLowe.R(Agent,Agent,Simon); -run denningSaccoLowe.S(Agent,Agent,Simon); -run denningSaccoLowe.I(Agent,Agent,Simon); -run denningSaccoLowe.R(Agent,Agent,Simon); -run denningSaccoLowe.S(Agent,Agent,Simon); +run denningSacco-Lowe.I(Agent,Agent,Simon); +run denningSacco-Lowe.R(Agent,Agent,Simon); +run denningSacco-Lowe.S(Agent,Agent,Simon); +run denningSacco-Lowe.I(Agent,Agent,Simon); +run denningSacco-Lowe.R(Agent,Agent,Simon); +run denningSacco-Lowe.S(Agent,Agent,Simon); diff --git a/spdl/SPORE/denning-sacco.spdl b/spdl/SPORE/denning-sacco.spdl index 8eabe4c..82f7a11 100644 --- a/spdl/SPORE/denning-sacco.spdl +++ b/spdl/SPORE/denning-sacco.spdl @@ -16,7 +16,7 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol denningSaccoSessionKeyCompromise(C) +protocol denningSacco^KeyCompromise(C) { // Read the names of 3 agents and disclose a session between them including // corresponding session key to simulate key compromise diff --git a/spdl/SPORE/kaochow-v2.spdl b/spdl/SPORE/kaochow-v2.spdl index 1dd4268..60db2d2 100644 --- a/spdl/SPORE/kaochow-v2.spdl +++ b/spdl/SPORE/kaochow-v2.spdl @@ -13,7 +13,7 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol kaochow2SessionKeyCompromise(C) +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 @@ -36,7 +36,7 @@ protocol kaochow2SessionKeyCompromise(C) } } -protocol kaochow2(I,R,S) +protocol kaochow-2(I,R,S) { role I { @@ -95,9 +95,9 @@ compromised k(Alice,Eve); compromised k(Bob,Eve); compromised k(Simon,Eve); -run kaochow2.I(Agent,Agent,Simon); -run kaochow2.R(Agent,Agent,Simon); -run kaochow2.S(Agent,Agent,Simon); -run kaochow2.I(Agent,Agent,Simon); -run kaochow2.R(Agent,Agent,Simon); -run kaochow2.S(Agent,Agent,Simon); +run kaochow-2.I(Agent,Agent,Simon); +run kaochow-2.R(Agent,Agent,Simon); +run kaochow-2.S(Agent,Agent,Simon); +run kaochow-2.I(Agent,Agent,Simon); +run kaochow-2.R(Agent,Agent,Simon); +run kaochow-2.S(Agent,Agent,Simon); diff --git a/spdl/SPORE/kaochow-v3.spdl b/spdl/SPORE/kaochow-v3.spdl index 285782a..256475d 100644 --- a/spdl/SPORE/kaochow-v3.spdl +++ b/spdl/SPORE/kaochow-v3.spdl @@ -15,7 +15,7 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol kaochow3SessionKeyCompromise(C) +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 @@ -41,7 +41,7 @@ protocol kaochow3SessionKeyCompromise(C) } } -protocol kaochow3(I,R,S) +protocol kaochow-3(I,R,S) { role I { @@ -102,9 +102,9 @@ compromised k(Alice,Eve); compromised k(Bob,Eve); compromised k(Simon,Eve); -run kaochow3.I(Agent,Agent,Simon); -run kaochow3.R(Agent,Agent,Simon); -run kaochow3.S(Agent,Agent,Simon); -run kaochow3.I(Agent,Agent,Simon); -run kaochow3.R(Agent,Agent,Simon); -run kaochow3.S(Agent,Agent,Simon); +run kaochow-3.I(Agent,Agent,Simon); +run kaochow-3.R(Agent,Agent,Simon); +run kaochow-3.S(Agent,Agent,Simon); +run kaochow-3.I(Agent,Agent,Simon); +run kaochow-3.R(Agent,Agent,Simon); +run kaochow-3.S(Agent,Agent,Simon); diff --git a/spdl/SPORE/kaochow.spdl b/spdl/SPORE/kaochow.spdl index 2822d5e..a60d13a 100644 --- a/spdl/SPORE/kaochow.spdl +++ b/spdl/SPORE/kaochow.spdl @@ -13,7 +13,7 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol kaochowSessionKeyCompromise(C) +protocol kaochow^KeyCompromise(C) { // Read the names of 3 agents and disclose a session between them including // corresponding session key to simulate key compromise diff --git a/spdl/SPORE/ksl-lowe.spdl b/spdl/SPORE/ksl-lowe.spdl index c9aca4b..1719b38 100644 --- a/spdl/SPORE/ksl-lowe.spdl +++ b/spdl/SPORE/ksl-lowe.spdl @@ -26,7 +26,7 @@ const kee: SessionKey; untrusted e; compromised k(e,s); -protocol kslLoweSessionKeyCompromise(C) +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 @@ -54,7 +54,7 @@ protocol kslLoweSessionKeyCompromise(C) } } -protocol kslLowe(A,B,S) +protocol ksl-Lowe(A,B,S) { role A { @@ -112,7 +112,7 @@ protocol kslLowe(A,B,S) } } -run kslLowe.A(a,b,s); -run kslLowe.B(a,b,s); -run kslLowe.S(a,b,s); +run ksl-Lowe.A(a,b,s); +run ksl-Lowe.B(a,b,s); +run ksl-Lowe.S(a,b,s); diff --git a/spdl/SPORE/ksl.spdl b/spdl/SPORE/ksl.spdl index 9fa728a..539039e 100644 --- a/spdl/SPORE/ksl.spdl +++ b/spdl/SPORE/ksl.spdl @@ -23,7 +23,7 @@ const kee: SessionKey; untrusted e; compromised k(e,s); -protocol kslSessionKeyCompromise(C) +protocol ksl^KeyCompromise(C) { // Read the names of 3 agents and disclose a session between them including // corresponding session key to simulate key compromise diff --git a/spdl/SPORE/needham-schroeder-lowe.spdl b/spdl/SPORE/needham-schroeder-lowe.spdl index 399ce52..8d65a50 100644 --- a/spdl/SPORE/needham-schroeder-lowe.spdl +++ b/spdl/SPORE/needham-schroeder-lowe.spdl @@ -10,11 +10,12 @@ # synchronisation and agreement, because the keys that the server sends # out can be replayed. -const pk: Function; +secret pk: Function; # For some reason SPORE models it such that the agents + # do not know the public keys of the other agents secret sk: Function; inversekeys(pk,sk); -protocol needhamschroederpkLowe(I,R,S) +protocol needhamschroederpk-Lowe(I,R,S) { role I { @@ -28,6 +29,7 @@ protocol needhamschroederpkLowe(I,R,S) send_7(I,R, {Nr}pk(R)); claim_I1(I,Secret,Ni); claim_I2(I,Secret,Nr); + claim_I3(I,Nisynch); } role R @@ -42,6 +44,7 @@ protocol needhamschroederpkLowe(I,R,S) read_7(I,R,{Nr}pk(R)); claim_R1(R,Secret,Nr); claim_R2(R,Secret,Ni); + claim_R3(R,Nisynch); } role S @@ -58,12 +61,14 @@ const Alice,Bob,Simon,Eve: Agent; untrusted Eve; const ne: Nonce; compromised sk(Eve); +compromised pk(Eve); +compromised pk(Simon); # Needed because of the way SPORE models nsl # General scenario, 2 parallel runs of the protocol -run needhamschroederpkLowe.I(Agent,Agent,Simon); -run needhamschroederpkLowe.S(Agent,Agent,Simon); -run needhamschroederpkLowe.R(Agent,Agent,Simon); -run needhamschroederpkLowe.I(Agent,Agent,Simon); -run needhamschroederpkLowe.R(Agent,Agent,Simon); -run needhamschroederpkLowe.S(Agent,Agent,Simon); +run needhamschroederpk-Lowe.I(Agent,Agent,Simon); +run needhamschroederpk-Lowe.S(Agent,Agent,Simon); +run needhamschroederpk-Lowe.R(Agent,Agent,Simon); +run needhamschroederpk-Lowe.I(Agent,Agent,Simon); +run needhamschroederpk-Lowe.R(Agent,Agent,Simon); +run needhamschroederpk-Lowe.S(Agent,Agent,Simon); diff --git a/spdl/SPORE/needham-schroeder-sk-amend.spdl b/spdl/SPORE/needham-schroeder-sk-amend.spdl index 808e31a..ca7446b 100644 --- a/spdl/SPORE/needham-schroeder-sk-amend.spdl +++ b/spdl/SPORE/needham-schroeder-sk-amend.spdl @@ -22,7 +22,7 @@ usertype SessionKey; const Fresh: Function; const Compromised: Function; -protocol needhamschroederskamendSessionKeyCompromise(C) +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 @@ -45,7 +45,7 @@ protocol needhamschroederskamendSessionKeyCompromise(C) } } -protocol needhamschroederskamend(I,R,S) +protocol needhamschroedersk-amend(I,R,S) { role I { @@ -100,9 +100,9 @@ compromised k(Eve,Simon); # General scenario, 2 parallel runs of the protocol -run needhamschroederskamend.I(Agent,Agent,Simon); -run needhamschroederskamend.R(Agent,Agent,Simon); -run needhamschroederskamend.S(Agent,Agent,Simon); -run needhamschroederskamend.I(Agent,Agent,Simon); -run needhamschroederskamend.R(Agent,Agent,Simon); -run needhamschroederskamend.S(Agent,Agent,Simon); +run needhamschroedersk-amend.I(Agent,Agent,Simon); +run needhamschroedersk-amend.R(Agent,Agent,Simon); +run needhamschroedersk-amend.S(Agent,Agent,Simon); +run needhamschroedersk-amend.I(Agent,Agent,Simon); +run needhamschroedersk-amend.R(Agent,Agent,Simon); +run needhamschroedersk-amend.S(Agent,Agent,Simon); diff --git a/spdl/SPORE/needham-schroeder-sk.spdl b/spdl/SPORE/needham-schroeder-sk.spdl index d648798..49436e7 100644 --- a/spdl/SPORE/needham-schroeder-sk.spdl +++ b/spdl/SPORE/needham-schroeder-sk.spdl @@ -18,7 +18,7 @@ usertype SessionKey; const Fresh: Function; const Compromised: Function; -protocol needhamschroederSessionKeyCompromise(C) +protocol needhamschroedersk^KeyCompromise(C) { // Read the names of 3 agents and disclose a session between them including // corresponding session key to simulate key compromise diff --git a/spdl/SPORE/needham-schroeder.spdl b/spdl/SPORE/needham-schroeder.spdl index 37bbd6d..f46e887 100644 --- a/spdl/SPORE/needham-schroeder.spdl +++ b/spdl/SPORE/needham-schroeder.spdl @@ -10,7 +10,8 @@ # synchronisation and agreement, because the keys that the server sends # out can be replayed. -const pk: Function; +secret pk: Function; # For some reason SPORE models it such that the agents + # do not know the public keys of the other agents secret sk: Function; inversekeys(pk,sk); @@ -28,6 +29,7 @@ protocol needhamschroederpk(I,R,S) send_7(I,R, {Nr}pk(R)); claim_I1(I,Secret,Ni); claim_I2(I,Secret,Nr); + claim_I3(I,Nisynch); } role R @@ -42,6 +44,7 @@ protocol needhamschroederpk(I,R,S) read_7(I,R,{Nr}pk(R)); claim_R1(R,Secret,Nr); claim_R2(R,Secret,Ni); + claim_R3(R,Nisynch); } role S @@ -58,6 +61,9 @@ const Alice,Bob,Simon,Eve: Agent; untrusted Eve; const ne: Nonce; compromised sk(Eve); +compromised pk(Eve); +compromised pk(Simon); # Needed because SPORE only assumes agents know their + # own public key and that of the server # General scenario, 2 parallel runs of the protocol diff --git a/spdl/SPORE/neumannstub-hwang.spdl b/spdl/SPORE/neumannstub-hwang.spdl index 030627f..271b391 100644 --- a/spdl/SPORE/neumannstub-hwang.spdl +++ b/spdl/SPORE/neumannstub-hwang.spdl @@ -26,7 +26,7 @@ const kee: SessionKey; untrusted e; compromised k(e,s); -protocol neustubHwangSessionKeyCompromise(C) +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 @@ -51,7 +51,7 @@ protocol neustubHwangSessionKeyCompromise(C) } } -protocol neustubHwang(I,R,S) +protocol neustub-Hwang(I,R,S) { role I { @@ -106,7 +106,7 @@ protocol neustubHwang(I,R,S) } } -run neustubHwang.A(a,b,s); -run neustubHwang.B(a,b,s); -run neustubHwang.S(a,b,s); +run neustub-Hwang.A(a,b,s); +run neustub-Hwang.B(a,b,s); +run neustub-Hwang.S(a,b,s); diff --git a/spdl/SPORE/neumannstub.spdl b/spdl/SPORE/neumannstub.spdl index cf92db7..87839b9 100644 --- a/spdl/SPORE/neumannstub.spdl +++ b/spdl/SPORE/neumannstub.spdl @@ -25,7 +25,7 @@ const kee: SessionKey; untrusted Eve; compromised k(Eve,Simon); -protocol neustubSessionKeyCompromise(C) +protocol neustub^KeyCompromise(C) { // Read the names of 3 agents and disclose a session between them including // corresponding session key to simulate key compromise @@ -50,7 +50,7 @@ protocol neustubSessionKeyCompromise(C) } } -protocol @neustubRepeat(I,R,S) +protocol neustub^Repeat(I,R,S) { const Kir: SessionKey; diff --git a/spdl/SPORE/otwayrees.spdl b/spdl/SPORE/otwayrees.spdl index 0ddc5db..dbf182f 100644 --- a/spdl/SPORE/otwayrees.spdl +++ b/spdl/SPORE/otwayrees.spdl @@ -16,7 +16,7 @@ const Compromised: Function; usertype String,SessionKey; -protocol otwayReesSessionKeyCompromise(C) +protocol otwayRees^KeyCompromise(C) { // Read the names of 3 agents and disclose a session between them including // corresponding session key to simulate key compromise diff --git a/spdl/SPORE/splice-as-cj.spdl b/spdl/SPORE/splice-as-cj.spdl index 72d294a..c092a53 100644 --- a/spdl/SPORE/splice-as-cj.spdl +++ b/spdl/SPORE/splice-as-cj.spdl @@ -18,7 +18,7 @@ inversekeys (pk,sk); const inc,dec: Function; inversekeys (inc,dec); -protocol spliceASCJ(I,R,S) +protocol spliceAS-CJ(I,R,S) { role I { @@ -73,9 +73,9 @@ untrusted Eve; const ne: Nonce; compromised sk(Eve); -run spliceASCJ.I(Agent,Agent,Agent); -run spliceASCJ.R(Agent,Agent,Agent); -run spliceASCJ.S(Agent,Agent,Agent); +run spliceAS-CJ.I(Agent,Agent,Agent); +run spliceAS-CJ.R(Agent,Agent,Agent); +run spliceAS-CJ.S(Agent,Agent,Agent); #run spliceASCJ.I(Alice,Bob,Simon); #run spliceASCJ.R(Alice,Bob,Simon); diff --git a/spdl/SPORE/splice-as-hc.spdl b/spdl/SPORE/splice-as-hc.spdl index 8ddf292..005f94d 100644 --- a/spdl/SPORE/splice-as-hc.spdl +++ b/spdl/SPORE/splice-as-hc.spdl @@ -13,7 +13,7 @@ inversekeys (pk,sk); const inc,dec: Function; inversekeys (inc,dec); -protocol spliceASHC(I,R,S) +protocol spliceAS-HC(I,R,S) { role I { @@ -72,8 +72,8 @@ compromised sk(Eve); #run spliceASHC.R(Alice,Bob,Simon); #run spliceASHC.S(Alice,Bob,Simon); -run spliceASHC.I(Agent,Agent,Agent); -run spliceASHC.R(Agent,Agent,Agent); -run spliceASHC.S(Agent,Agent,Agent); +run spliceAS-HC.I(Agent,Agent,Agent); +run spliceAS-HC.R(Agent,Agent,Agent); +run spliceAS-HC.S(Agent,Agent,Agent); diff --git a/spdl/SPORE/tmn.spdl b/spdl/SPORE/tmn.spdl index ad6b610..817b6c9 100644 --- a/spdl/SPORE/tmn.spdl +++ b/spdl/SPORE/tmn.spdl @@ -14,7 +14,7 @@ inversekeys(pk,sk); const Fresh: Function; const Compromised: Function; -protocol tmnSessionKeyCompromise(C) +protocol tmn^KeyCompromise(C) { // Read the names of 3 agents and disclose a session between them including // corresponding session key to simulate key compromise diff --git a/spdl/SPORE/wmf-lowe.spdl b/spdl/SPORE/wmf-lowe.spdl index b66a5f9..6c78240 100644 --- a/spdl/SPORE/wmf-lowe.spdl +++ b/spdl/SPORE/wmf-lowe.spdl @@ -19,7 +19,7 @@ const Compromised: Function; secret k: Function; -protocol wmfLoweSessionKeyCompromise(C) +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 @@ -40,7 +40,7 @@ protocol wmfLoweSessionKeyCompromise(C) } } -protocol wmfLowe(I,R,S) +protocol wmf-Lowe(I,R,S) { role I { @@ -92,9 +92,9 @@ const Te: TimeStamp; untrusted Eve; compromised k(Eve,Simon); -run wmfLowe.I (Agent,Agent,Simon); -run wmfLowe.R (Agent,Agent,Simon); -run wmfLowe.S (Agent,Agent,Simon); +run wmf-Lowe.I (Agent,Agent,Simon); +run wmf-Lowe.R (Agent,Agent,Simon); +run wmf-Lowe.S (Agent,Agent,Simon); diff --git a/spdl/SPORE/wmf.spdl b/spdl/SPORE/wmf.spdl index 5edb81b..5cd2125 100644 --- a/spdl/SPORE/wmf.spdl +++ b/spdl/SPORE/wmf.spdl @@ -16,7 +16,7 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol wmfSessionKeyCompromise(C) +protocol wmf^KeyCompromise(C) { // Read the names of 3 agents and disclose a session between them including // corresponding session key to simulate key compromise diff --git a/spdl/SPORE/woo-lam-pi-1.spdl b/spdl/SPORE/woo-lam-pi-1.spdl index b03641e..831aec2 100644 --- a/spdl/SPORE/woo-lam-pi-1.spdl +++ b/spdl/SPORE/woo-lam-pi-1.spdl @@ -10,7 +10,7 @@ secret k: Function; -protocol woolamPi1(I,R,S) +protocol woolamPi-1(I,R,S) { role I { @@ -53,9 +53,9 @@ const Ne: Nonce; untrusted Eve; compromised k(Eve,Simon); -run woolamPi1.I (Agent,Agent,Simon); -run woolamPi1.R (Agent,Agent,Simon); -run woolamPi1.S (Agent,Agent,Simon); +run woolamPi-1.I (Agent,Agent,Simon); +run woolamPi-1.R (Agent,Agent,Simon); +run woolamPi-1.S (Agent,Agent,Simon); diff --git a/spdl/SPORE/woo-lam-pi-2.spdl b/spdl/SPORE/woo-lam-pi-2.spdl index e7d7d5a..3977d2c 100644 --- a/spdl/SPORE/woo-lam-pi-2.spdl +++ b/spdl/SPORE/woo-lam-pi-2.spdl @@ -10,7 +10,7 @@ secret k: Function; -protocol woolamPi2(I,R,S) +protocol woolamPi-2(I,R,S) { role I { @@ -53,9 +53,9 @@ const Ne: Nonce; untrusted Eve; compromised k(Eve,Simon); -run woolamPi2.I (Agent,Agent,Simon); -run woolamPi2.R (Agent,Agent,Simon); -run woolamPi2.S (Agent,Agent,Simon); +run woolamPi-2.I (Agent,Agent,Simon); +run woolamPi-2.R (Agent,Agent,Simon); +run woolamPi-2.S (Agent,Agent,Simon); diff --git a/spdl/SPORE/woo-lam-pi-3.spdl b/spdl/SPORE/woo-lam-pi-3.spdl index 98df50f..393686b 100644 --- a/spdl/SPORE/woo-lam-pi-3.spdl +++ b/spdl/SPORE/woo-lam-pi-3.spdl @@ -10,7 +10,7 @@ secret k: Function; -protocol woolamPi3(I,R,S) +protocol woolamPi-3(I,R,S) { role I { @@ -53,9 +53,9 @@ const Ne: Nonce; untrusted Eve; compromised k(Eve,Simon); -run woolamPi3.I (Agent,Agent,Simon); -run woolamPi3.R (Agent,Agent,Simon); -run woolamPi3.S (Agent,Agent,Simon); +run woolamPi-3.I (Agent,Agent,Simon); +run woolamPi-3.R (Agent,Agent,Simon); +run woolamPi-3.S (Agent,Agent,Simon); diff --git a/spdl/SPORE/woo-lam-pi-f.spdl b/spdl/SPORE/woo-lam-pi-f.spdl index 5889b20..bb10e15 100644 --- a/spdl/SPORE/woo-lam-pi-f.spdl +++ b/spdl/SPORE/woo-lam-pi-f.spdl @@ -10,7 +10,7 @@ secret k: Function; -protocol woolamPif(I,R,S) +protocol woolamPi-f(I,R,S) { role I { @@ -53,7 +53,7 @@ const Ne: Nonce; untrusted Eve; compromised k(Eve,Simon); -run woolamPif.I (Agent,Agent,Simon); -run woolamPif.R (Agent,Agent,Simon); -run woolamPif.S (Agent,Agent,Simon); +run woolamPi-f.I (Agent,Agent,Simon); +run woolamPi-f.R (Agent,Agent,Simon); +run woolamPi-f.S (Agent,Agent,Simon); diff --git a/spdl/SPORE/woo-lam.spdl b/spdl/SPORE/woo-lam.spdl index d4d3b60..bb5c736 100644 --- a/spdl/SPORE/woo-lam.spdl +++ b/spdl/SPORE/woo-lam.spdl @@ -15,7 +15,7 @@ secret k: Function; const Fresh: Function; const Compromised: Function; -protocol woolamSessionKeyCompromise(C) +protocol woolam^KeyCompromise(C) { // Read the names of 3 agents and disclose a session between them including // corresponding session key to simulate key compromise diff --git a/spdl/SPORE/yahalom-ban.spdl b/spdl/SPORE/yahalom-ban.spdl index 98eefde..63110db 100644 --- a/spdl/SPORE/yahalom-ban.spdl +++ b/spdl/SPORE/yahalom-ban.spdl @@ -14,7 +14,7 @@ usertype SessionKey; const Fresh: Function; const Compromised: Function; -protocol yahalomBANSessionKeyCompromise(C) +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 @@ -37,7 +37,7 @@ protocol yahalomBANSessionKeyCompromise(C) -protocol yahalomBAN(I,R,S) +protocol yahalom-BAN(I,R,S) { role I { @@ -83,7 +83,7 @@ protocol yahalomBAN(I,R,S) const Alice,Bob,Simon : Agent; -run yahalomBAN.I(Agent,Agent,s); -run yahalomBAN.I(Agent,Agent,s); -run yahalomBAN.R(Agent,Agent,s); +run yahalom-BAN.I(Agent,Agent,s); +run yahalom-BAN.I(Agent,Agent,s); +run yahalom-BAN.R(Agent,Agent,s); diff --git a/spdl/SPORE/yahalom-lowe.spdl b/spdl/SPORE/yahalom-lowe.spdl index fe9341d..c1fd05d 100644 --- a/spdl/SPORE/yahalom-lowe.spdl +++ b/spdl/SPORE/yahalom-lowe.spdl @@ -10,7 +10,7 @@ secret k : Function; usertype SessionKey; -protocol yahalomLowe(I,R,S) +protocol yahalom-Lowe(I,R,S) { role I { @@ -54,7 +54,7 @@ protocol yahalomLowe(I,R,S) const Alice,Bob,Simon : Agent; -run yahalomLowe.I(Agent,Agent,s); -run yahalomLowe.I(Agent,Agent,s); -run yahalomLowe.R(Agent,Agent,s); +run yahalom-Lowe.I(Agent,Agent,s); +run yahalom-Lowe.I(Agent,Agent,s); +run yahalom-Lowe.R(Agent,Agent,s); diff --git a/spdl/SPORE/yahalom-paulson.spdl b/spdl/SPORE/yahalom-paulson.spdl index 5b122e0..be2e431 100644 --- a/spdl/SPORE/yahalom-paulson.spdl +++ b/spdl/SPORE/yahalom-paulson.spdl @@ -14,7 +14,7 @@ const Compromised: Function; usertype SessionKey; -protocol yahalomPaulsonSessionKeyCompromise(C) +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 @@ -36,7 +36,7 @@ protocol yahalomPaulsonSessionKeyCompromise(C) } -protocol yahalomPaulson(I,R,S) +protocol yahalom-Paulson(I,R,S) { role I { @@ -82,7 +82,7 @@ protocol yahalomPaulson(I,R,S) const Alice,Bob,Simon : Agent; -run yahalomPaulson.I(Agent,Agent,s); -run yahalomPaulson.I(Agent,Agent,s); -run yahalomPaulson.R(Agent,Agent,s); +run yahalom-Paulson.I(Agent,Agent,s); +run yahalom-Paulson.I(Agent,Agent,s); +run yahalom-Paulson.R(Agent,Agent,s); diff --git a/spdl/SPORE/yahalom.spdl b/spdl/SPORE/yahalom.spdl index 1a181ed..611ec3c 100644 --- a/spdl/SPORE/yahalom.spdl +++ b/spdl/SPORE/yahalom.spdl @@ -14,7 +14,7 @@ usertype SessionKey; const Fresh: Function; const Compromised: Function; -protocol yahalomSessionKeyCompromise(C) +protocol yahalom^KeyCompromise(C) { // Read the names of 3 agents and disclose a session between them including // corresponding session key to simulate key compromise