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

- Fixed some protocols with wrong protocol names in the specification.

Browse Source 
- Added more safety stuff to the testing code.
This commit is contained in:
ccremers 2004-11-18 16:07:58 +00:00
parent 2b53516542
commit 83922f3f2c
6 changed files with 43 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
spdl/bke-broken.spdl
View File

@ -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);

24
spdl/bke-one.spdl
View File

@ -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);

22
spdl/bke.spdl
View File

@ -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);

20
spdl/bkepk-ce.spdl
View File

@ -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);

7
spdl/multiprotocoltest.py
View File

@ -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()

2
spdl/samasc-broken.spdl
View File

@ -9,7 +9,7 @@ secret sk: Function;
inversekeys (pk,sk);
protocol bkepk(I,R)
protocol samasc-broken(I,R)
{
role R
{