andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Update modeling of needham schroeder to better reflect the modelling in

Browse Source 
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.
This commit is contained in:
gijs 2005-08-15 13:31:48 +00:00
parent 1ee77472a0
commit 0f54f2ed23
36 changed files with 156 additions and 145 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
spdl/SPORE/andrew-ban-concrete.spdl
View File

@ -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 // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // 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 role I
@ -99,7 +99,7 @@ const kee: SessionKey;
# run andrewConcrete.R(Bob,Alice); # run andrewConcrete.R(Bob,Alice);
# This is the original scenario # This is the original scenario
run andrewConcrete.I(Agent,Agent); run andrew-Concrete.I(Agent,Agent);
run andrewConcrete.R(Agent,Agent); run andrew-Concrete.R(Agent,Agent);
run andrewConcrete.I(Agent,Agent); run andrew-Concrete.I(Agent,Agent);
run andrewConcrete.R(Agent,Agent); run andrew-Concrete.R(Agent,Agent);

12
spdl/SPORE/andrew-ban.spdl
View File

@ -16,7 +16,7 @@ secret k: Function;
const Fresh: Function; const Fresh: Function;
const Compromised: 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 // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // 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 role I
{ {
@ -84,7 +84,7 @@ compromised k(Eve,Bob);
compromised k(Alice,Eve); compromised k(Alice,Eve);
compromised k(Bob,Eve); compromised k(Bob,Eve);
run andrewBan.I(Agent,Agent); run andrew-Ban.I(Agent,Agent);
run andrewBan.R(Agent,Agent); run andrew-Ban.R(Agent,Agent);
run andrewBan.I(Agent,Agent); run andrew-Ban.I(Agent,Agent);
run andrewBan.R(Agent,Agent); run andrew-Ban.R(Agent,Agent);

12
spdl/SPORE/andrew-lowe-ban.spdl
View File

@ -23,7 +23,7 @@ secret k: Function;
const Fresh: Function; const Fresh: Function;
const Compromised: 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 // Read the names of 2 agents and disclose a session between them including
// corresponding session key to simulate key compromise // 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 role I
{ {
@ -89,7 +89,7 @@ compromised k(Bob,Eve);
run andrewLoweBan.I(Agent,Agent); run andrew-LoweBan.I(Agent,Agent);
run andrewLoweBan.R(Agent,Agent); run andrew-LoweBan.R(Agent,Agent);
run andrewLoweBan.I(Agent,Agent); run andrew-LoweBan.I(Agent,Agent);
run andrewLoweBan.R(Agent,Agent); run andrew-LoweBan.R(Agent,Agent);

2
spdl/SPORE/andrew.spdl
View File

@ -15,7 +15,7 @@ const succ: Function;
const Fresh: Function; const Fresh: Function;
const Compromised: Function; const Compromised: Function;
protocol andrewSessionKeyCompromise(C) protocol andrew^KeyCompromise(C)
{ {
// Read the names of 2 agents and disclose a session between them including // Read the names of 2 agents and disclose a session between them including
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise

10
spdl/SPORE/ccitt509-1.spdl
View File

@ -14,7 +14,7 @@ secret sk: Function;
inversekeys(pk,sk); inversekeys(pk,sk);
usertype Timestamp; usertype Timestamp;
protocol ccitt5091(I,R) protocol ccitt509-1(I,R)
{ {
role I role I
{ {
@ -45,7 +45,7 @@ compromised sk(Eve);
# General scenario, 2 parallel runs of the protocol # General scenario, 2 parallel runs of the protocol
run ccitt5091.I(Agent,Agent); run ccitt509-1.I(Agent,Agent);
run ccitt5091.R(Agent,Agent); run ccitt509-1.R(Agent,Agent);
run ccitt5091.I(Agent,Agent); run ccitt509-1.I(Agent,Agent);
run ccitt5091.R(Agent,Agent); run ccitt509-1.R(Agent,Agent);

10
spdl/SPORE/ccitt509-1c.spdl
View File

@ -13,7 +13,7 @@ inversekeys (hash,unhash);
inversekeys(pk,sk); inversekeys(pk,sk);
usertype Timestamp; usertype Timestamp;
protocol ccitt5091c(I,R) protocol ccitt509-1c(I,R)
{ {
role I role I
{ {
@ -44,7 +44,7 @@ compromised sk(Eve);
# General scenario, 2 parallel runs of the protocol # General scenario, 2 parallel runs of the protocol
run ccitt5091c.I(Agent,Agent); run ccitt509-1c.I(Agent,Agent);
run ccitt5091c.R(Agent,Agent); run ccitt509-1c.R(Agent,Agent);
run ccitt5091c.I(Agent,Agent); run ccitt509-1c.I(Agent,Agent);
run ccitt5091c.R(Agent,Agent); run ccitt509-1c.R(Agent,Agent);

10
spdl/SPORE/ccitt509-3.spdl
View File

@ -13,7 +13,7 @@ secret sk: Function;
inversekeys(pk,sk); inversekeys(pk,sk);
usertype Timestamp; usertype Timestamp;
protocol ccitt5093(I,R) protocol ccitt509-3(I,R)
{ {
role I role I
{ {
@ -56,7 +56,7 @@ compromised sk(Eve);
# General scenario, 2 parallel runs of the protocol # General scenario, 2 parallel runs of the protocol
run ccitt5093.I(Agent,Agent); run ccitt509-3.I(Agent,Agent);
run ccitt5093.R(Agent,Agent); run ccitt509-3.R(Agent,Agent);
run ccitt5093.I(Agent,Agent); run ccitt509-3.I(Agent,Agent);
run ccitt5093.R(Agent,Agent); run ccitt509-3.R(Agent,Agent);

10
spdl/SPORE/ccitt509-ban3.spdl
View File

@ -15,7 +15,7 @@ const pk: Function;
secret sk: Function; secret sk: Function;
inversekeys(pk,sk); inversekeys(pk,sk);
protocol ccitt509ban3(I,R) protocol ccitt509-ban3(I,R)
{ {
role I role I
{ {
@ -49,7 +49,7 @@ compromised sk(Eve);
# General scenario, 2 parallel runs of the protocol # General scenario, 2 parallel runs of the protocol
run ccitt509ban3.I(Agent,Agent); run ccitt509-ban3.I(Agent,Agent);
run ccitt509ban3.R(Agent,Agent); run ccitt509-ban3.R(Agent,Agent);
run ccitt509ban3.I(Agent,Agent); run ccitt509-ban3.I(Agent,Agent);
run ccitt509ban3.R(Agent,Agent); run ccitt509-ban3.R(Agent,Agent);

18
spdl/SPORE/denning-sacco-lowe.spdl
View File

@ -21,14 +21,14 @@ const dec: PseudoFunction;
const Fresh: Function; const Fresh: Function;
const Compromised: 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 // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise
role C { role C {
const Ni,Nr: Nonce; const Ni,Nr: Nonce;
const Kir: SessionKey; const Kir: SessionKey;
const T: ExpiredTimeStamp; const T: TimeStamp;
var I,R,S: Agent; var I,R,S: Agent;
read_C1(C,C, I,R,S); 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 role I
{ {
@ -102,9 +102,9 @@ compromised k(Eve,Simon);
# Note because the modelchecker does not support tickets this might not # Note because the modelchecker does not support tickets this might not
# be very useful # be very useful
run denningSaccoLowe.I(Agent,Agent,Simon); run denningSacco-Lowe.I(Agent,Agent,Simon);
run denningSaccoLowe.R(Agent,Agent,Simon); run denningSacco-Lowe.R(Agent,Agent,Simon);
run denningSaccoLowe.S(Agent,Agent,Simon); run denningSacco-Lowe.S(Agent,Agent,Simon);
run denningSaccoLowe.I(Agent,Agent,Simon); run denningSacco-Lowe.I(Agent,Agent,Simon);
run denningSaccoLowe.R(Agent,Agent,Simon); run denningSacco-Lowe.R(Agent,Agent,Simon);
run denningSaccoLowe.S(Agent,Agent,Simon); run denningSacco-Lowe.S(Agent,Agent,Simon);

2
spdl/SPORE/denning-sacco.spdl
View File

@ -16,7 +16,7 @@ secret k: Function;
const Fresh: Function; const Fresh: Function;
const Compromised: Function; const Compromised: Function;
protocol denningSaccoSessionKeyCompromise(C) protocol denningSacco^KeyCompromise(C)
{ {
// Read the names of 3 agents and disclose a session between them including // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise

16
spdl/SPORE/kaochow-v2.spdl
View File

@ -13,7 +13,7 @@ secret k: Function;
const Fresh: Function; const Fresh: Function;
const Compromised: 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 // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // 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 role I
{ {
@ -95,9 +95,9 @@ compromised k(Alice,Eve);
compromised k(Bob,Eve); compromised k(Bob,Eve);
compromised k(Simon,Eve); compromised k(Simon,Eve);
run kaochow2.I(Agent,Agent,Simon); run kaochow-2.I(Agent,Agent,Simon);
run kaochow2.R(Agent,Agent,Simon); run kaochow-2.R(Agent,Agent,Simon);
run kaochow2.S(Agent,Agent,Simon); run kaochow-2.S(Agent,Agent,Simon);
run kaochow2.I(Agent,Agent,Simon); run kaochow-2.I(Agent,Agent,Simon);
run kaochow2.R(Agent,Agent,Simon); run kaochow-2.R(Agent,Agent,Simon);
run kaochow2.S(Agent,Agent,Simon); run kaochow-2.S(Agent,Agent,Simon);

16
spdl/SPORE/kaochow-v3.spdl
View File

@ -15,7 +15,7 @@ secret k: Function;
const Fresh: Function; const Fresh: Function;
const Compromised: 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 // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // 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 role I
{ {
@ -102,9 +102,9 @@ compromised k(Alice,Eve);
compromised k(Bob,Eve); compromised k(Bob,Eve);
compromised k(Simon,Eve); compromised k(Simon,Eve);
run kaochow3.I(Agent,Agent,Simon); run kaochow-3.I(Agent,Agent,Simon);
run kaochow3.R(Agent,Agent,Simon); run kaochow-3.R(Agent,Agent,Simon);
run kaochow3.S(Agent,Agent,Simon); run kaochow-3.S(Agent,Agent,Simon);
run kaochow3.I(Agent,Agent,Simon); run kaochow-3.I(Agent,Agent,Simon);
run kaochow3.R(Agent,Agent,Simon); run kaochow-3.R(Agent,Agent,Simon);
run kaochow3.S(Agent,Agent,Simon); run kaochow-3.S(Agent,Agent,Simon);

2
spdl/SPORE/kaochow.spdl
View File

@ -13,7 +13,7 @@ secret k: Function;
const Fresh: Function; const Fresh: Function;
const Compromised: Function; const Compromised: Function;
protocol kaochowSessionKeyCompromise(C) protocol kaochow^KeyCompromise(C)
{ {
// Read the names of 3 agents and disclose a session between them including // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise

10
spdl/SPORE/ksl-lowe.spdl
View File

@ -26,7 +26,7 @@ const kee: SessionKey;
untrusted e; untrusted e;
compromised k(e,s); 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 // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // 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 role A
{ {
@ -112,7 +112,7 @@ protocol kslLowe(A,B,S)
} }
} }
run kslLowe.A(a,b,s); run ksl-Lowe.A(a,b,s);
run kslLowe.B(a,b,s); run ksl-Lowe.B(a,b,s);
run kslLowe.S(a,b,s); run ksl-Lowe.S(a,b,s);

2
spdl/SPORE/ksl.spdl
View File

@ -23,7 +23,7 @@ const kee: SessionKey;
untrusted e; untrusted e;
compromised k(e,s); compromised k(e,s);
protocol kslSessionKeyCompromise(C) protocol ksl^KeyCompromise(C)
{ {
// Read the names of 3 agents and disclose a session between them including // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise

21
spdl/SPORE/needham-schroeder-lowe.spdl
View File

@ -10,11 +10,12 @@
# synchronisation and agreement, because the keys that the server sends # synchronisation and agreement, because the keys that the server sends
# out can be replayed. # 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; secret sk: Function;
inversekeys(pk,sk); inversekeys(pk,sk);
protocol needhamschroederpkLowe(I,R,S) protocol needhamschroederpk-Lowe(I,R,S)
{ {
role I role I
{ {
@ -28,6 +29,7 @@ protocol needhamschroederpkLowe(I,R,S)
send_7(I,R, {Nr}pk(R)); send_7(I,R, {Nr}pk(R));
claim_I1(I,Secret,Ni); claim_I1(I,Secret,Ni);
claim_I2(I,Secret,Nr); claim_I2(I,Secret,Nr);
claim_I3(I,Nisynch);
} }
role R role R
@ -42,6 +44,7 @@ protocol needhamschroederpkLowe(I,R,S)
read_7(I,R,{Nr}pk(R)); read_7(I,R,{Nr}pk(R));
claim_R1(R,Secret,Nr); claim_R1(R,Secret,Nr);
claim_R2(R,Secret,Ni); claim_R2(R,Secret,Ni);
claim_R3(R,Nisynch);
} }
role S role S
@ -58,12 +61,14 @@ const Alice,Bob,Simon,Eve: Agent;
untrusted Eve; untrusted Eve;
const ne: Nonce; const ne: Nonce;
compromised sk(Eve); 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 # General scenario, 2 parallel runs of the protocol
run needhamschroederpkLowe.I(Agent,Agent,Simon); run needhamschroederpk-Lowe.I(Agent,Agent,Simon);
run needhamschroederpkLowe.S(Agent,Agent,Simon); run needhamschroederpk-Lowe.S(Agent,Agent,Simon);
run needhamschroederpkLowe.R(Agent,Agent,Simon); run needhamschroederpk-Lowe.R(Agent,Agent,Simon);
run needhamschroederpkLowe.I(Agent,Agent,Simon); run needhamschroederpk-Lowe.I(Agent,Agent,Simon);
run needhamschroederpkLowe.R(Agent,Agent,Simon); run needhamschroederpk-Lowe.R(Agent,Agent,Simon);
run needhamschroederpkLowe.S(Agent,Agent,Simon); run needhamschroederpk-Lowe.S(Agent,Agent,Simon);

16
spdl/SPORE/needham-schroeder-sk-amend.spdl
View File

@ -22,7 +22,7 @@ usertype SessionKey;
const Fresh: Function; const Fresh: Function;
const Compromised: 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 // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // 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 role I
{ {
@ -100,9 +100,9 @@ compromised k(Eve,Simon);
# General scenario, 2 parallel runs of the protocol # General scenario, 2 parallel runs of the protocol
run needhamschroederskamend.I(Agent,Agent,Simon); run needhamschroedersk-amend.I(Agent,Agent,Simon);
run needhamschroederskamend.R(Agent,Agent,Simon); run needhamschroedersk-amend.R(Agent,Agent,Simon);
run needhamschroederskamend.S(Agent,Agent,Simon); run needhamschroedersk-amend.S(Agent,Agent,Simon);
run needhamschroederskamend.I(Agent,Agent,Simon); run needhamschroedersk-amend.I(Agent,Agent,Simon);
run needhamschroederskamend.R(Agent,Agent,Simon); run needhamschroedersk-amend.R(Agent,Agent,Simon);
run needhamschroederskamend.S(Agent,Agent,Simon); run needhamschroedersk-amend.S(Agent,Agent,Simon);

2
spdl/SPORE/needham-schroeder-sk.spdl
View File

@ -18,7 +18,7 @@ usertype SessionKey;
const Fresh: Function; const Fresh: Function;
const Compromised: Function; const Compromised: Function;
protocol needhamschroederSessionKeyCompromise(C) protocol needhamschroedersk^KeyCompromise(C)
{ {
// Read the names of 3 agents and disclose a session between them including // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise

8
spdl/SPORE/needham-schroeder.spdl
View File

@ -10,7 +10,8 @@
# synchronisation and agreement, because the keys that the server sends # synchronisation and agreement, because the keys that the server sends
# out can be replayed. # 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; secret sk: Function;
inversekeys(pk,sk); inversekeys(pk,sk);
@ -28,6 +29,7 @@ protocol needhamschroederpk(I,R,S)
send_7(I,R, {Nr}pk(R)); send_7(I,R, {Nr}pk(R));
claim_I1(I,Secret,Ni); claim_I1(I,Secret,Ni);
claim_I2(I,Secret,Nr); claim_I2(I,Secret,Nr);
claim_I3(I,Nisynch);
} }
role R role R
@ -42,6 +44,7 @@ protocol needhamschroederpk(I,R,S)
read_7(I,R,{Nr}pk(R)); read_7(I,R,{Nr}pk(R));
claim_R1(R,Secret,Nr); claim_R1(R,Secret,Nr);
claim_R2(R,Secret,Ni); claim_R2(R,Secret,Ni);
claim_R3(R,Nisynch);
} }
role S role S
@ -58,6 +61,9 @@ const Alice,Bob,Simon,Eve: Agent;
untrusted Eve; untrusted Eve;
const ne: Nonce; const ne: Nonce;
compromised sk(Eve); 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 # General scenario, 2 parallel runs of the protocol

10
spdl/SPORE/neumannstub-hwang.spdl
View File

@ -26,7 +26,7 @@ const kee: SessionKey;
untrusted e; untrusted e;
compromised k(e,s); 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 // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // 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 role I
{ {
@ -106,7 +106,7 @@ protocol neustubHwang(I,R,S)
} }
} }
run neustubHwang.A(a,b,s); run neustub-Hwang.A(a,b,s);
run neustubHwang.B(a,b,s); run neustub-Hwang.B(a,b,s);
run neustubHwang.S(a,b,s); run neustub-Hwang.S(a,b,s);

4
spdl/SPORE/neumannstub.spdl
View File

@ -25,7 +25,7 @@ const kee: SessionKey;
untrusted Eve; untrusted Eve;
compromised k(Eve,Simon); compromised k(Eve,Simon);
protocol neustubSessionKeyCompromise(C) protocol neustub^KeyCompromise(C)
{ {
// Read the names of 3 agents and disclose a session between them including // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // 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; const Kir: SessionKey;

2
spdl/SPORE/otwayrees.spdl
View File

@ -16,7 +16,7 @@ const Compromised: Function;
usertype String,SessionKey; usertype String,SessionKey;
protocol otwayReesSessionKeyCompromise(C) protocol otwayRees^KeyCompromise(C)
{ {
// Read the names of 3 agents and disclose a session between them including // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise

8
spdl/SPORE/splice-as-cj.spdl
View File

@ -18,7 +18,7 @@ inversekeys (pk,sk);
const inc,dec: Function; const inc,dec: Function;
inversekeys (inc,dec); inversekeys (inc,dec);
protocol spliceASCJ(I,R,S) protocol spliceAS-CJ(I,R,S)
{ {
role I role I
{ {
@ -73,9 +73,9 @@ untrusted Eve;
const ne: Nonce; const ne: Nonce;
compromised sk(Eve); compromised sk(Eve);
run spliceASCJ.I(Agent,Agent,Agent); run spliceAS-CJ.I(Agent,Agent,Agent);
run spliceASCJ.R(Agent,Agent,Agent); run spliceAS-CJ.R(Agent,Agent,Agent);
run spliceASCJ.S(Agent,Agent,Agent); run spliceAS-CJ.S(Agent,Agent,Agent);
#run spliceASCJ.I(Alice,Bob,Simon); #run spliceASCJ.I(Alice,Bob,Simon);
#run spliceASCJ.R(Alice,Bob,Simon); #run spliceASCJ.R(Alice,Bob,Simon);

8
spdl/SPORE/splice-as-hc.spdl
View File

@ -13,7 +13,7 @@ inversekeys (pk,sk);
const inc,dec: Function; const inc,dec: Function;
inversekeys (inc,dec); inversekeys (inc,dec);
protocol spliceASHC(I,R,S) protocol spliceAS-HC(I,R,S)
{ {
role I role I
{ {
@ -72,8 +72,8 @@ compromised sk(Eve);
#run spliceASHC.R(Alice,Bob,Simon); #run spliceASHC.R(Alice,Bob,Simon);
#run spliceASHC.S(Alice,Bob,Simon); #run spliceASHC.S(Alice,Bob,Simon);
run spliceASHC.I(Agent,Agent,Agent); run spliceAS-HC.I(Agent,Agent,Agent);
run spliceASHC.R(Agent,Agent,Agent); run spliceAS-HC.R(Agent,Agent,Agent);
run spliceASHC.S(Agent,Agent,Agent); run spliceAS-HC.S(Agent,Agent,Agent);

2
spdl/SPORE/tmn.spdl
View File

@ -14,7 +14,7 @@ inversekeys(pk,sk);
const Fresh: Function; const Fresh: Function;
const Compromised: Function; const Compromised: Function;
protocol tmnSessionKeyCompromise(C) protocol tmn^KeyCompromise(C)
{ {
// Read the names of 3 agents and disclose a session between them including // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise

10
spdl/SPORE/wmf-lowe.spdl
View File

@ -19,7 +19,7 @@ const Compromised: Function;
secret k: 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 // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // 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 role I
{ {
@ -92,9 +92,9 @@ const Te: TimeStamp;
untrusted Eve; untrusted Eve;
compromised k(Eve,Simon); compromised k(Eve,Simon);
run wmfLowe.I (Agent,Agent,Simon); run wmf-Lowe.I (Agent,Agent,Simon);
run wmfLowe.R (Agent,Agent,Simon); run wmf-Lowe.R (Agent,Agent,Simon);
run wmfLowe.S (Agent,Agent,Simon); run wmf-Lowe.S (Agent,Agent,Simon);

2
spdl/SPORE/wmf.spdl
View File

@ -16,7 +16,7 @@ secret k: Function;
const Fresh: Function; const Fresh: Function;
const Compromised: Function; const Compromised: Function;
protocol wmfSessionKeyCompromise(C) protocol wmf^KeyCompromise(C)
{ {
// Read the names of 3 agents and disclose a session between them including // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise

8
spdl/SPORE/woo-lam-pi-1.spdl
View File

@ -10,7 +10,7 @@
secret k: Function; secret k: Function;
protocol woolamPi1(I,R,S) protocol woolamPi-1(I,R,S)
{ {
role I role I
{ {
@ -53,9 +53,9 @@ const Ne: Nonce;
untrusted Eve; untrusted Eve;
compromised k(Eve,Simon); compromised k(Eve,Simon);
run woolamPi1.I (Agent,Agent,Simon); run woolamPi-1.I (Agent,Agent,Simon);
run woolamPi1.R (Agent,Agent,Simon); run woolamPi-1.R (Agent,Agent,Simon);
run woolamPi1.S (Agent,Agent,Simon); run woolamPi-1.S (Agent,Agent,Simon);

8
spdl/SPORE/woo-lam-pi-2.spdl
View File

@ -10,7 +10,7 @@
secret k: Function; secret k: Function;
protocol woolamPi2(I,R,S) protocol woolamPi-2(I,R,S)
{ {
role I role I
{ {
@ -53,9 +53,9 @@ const Ne: Nonce;
untrusted Eve; untrusted Eve;
compromised k(Eve,Simon); compromised k(Eve,Simon);
run woolamPi2.I (Agent,Agent,Simon); run woolamPi-2.I (Agent,Agent,Simon);
run woolamPi2.R (Agent,Agent,Simon); run woolamPi-2.R (Agent,Agent,Simon);
run woolamPi2.S (Agent,Agent,Simon); run woolamPi-2.S (Agent,Agent,Simon);

8
spdl/SPORE/woo-lam-pi-3.spdl
View File

@ -10,7 +10,7 @@
secret k: Function; secret k: Function;
protocol woolamPi3(I,R,S) protocol woolamPi-3(I,R,S)
{ {
role I role I
{ {
@ -53,9 +53,9 @@ const Ne: Nonce;
untrusted Eve; untrusted Eve;
compromised k(Eve,Simon); compromised k(Eve,Simon);
run woolamPi3.I (Agent,Agent,Simon); run woolamPi-3.I (Agent,Agent,Simon);
run woolamPi3.R (Agent,Agent,Simon); run woolamPi-3.R (Agent,Agent,Simon);
run woolamPi3.S (Agent,Agent,Simon); run woolamPi-3.S (Agent,Agent,Simon);

8
spdl/SPORE/woo-lam-pi-f.spdl
View File

@ -10,7 +10,7 @@
secret k: Function; secret k: Function;
protocol woolamPif(I,R,S) protocol woolamPi-f(I,R,S)
{ {
role I role I
{ {
@ -53,7 +53,7 @@ const Ne: Nonce;
untrusted Eve; untrusted Eve;
compromised k(Eve,Simon); compromised k(Eve,Simon);
run woolamPif.I (Agent,Agent,Simon); run woolamPi-f.I (Agent,Agent,Simon);
run woolamPif.R (Agent,Agent,Simon); run woolamPi-f.R (Agent,Agent,Simon);
run woolamPif.S (Agent,Agent,Simon); run woolamPi-f.S (Agent,Agent,Simon);

2
spdl/SPORE/woo-lam.spdl
View File

@ -15,7 +15,7 @@ secret k: Function;
const Fresh: Function; const Fresh: Function;
const Compromised: Function; const Compromised: Function;
protocol woolamSessionKeyCompromise(C) protocol woolam^KeyCompromise(C)
{ {
// Read the names of 3 agents and disclose a session between them including // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise

10
spdl/SPORE/yahalom-ban.spdl
View File

@ -14,7 +14,7 @@ usertype SessionKey;
const Fresh: Function; const Fresh: Function;
const Compromised: 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 // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // 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 role I
{ {
@ -83,7 +83,7 @@ protocol yahalomBAN(I,R,S)
const Alice,Bob,Simon : Agent; const Alice,Bob,Simon : Agent;
run yahalomBAN.I(Agent,Agent,s); run yahalom-BAN.I(Agent,Agent,s);
run yahalomBAN.I(Agent,Agent,s); run yahalom-BAN.I(Agent,Agent,s);
run yahalomBAN.R(Agent,Agent,s); run yahalom-BAN.R(Agent,Agent,s);

8
spdl/SPORE/yahalom-lowe.spdl
View File

@ -10,7 +10,7 @@ secret k : Function;
usertype SessionKey; usertype SessionKey;
protocol yahalomLowe(I,R,S) protocol yahalom-Lowe(I,R,S)
{ {
role I role I
{ {
@ -54,7 +54,7 @@ protocol yahalomLowe(I,R,S)
const Alice,Bob,Simon : Agent; const Alice,Bob,Simon : Agent;
run yahalomLowe.I(Agent,Agent,s); run yahalom-Lowe.I(Agent,Agent,s);
run yahalomLowe.I(Agent,Agent,s); run yahalom-Lowe.I(Agent,Agent,s);
run yahalomLowe.R(Agent,Agent,s); run yahalom-Lowe.R(Agent,Agent,s);

10
spdl/SPORE/yahalom-paulson.spdl
View File

@ -14,7 +14,7 @@ const Compromised: Function;
usertype SessionKey; usertype SessionKey;
protocol yahalomPaulsonSessionKeyCompromise(C) protocol yahalom-Paulson^KeyCompromise(C)
{ {
// Read the names of 3 agents and disclose a session between them including // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // 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 role I
{ {
@ -82,7 +82,7 @@ protocol yahalomPaulson(I,R,S)
const Alice,Bob,Simon : Agent; const Alice,Bob,Simon : Agent;
run yahalomPaulson.I(Agent,Agent,s); run yahalom-Paulson.I(Agent,Agent,s);
run yahalomPaulson.I(Agent,Agent,s); run yahalom-Paulson.I(Agent,Agent,s);
run yahalomPaulson.R(Agent,Agent,s); run yahalom-Paulson.R(Agent,Agent,s);

2
spdl/SPORE/yahalom.spdl
View File

@ -14,7 +14,7 @@ usertype SessionKey;
const Fresh: Function; const Fresh: Function;
const Compromised: Function; const Compromised: Function;
protocol yahalomSessionKeyCompromise(C) protocol yahalom^KeyCompromise(C)
{ {
// Read the names of 3 agents and disclose a session between them including // Read the names of 3 agents and disclose a session between them including
// corresponding session key to simulate key compromise // corresponding session key to simulate key compromise