From 83922f3f2c92c70d33a7feeb255c3d4def489b43 Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 18 Nov 2004 16:07:58 +0000 Subject: [PATCH] - Fixed some protocols with wrong protocol names in the specification. - Added more safety stuff to the testing code. --- spdl/bke-broken.spdl | 8 ++++---- spdl/bke-one.spdl | 24 ++++++++++++------------ spdl/bke.spdl | 22 +++++++++++----------- spdl/bkepk-ce.spdl | 20 ++++++++++---------- spdl/multiprotocoltest.py | 7 +++++-- spdl/samasc-broken.spdl | 2 +- 6 files changed, 43 insertions(+), 40 deletions(-) diff --git a/spdl/bke-broken.spdl b/spdl/bke-broken.spdl index 0164e65..92f4fe3 100644 --- a/spdl/bke-broken.spdl +++ b/spdl/bke-broken.spdl @@ -1,5 +1,5 @@ /* - Bilateral Key Exchange with Public Key protocol (BKEPK) + Bilateral Key Exchange with Public Key protocol (bkebroken) Broken version with man in the middle attack. */ @@ -11,7 +11,7 @@ secret SK,hinv: Function; inversekeys (PK,SK); inversekeys (h,hinv); -protocol bkepk(I,R) +protocol bkebroken(I,R) { role I { @@ -44,5 +44,5 @@ untrusted e; compromised SK(e); const ne: Nonce; -run bkepk.I(a,Agent); -run bkepk.R(Agent,b); +run bkebroken.I(a,Agent); +run bkebroken.R(Agent,b); diff --git a/spdl/bke-one.spdl b/spdl/bke-one.spdl index 105fde5..a5e8325 100644 --- a/spdl/bke-one.spdl +++ b/spdl/bke-one.spdl @@ -1,5 +1,5 @@ /* - Bilateral Key Exchange with Public Key protocol (BKEPK) + Bilateral Key Exchange with Public Key protocol (bkeONE) */ usertype Key; @@ -10,7 +10,7 @@ secret sk,unhash: Function; inversekeys (pk,sk); inversekeys (hash,unhash); -protocol bkepk(I,R) +protocol bkeONE(I,R) { role I { @@ -43,16 +43,16 @@ untrusted e; compromised sk(e); const ne: Nonce; -run bkepk.I(a,Agent); -run bkepk.R(Agent,a); -run bkepk.I(a,Agent); -run bkepk.R(Agent,a); +run bkeONE.I(a,Agent); +run bkeONE.R(Agent,a); +run bkeONE.I(a,Agent); +run bkeONE.R(Agent,a); -run bkepk.I(a,Agent); -run bkepk.R(Agent,a); -run bkepk.I(a,Agent); -run bkepk.R(Agent,a); +run bkeONE.I(a,Agent); +run bkeONE.R(Agent,a); +run bkeONE.I(a,Agent); +run bkeONE.R(Agent,a); -run bkepk.I(a,Agent); -run bkepk.R(Agent,a); +run bkeONE.I(a,Agent); +run bkeONE.R(Agent,a); diff --git a/spdl/bke.spdl b/spdl/bke.spdl index 027e414..ead3ac2 100644 --- a/spdl/bke.spdl +++ b/spdl/bke.spdl @@ -10,7 +10,7 @@ secret sk,unhash: Function; inversekeys (pk,sk); inversekeys (hash,unhash); -protocol bkepk(I,R) +protocol bke(I,R) { role I { @@ -45,16 +45,16 @@ untrusted e; compromised sk(e); const ne: Nonce; -run bkepk.I(a,Agent); -run bkepk.R(Agent,b); -run bkepk.I(a,Agent); -run bkepk.R(Agent,b); +run bke.I(a,Agent); +run bke.R(Agent,b); +run bke.I(a,Agent); +run bke.R(Agent,b); -run bkepk.I(a,Agent); -run bkepk.R(Agent,b); -run bkepk.I(a,Agent); -run bkepk.R(Agent,b); +run bke.I(a,Agent); +run bke.R(Agent,b); +run bke.I(a,Agent); +run bke.R(Agent,b); -run bkepk.I(a,Agent); -run bkepk.R(Agent,b); +run bke.I(a,Agent); +run bke.R(Agent,b); diff --git a/spdl/bkepk-ce.spdl b/spdl/bkepk-ce.spdl index d19fdbc..d74a1f2 100644 --- a/spdl/bkepk-ce.spdl +++ b/spdl/bkepk-ce.spdl @@ -1,5 +1,5 @@ /* - Bilateral Key Exchange with Public Key protocol (BKEPK) + Bilateral Key Exchange with Public Key protocol (bkeCE) Version from Corin/Etalle: An Improved Constraint-Based System for the Verification of Security Protocols. Tried to stay as close as possible to compare timing results. @@ -12,7 +12,7 @@ secret sk: Function; inversekeys (pk,sk); -protocol bkepk(A,B,testnonce) +protocol bkeCE(A,B,testnonce) { role B { @@ -50,12 +50,12 @@ compromised sk(Eve); untrusted Eve; -run bkepk.A(Alice,Bob,Alice); -run bkepk.A(Alice,Bob,Alice); -run bkepk.B(Alice,Bob,Alice); -run bkepk.B(Alice,Bob,Alice); -run bkepk.testnonce(Alice,Bob,Alice); -run bkepk.testnonce(Alice,Bob,Alice); +run bkeCE.A(Alice,Bob,Alice); +run bkeCE.A(Alice,Bob,Alice); +run bkeCE.B(Alice,Bob,Alice); +run bkeCE.B(Alice,Bob,Alice); +run bkeCE.testnonce(Alice,Bob,Alice); +run bkeCE.testnonce(Alice,Bob,Alice); -run bkepk.A(Alice,Bob,Alice); -run bkepk.testnonce(Alice,Bob,Alice); +run bkeCE.A(Alice,Bob,Alice); +run bkeCE.testnonce(Alice,Bob,Alice); diff --git a/spdl/multiprotocoltest.py b/spdl/multiprotocoltest.py index a2b9823..986c542 100755 --- a/spdl/multiprotocoltest.py +++ b/spdl/multiprotocoltest.py @@ -63,8 +63,7 @@ def ScytherEval (plist): if tag == 'correct:': value = 1 if value == -1: - print "Scyther parse error for the input line: " + commandline - print "On the output line: " + line + raise IOError, 'Scyther output for ' + commandline + ', line ' + line + ' cannot be parsed.' results[claim] = value return results @@ -73,6 +72,9 @@ def ScytherEval (plist): # The above, but do the preprocessing for a single protocol def ScytherEval1 (protocol): results = ScytherEval ([protocol]) + for claim in results.keys(): + if ProtocolClaims.has_key(claim): + raise IOError, 'Claim occurs in two protocols: ' + claim ProtocolClaims.update (results) @@ -219,5 +221,6 @@ for tline in inp: ClearProgress (TupleCount, safetxt) print "Processed", processed,"tuple combinations in total." +print "Found", newattacks, "new attacks." inp.close() diff --git a/spdl/samasc-broken.spdl b/spdl/samasc-broken.spdl index 755e1fb..f5a8976 100644 --- a/spdl/samasc-broken.spdl +++ b/spdl/samasc-broken.spdl @@ -9,7 +9,7 @@ secret sk: Function; inversekeys (pk,sk); -protocol bkepk(I,R) +protocol samasc-broken(I,R) { role R {