diff --git a/gui/Scyther/Bin/scyther-linux b/gui/Scyther/Bin/scyther-linux index 65e7e3e..0547a42 100755 Binary files a/gui/Scyther/Bin/scyther-linux and b/gui/Scyther/Bin/scyther-linux differ diff --git a/gui/Scyther/Bin/scyther-w32.exe b/gui/Scyther/Bin/scyther-w32.exe index 4c452c8..c33dd00 100755 Binary files a/gui/Scyther/Bin/scyther-w32.exe and b/gui/Scyther/Bin/scyther-w32.exe differ diff --git a/spdl/SPORE/andrew-ban-concrete.spdl b/spdl/SPORE/andrew-ban-concrete.spdl index d008d6b..2fbab12 100644 --- a/spdl/SPORE/andrew-ban-concrete.spdl +++ b/spdl/SPORE/andrew-ban-concrete.spdl @@ -28,8 +28,8 @@ protocol @swapkey(X) { var I,R: Agent; var T:Ticket; - read_X1(X,X,I,R,{T}k(I,R)); - send_X2(X,X,{T}k(R,I)); + read_!X1(X,X,I,R,{T}k(I,R)); + send_!X2(X,X,{T}k(R,I)); } } @@ -42,8 +42,8 @@ protocol andrew-Concrete^KeyCompromise(C) const kir: SessionKey; var I,R: Agent; - read_C1(C,C, I,R); - send_C2(C,C, (I,ni), + read_!C1(C,C, I,R); + send_!C2(C,C, (I,ni), {ni,kir}k(I,R), {ni}kir, nr, diff --git a/spdl/SPORE/andrew-ban.spdl b/spdl/SPORE/andrew-ban.spdl index 01dff68..8fb918d 100644 --- a/spdl/SPORE/andrew-ban.spdl +++ b/spdl/SPORE/andrew-ban.spdl @@ -25,8 +25,8 @@ protocol andrew-Ban^KeyCompromise(C) const kir: SessionKey; var I,R: Agent; - read_C1(C,C, I,R); - send_C2(C,C, (I,{ni}k(I,R)), + 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), diff --git a/spdl/SPORE/andrew-lowe-ban.spdl b/spdl/SPORE/andrew-lowe-ban.spdl index 0958dd8..57785be 100644 --- a/spdl/SPORE/andrew-lowe-ban.spdl +++ b/spdl/SPORE/andrew-lowe-ban.spdl @@ -32,8 +32,8 @@ protocol andrew-LoweBan^KeyCompromise(C) const kir: SessionKey; var I,R: Agent; - read_C1(C,C, I,R); - send_C2(C,C, (I,ni), + read_!C1(C,C, I,R); + send_!C2(C,C, (I,ni), {ni,kir,R}k(I,R), {ni}kir, nr, diff --git a/spdl/SPORE/andrew.spdl b/spdl/SPORE/andrew.spdl index f56f43d..d7b006f 100644 --- a/spdl/SPORE/andrew.spdl +++ b/spdl/SPORE/andrew.spdl @@ -24,8 +24,8 @@ protocol andrew^KeyCompromise(C) const kir: SessionKey; var I,R: Agent; - read_C1(C,C, I,R); - send_C2(C,C, (I,{ni}k(I,R)), + 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), diff --git a/spdl/SPORE/denning-sacco-lowe.spdl b/spdl/SPORE/denning-sacco-lowe.spdl index b5d0608..e5cbd1b 100644 --- a/spdl/SPORE/denning-sacco-lowe.spdl +++ b/spdl/SPORE/denning-sacco-lowe.spdl @@ -27,8 +27,8 @@ protocol denningSacco-Lowe^KeyCompromise(C) const T: ExpiredTimeStamp; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, (I,R), + 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, diff --git a/spdl/SPORE/denning-sacco.spdl b/spdl/SPORE/denning-sacco.spdl index c725048..52f2f45 100644 --- a/spdl/SPORE/denning-sacco.spdl +++ b/spdl/SPORE/denning-sacco.spdl @@ -22,8 +22,8 @@ protocol denningSacco^KeyCompromise(C) const T: ExpiredTimeStamp; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, (I,R), + 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 diff --git a/spdl/SPORE/kaochow-v2.spdl b/spdl/SPORE/kaochow-v2.spdl index 731fe3a..2ce4f02 100644 --- a/spdl/SPORE/kaochow-v2.spdl +++ b/spdl/SPORE/kaochow-v2.spdl @@ -18,8 +18,8 @@ protocol kaochow-2^KeyCompromise(C) const Kir,Kt: SessionKey; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, (I,R,Ni), + 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, diff --git a/spdl/SPORE/kaochow-v3.spdl b/spdl/SPORE/kaochow-v3.spdl index 7569ded..18d4d3d 100644 --- a/spdl/SPORE/kaochow-v3.spdl +++ b/spdl/SPORE/kaochow-v3.spdl @@ -21,8 +21,8 @@ protocol kaochow-3^KeyCompromise(C) const T2: ExpiredTimeStamp; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, (I,R,Ni), + 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, diff --git a/spdl/SPORE/kaochow.spdl b/spdl/SPORE/kaochow.spdl index 0657aed..1e2e91e 100644 --- a/spdl/SPORE/kaochow.spdl +++ b/spdl/SPORE/kaochow.spdl @@ -18,8 +18,8 @@ protocol kaochow^KeyCompromise(C) const Kir: SessionKey; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, (I,R,Ni), + 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, diff --git a/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl b/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl index 9be70bf..c461405 100644 --- a/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl +++ b/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl @@ -27,8 +27,8 @@ protocol needhamschroederSessionKeyCompromise(C) const Kir: SessionKey; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, (I,R,Ni), + 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, diff --git a/spdl/SPORE/ksl-lowe.spdl b/spdl/SPORE/ksl-lowe.spdl index 662e9e9..226899c 100644 --- a/spdl/SPORE/ksl-lowe.spdl +++ b/spdl/SPORE/ksl-lowe.spdl @@ -33,8 +33,8 @@ protocol ksl-Lowe^KeyCompromise(C) const Tr: ExpiredTimeStamp; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, (Ni,I), + 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), diff --git a/spdl/SPORE/needham-schroeder-sk-amend.spdl b/spdl/SPORE/needham-schroeder-sk-amend.spdl index d593fd7..739d4ce 100644 --- a/spdl/SPORE/needham-schroeder-sk-amend.spdl +++ b/spdl/SPORE/needham-schroeder-sk-amend.spdl @@ -27,8 +27,8 @@ protocol needhamschroedersk-amend^KeyCompromise(C) const Kir: SessionKey; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, I, + 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), diff --git a/spdl/SPORE/needham-schroeder-sk.spdl b/spdl/SPORE/needham-schroeder-sk.spdl index 7ccee65..8beed6a 100644 --- a/spdl/SPORE/needham-schroeder-sk.spdl +++ b/spdl/SPORE/needham-schroeder-sk.spdl @@ -23,8 +23,8 @@ protocol needhamschroedersk^KeyCompromise(C) const Kir: SessionKey; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, (I,R,Ni), + 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, diff --git a/spdl/SPORE/neumannstub-hwang.spdl b/spdl/SPORE/neumannstub-hwang.spdl index 2a79550..1f402db 100644 --- a/spdl/SPORE/neumannstub-hwang.spdl +++ b/spdl/SPORE/neumannstub-hwang.spdl @@ -32,8 +32,8 @@ protocol neustub-Hwang^KeyCompromise(C) const Tr: ExpiredTimeStamp; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, I,Ni, + 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, diff --git a/spdl/SPORE/neumannstub-keycompromise.spdl b/spdl/SPORE/neumannstub-keycompromise.spdl index 5dd1aeb..d1e4784 100644 --- a/spdl/SPORE/neumannstub-keycompromise.spdl +++ b/spdl/SPORE/neumannstub-keycompromise.spdl @@ -31,8 +31,8 @@ protocol neustub^KeyCompromise(C) const Tr: ExpiredTimeStamp; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, I,Ni, + 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, diff --git a/spdl/SPORE/otwayrees.spdl b/spdl/SPORE/otwayrees.spdl index 3d1c4b1..5aa87df 100644 --- a/spdl/SPORE/otwayrees.spdl +++ b/spdl/SPORE/otwayrees.spdl @@ -21,8 +21,8 @@ protocol otwayRees^KeyCompromise(C) 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), + 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 diff --git a/spdl/SPORE/tmn.spdl b/spdl/SPORE/tmn.spdl index 59e2736..51e5b7f 100644 --- a/spdl/SPORE/tmn.spdl +++ b/spdl/SPORE/tmn.spdl @@ -23,8 +23,8 @@ protocol tmn^KeyCompromise(C) const Kr,Ki: SessionKey; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, R,{Ki}pk(S), + read_!C1(C,C, I,R,S); + send_!C2(C,C, R,{Ki}pk(S), I, {Kr}pk(S), {Kr}Ki, Kr diff --git a/spdl/SPORE/wmf-lowe.spdl b/spdl/SPORE/wmf-lowe.spdl index 0dbade1..58cf2f8 100644 --- a/spdl/SPORE/wmf-lowe.spdl +++ b/spdl/SPORE/wmf-lowe.spdl @@ -29,8 +29,8 @@ protocol wmf-Lowe^KeyCompromise(C) 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), + 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, diff --git a/spdl/SPORE/wmf.spdl b/spdl/SPORE/wmf.spdl index 80ae8f2..1c6ad7d 100644 --- a/spdl/SPORE/wmf.spdl +++ b/spdl/SPORE/wmf.spdl @@ -26,8 +26,8 @@ protocol wmf^KeyCompromise(C) 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), + 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 ); diff --git a/spdl/SPORE/woo-lam.spdl b/spdl/SPORE/woo-lam.spdl index a60ad71..685d95e 100644 --- a/spdl/SPORE/woo-lam.spdl +++ b/spdl/SPORE/woo-lam.spdl @@ -20,8 +20,8 @@ protocol woolam^KeyCompromise(C) const Kir: SessionKey; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, I,N1, + 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), diff --git a/spdl/SPORE/yahalom-ban.spdl b/spdl/SPORE/yahalom-ban.spdl index c6908af..d2047ef 100644 --- a/spdl/SPORE/yahalom-ban.spdl +++ b/spdl/SPORE/yahalom-ban.spdl @@ -19,8 +19,8 @@ protocol yahalom-BAN^KeyCompromise(C) const Kir: SessionKey; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, I,Ni, + 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), diff --git a/spdl/SPORE/yahalom-paulson.spdl b/spdl/SPORE/yahalom-paulson.spdl index 86cb67e..0295038 100644 --- a/spdl/SPORE/yahalom-paulson.spdl +++ b/spdl/SPORE/yahalom-paulson.spdl @@ -11,26 +11,26 @@ 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^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) diff --git a/spdl/SPORE/yahalom.spdl b/spdl/SPORE/yahalom.spdl index f8c05bf..a8a9d96 100644 --- a/spdl/SPORE/yahalom.spdl +++ b/spdl/SPORE/yahalom.spdl @@ -20,8 +20,8 @@ protocol yahalom^KeyCompromise(C) const Kir: SessionKey; var I,R,S: Agent; - read_C1(C,C, I,R,S); - send_C2(C,C, I,Ni, + 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), diff --git a/spdl/misc/bkepk-ce2.spdl b/spdl/misc/bkepk-ce2.spdl index 0e50a55..09879bf 100644 --- a/spdl/misc/bkepk-ce2.spdl +++ b/spdl/misc/bkepk-ce2.spdl @@ -40,7 +40,7 @@ protocol bkepkCE2(A,B,testnonce) { var n: Nonce; - read_4 (testnonce,testnonce, n); + read_!4 (testnonce,testnonce, n); } } diff --git a/spdl/misc/bunava-1-3.spdl b/spdl/misc/bunava-1-3.spdl index 0bae140..17858d1 100644 --- a/spdl/misc/bunava-1-3.spdl +++ b/spdl/misc/bunava-1-3.spdl @@ -20,8 +20,8 @@ protocol intruderhelp(Swap) var T: Ticket; var R0,R1: Agent; - read_1(Swap,Swap, { T }k(R0,R1) ); - send_2(Swap,Swap, { T }k(R1,R0) ); + read_!1(Swap,Swap, { T }k(R0,R1) ); + send_!2(Swap,Swap, { T }k(R1,R0) ); } } diff --git a/spdl/misc/bunava-1-4.spdl b/spdl/misc/bunava-1-4.spdl index 8e69760..b858e5a 100644 --- a/spdl/misc/bunava-1-4.spdl +++ b/spdl/misc/bunava-1-4.spdl @@ -21,8 +21,8 @@ protocol intruderhelp(Swap) var T: Ticket; var A,B: Agent; - read_1(Swap,Swap, { T }k(A,B) ); - send_2(Swap,Swap, { T }k(B,A) ); + read_!1(Swap,Swap, { T }k(A,B) ); + send_!2(Swap,Swap, { T }k(B,A) ); } } diff --git a/spdl/misc/bunava-2-3.spdl b/spdl/misc/bunava-2-3.spdl index 76224e1..2ecf955 100644 --- a/spdl/misc/bunava-2-3.spdl +++ b/spdl/misc/bunava-2-3.spdl @@ -16,8 +16,8 @@ protocol intruderhelp(Swap) var T: Ticket; var R0,R1: Agent; - read_1(Swap,Swap, { T }k(R0,R1) ); - send_2(Swap,Swap, { T }k(R1,R0) ); + read_!1(Swap,Swap, { T }k(R0,R1) ); + send_!2(Swap,Swap, { T }k(R1,R0) ); } } diff --git a/spdl/misc/f4.spdl b/spdl/misc/f4.spdl index b34a06f..eb1d54f 100644 --- a/spdl/misc/f4.spdl +++ b/spdl/misc/f4.spdl @@ -19,17 +19,17 @@ protocol f4(I,R) { var nr: Nonce; - read_1(R,I, nr ); - send_2(I,R, { nr }sk(I) ); - read_3(R,I, {{{{ nr }sk(R)}sk(R)}sk(R)}sk(R) ); + read_!1(R,I, nr ); + send_!2(I,R, { nr }sk(I) ); + read_!3(R,I, {{{{ nr }sk(R)}sk(R)}sk(R)}sk(R) ); - claim_i1(I,Niagree); + claim_i1(I,Reachable); } role R { const nr: Nonce; - send_1(R,I, nr ); + send_!1(R,I, nr ); } } @@ -40,9 +40,3 @@ untrusted Eve; const ne: Nonce; compromised sk(Eve); -run f4.I(Agent,Agent); -run f4.I(Agent,Agent); -run f4.I(Agent,Agent); -run f4.I(Agent,Agent); -run f4.I(Agent,Agent); -run f4.I(Agent,Agent); diff --git a/spdl/misc/f5.spdl b/spdl/misc/f5.spdl index 8ed74f2..a0b8f7e 100644 --- a/spdl/misc/f5.spdl +++ b/spdl/misc/f5.spdl @@ -13,23 +13,23 @@ const pk: Function; secret sk: Function; inversekeys (pk,sk); -protocol f4(I,R) +protocol f5(I,R) { role I { var nr: Nonce; - read_1(R,I, nr ); - send_2(I,R, { nr }sk(I) ); - read_3(R,I, {{{{{ nr }sk(R)}sk(R)}sk(R)}sk(R)}sk(R) ); + read_!1(R,I, nr ); + send_!2(I,R, { nr }sk(I) ); + read_!3(R,I, {{{{{ nr }sk(R)}sk(R)}sk(R)}sk(R)}sk(R) ); - claim_i1(I,Niagree); + claim_i1(I,Reachable); } role R { const nr: Nonce; - send_1(R,I, nr ); + send_!1(R,I, nr ); } } @@ -40,9 +40,3 @@ untrusted Eve; const ne: Nonce; compromised sk(Eve); -run f4.I(Agent,Agent); -run f4.I(Agent,Agent); -run f4.I(Agent,Agent); -run f4.I(Agent,Agent); -run f4.I(Agent,Agent); -run f4.I(Agent,Agent); diff --git a/spdl/misc/five-run-bound.spdl b/spdl/misc/five-run-bound.spdl index f3cd1e9..c60735c 100644 --- a/spdl/misc/five-run-bound.spdl +++ b/spdl/misc/five-run-bound.spdl @@ -10,10 +10,10 @@ protocol r5bound(I,R) var ni: Nonce; const k2: Nonce; - read_1 (I,R, ni ); - send_2 (R,I, { ni }sk(R) ); - read_3 (I,R, {{{ {k1}pk(R) }sk(I)}sk(I)}sk(I) ); - send_4 (R,I, {k2}k1 ); + read_!1 (I,R, ni ); + send_!2 (R,I, { ni }sk(R) ); + read_!3 (I,R, {{{ {k1}pk(R) }sk(I)}sk(I)}sk(I) ); + send_!4 (R,I, {k2}k1 ); claim_6 (R, Secret, k2); } @@ -22,11 +22,3 @@ protocol r5bound(I,R) const Alice, Bob: Agent; const ne: Nonce; -run r5bound.R(Agent); -run r5bound.R(Agent); - -run r5bound.R(Agent); -run r5bound.R(Agent); - -run r5bound.R(Agent); -run r5bound.R(Agent); diff --git a/spdl/misc/nsl7.spdl b/spdl/misc/nsl7.spdl deleted file mode 100644 index 452978f..0000000 --- a/spdl/misc/nsl7.spdl +++ /dev/null @@ -1,26 +0,0 @@ -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); - -protocol nsl7(I,R) -{ - role R - { - var ni; - const nr; - - read_1(I,R, {I,ni}pk(R) ); - send_2(R,I, {ni,nr,R}pk(I) ); - read_3(I,R, {nr}pk(R) ); - claim_4(R,Secret,ni); - claim_5(R,Secret,nr); - } -} - -const Alice,Bob,Eve; -const ne; -untrusted Eve; -compromised sk(Eve); - -run nsl7.R(Agent,Agent); -run nsl7.R(Agent,Agent); diff --git a/spdl/misc/onetrace.spdl b/spdl/misc/onetrace.spdl index 5901396..026115d 100644 --- a/spdl/misc/onetrace.spdl +++ b/spdl/misc/onetrace.spdl @@ -9,22 +9,10 @@ protocol onetrace(I) { var input: String; - read_1(I,I, input); - send_2(I,I, Hallo); - read_3(I,I, input); + read_!1(I,I, input); + send_!2(I,I, Hallo); + read_!3(I,I, input); claim_4(I, Secret, input); } } -run onetrace.I(Alice); -run onetrace.I(Alice); -run onetrace.I(Alice); -run onetrace.I(Alice); - -run onetrace.I(Alice); -run onetrace.I(Alice); -run onetrace.I(Alice); -run onetrace.I(Alice); - -run onetrace.I(Alice); -run onetrace.I(Alice); diff --git a/spdl/misc/samasc-broken.spdl b/spdl/misc/samasc-broken.spdl index d97f7fd..ae7f2b3 100644 --- a/spdl/misc/samasc-broken.spdl +++ b/spdl/misc/samasc-broken.spdl @@ -16,14 +16,14 @@ protocol samascbroken(I,R) const nr: Nonce; var kir: Key; - read_1a (I,R, { kir,I }pk(R) ); - send_1b (R,I, {nr,R}pk(I) ); + read_!1a (I,R, { kir,I }pk(R) ); + send_!1b (R,I, {nr,R}pk(I) ); /* Commenting out these two lines yields an attack: */ - read_2a (I,R, { nr }kir ); - send_2b (R,I, { I,R,nr }kir ); + read_!2a (I,R, { nr }kir ); + send_!2b (R,I, { I,R,nr }kir ); - read_3 (I,R, { I,R }kir ); + read_!3 (I,R, { I,R }kir ); claim_4 (R, Secret, kir ); } diff --git a/spdl/misc/simplest.spdl b/spdl/misc/simplest.spdl index d96633f..53bf29f 100644 --- a/spdl/misc/simplest.spdl +++ b/spdl/misc/simplest.spdl @@ -10,11 +10,9 @@ protocol simplest(I) var x: Nonce; const n: Nonce; - read_1(I,I, x); - send_2(I,I, n, {n, x}k ); + read_!1(I,I, x); + send_!2(I,I, n, {n, x}k ); claim_3(I, Secret, n); } } -run simplest.I(Alice); -run simplest.I(Alice); diff --git a/spdl/misc/woolam-ce.spdl b/spdl/misc/woolam-ce.spdl deleted file mode 100644 index 5bbcc65..0000000 --- a/spdl/misc/woolam-ce.spdl +++ /dev/null @@ -1,38 +0,0 @@ -usertype Server, SessionKey, Token, SymmetricKey; -secret k: Function; - -const Alice, Bob, Charlie, Eve: Agent; -const Simon: Server; - -/* give the intruder something to work with */ -const ne: Nonce; -const ke: SessionKey; -untrusted Eve; -compromised k(Eve,Simon); - -const authToken: Token; - -protocol woolamce(A,B,S) -{ - role B - { - var Na: Nonce; - const Nb: Nonce; - var Kab: SessionKey; - var Kas : SymmetricKey; - - read_1(A,B, A,Na); - send_2(B,A, B,Nb); - read_3(A,B, { A,(B,(Na,Nb)) }Kas ); - send_4(B,S, { A,(B,(Na,Nb)) }Kas, { A,(B,(Na,Nb)) }k(B,S) ); - read_5(S,B, { B,(Na,(Nb,Kab)) }Kas, { A,(Na,(Nb,Kab)) }k(B,S) ); - send_6(B,A, { B,(Na,(Nb,Kab)) }Kas, { Na,Nb }Kab ); - read_7(A,B, { Nb }Kab ); - - claim_8(B,Secret,authToken); - } -} - -run woolamce.B(Agent,Agent,Simon); -run woolamce.B(Agent,Agent,Simon); - diff --git a/spdl/misc/yahalom.spdl b/spdl/misc/yahalom.spdl deleted file mode 100644 index 5b62b62..0000000 --- a/spdl/misc/yahalom.spdl +++ /dev/null @@ -1,54 +0,0 @@ -// Yahalom protocol - -const a,b,s : Agent; -secret k : Function; - -usertype Nonce, Ticket, SessionKey; - - -protocol yahalom(A,B,S) -{ - role A - { - const na: Nonce; - var nb: Nonce; - var ticket: Ticket; - var kab: SessionKey; - - send_1(A,B, A,na); - read_3(S,A, nb, {B,kab,na,nb}k(A,S), ticket ); - send_4(A,B, ticket, {nb}kab ); - - claim_5(A, Secret,kab); - } - - role B - { - const nb: Nonce; - var na: Nonce; - var ticket: Ticket; - var kab: SessionKey; - - read_1(A,B, A,na); - send_2(B,S, B,nb, {A,na,nb}k(B,S) ); - read_4(A,B, {A,kab}k(B,S) , {nb}kab ); - - claim_6(B, Secret,kab); - } - - role S - { - const kab: SessionKey; - var na,nb: Nonce; - - read_2(B,S, B,nb, {A,na}k(B,S) ); - send_3(S,A, nb, {B,kab,na,nb}k(A,S), {A,kab}k(B,S) ); - } -} - -run yahalom.A(Agent,Agent,s); -run yahalom.A(Agent,Agent,s); -run yahalom.B(Agent,Agent,s); -run yahalom.B(Agent,Agent,s); -run yahalom.S(Agent,Agent,s); - diff --git a/src/compiler.c b/src/compiler.c index e8c6fcd..ef42bb5 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -2008,6 +2008,7 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, */ if (found == 0) { + globalError++; eprintf ("error: for the read event "); roledefPrint (readevent); eprintf (" of protocol "); @@ -2015,6 +2016,7 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole, eprintf (" there is no corresponding send event (with the same label and matching content). Start the label name with '!' if this is intentional.\n"); error_die (); + globalError--; } } @@ -2048,10 +2050,12 @@ checkLabelMatchProtocol (const System sys, const Protocol p) } else { + globalError++; eprintf ("error: cannot determine label information for "); roledefPrint (rd); eprintf ("\n"); error_die (); + globalError--; } } rd = rd->next;