Synchronising MPA branch with compromise branch where possible.
This commit is contained in:
parent
19359f9ba9
commit
9b0915441f
@ -34,7 +34,7 @@ Scyther 1.0-beta6
|
||||
|
||||
Other new features:
|
||||
|
||||
* [Backend] Scyther now detects when a read event cannot match
|
||||
* [Backend] Scyther now detects when a recv event cannot match
|
||||
with a send event. This significantly helps in reducing errors
|
||||
in the protocol descriptions.
|
||||
* [Language] Added claim parameter for Reachable claim;
|
||||
|
@ -134,6 +134,7 @@ def makeImageDot(dotdata,attackthread=None):
|
||||
# execute command
|
||||
p = Popen(cmd, shell=True, stdin=PIPE, stdout=PIPE)
|
||||
|
||||
|
||||
if attackthread:
|
||||
writeGraph(attackthread,dotdata,p.stdin)
|
||||
else:
|
||||
|
@ -123,6 +123,13 @@ def testPIL():
|
||||
|
||||
class Preferences(dict):
|
||||
|
||||
def setDict(self,d):
|
||||
"""
|
||||
Copy dict into self.
|
||||
"""
|
||||
for x in d.keys():
|
||||
self[x] = d[x]
|
||||
|
||||
def parse(self,line):
|
||||
line = line.strip()
|
||||
|
||||
@ -213,6 +220,11 @@ def get(key,alt=None):
|
||||
else:
|
||||
return alt
|
||||
|
||||
def getkeys():
|
||||
global prefs
|
||||
|
||||
return prefs.keys()
|
||||
|
||||
def set(key,value):
|
||||
global prefs
|
||||
|
||||
|
@ -337,6 +337,9 @@ class ResultWindow(wx.Frame):
|
||||
claimdetails = str(cl.claimtype)
|
||||
if cl.parameter:
|
||||
claimdetails += " %s" % (cl.parameter)
|
||||
# Cut off if very very long
|
||||
if len(claimdetails) > 50:
|
||||
claimdetails = claimdetails[:50] + "..."
|
||||
addtxt(claimdetails + " ",xpos)
|
||||
xpos += 1
|
||||
|
||||
|
@ -114,11 +114,21 @@ def safeCommand(cmd):
|
||||
""" Execute a command with some arguments. Safe cross-platform
|
||||
version, I hope. """
|
||||
|
||||
p = Popen(cmd, shell=getShell())
|
||||
sts = p.wait()
|
||||
try:
|
||||
p = Popen(cmd, shell=getShell())
|
||||
sts = p.wait()
|
||||
except KeyboardInterrupt, EnvironmentError:
|
||||
raise
|
||||
except:
|
||||
print "Wile processing [%s] we had an" % (cmd)
|
||||
print "unexpected error:", sys.exc_info()[0]
|
||||
print
|
||||
sts = -1
|
||||
raise # For now still raise
|
||||
|
||||
return sts
|
||||
|
||||
|
||||
def panic(text):
|
||||
"""
|
||||
Errors that occur before we even are sure about wxPython etc. are dumped
|
||||
|
@ -1,7 +1,7 @@
|
||||
#!/usr/bin/python
|
||||
"""
|
||||
Scyther : An automatic verifier for security protocols.
|
||||
Copyright (C) 2007-2012-2009 Cas Cremers
|
||||
Copyright (C) 2007-2012 Cas Cremers
|
||||
|
||||
This program is free software; you can redistribute it and/or
|
||||
modify it under the terms of the GNU General Public License
|
||||
|
@ -130,7 +130,7 @@ class SemiTrace(object):
|
||||
# Initiations are runs of honest agents
|
||||
if (run.intruder):
|
||||
continue
|
||||
# Which contain no reads before the first send
|
||||
# Which contain no recvs before the first send
|
||||
for action in run:
|
||||
if (isinstance(action,EventRead)):
|
||||
break
|
||||
|
12
gui/mpa.spdl
12
gui/mpa.spdl
@ -12,7 +12,7 @@ protocol nsl3(I,R)
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {ni,I}pk(R) );
|
||||
read_2(R,I, {ni,nr,R}pk(I) );
|
||||
recv_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
@ -26,9 +26,9 @@ protocol nsl3(I,R)
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
read_1(I,R, {ni,I}pk(R) );
|
||||
recv_1(I,R, {ni,I}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
@ -52,7 +52,7 @@ protocol nsl3-broken(I,R)
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {ni,R}pk(R) );
|
||||
read_2(R,I, {ni,nr,R}pk(I) );
|
||||
recv_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
@ -66,9 +66,9 @@ protocol nsl3-broken(I,R)
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
read_1(I,R, {ni,R}pk(R) );
|
||||
recv_1(I,R, {ni,R}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
|
16
gui/ns3.spdl
16
gui/ns3.spdl
@ -12,13 +12,14 @@ protocol ns3(I,R)
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {ni,I}pk(R) );
|
||||
read_2(R,I, {ni,nr}pk(I) );
|
||||
recv_2(R,I, {ni,nr}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
claim_i2(I,Secret,nr);
|
||||
claim_i3(I,Niagree);
|
||||
claim_i4(I,Nisynch);
|
||||
claim_i3(I,Alive);
|
||||
claim_i4(I,Niagree);
|
||||
claim_i5(I,Nisynch);
|
||||
}
|
||||
|
||||
role R
|
||||
@ -26,14 +27,15 @@ protocol ns3(I,R)
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
read_1(I,R, {ni,I}pk(R) );
|
||||
recv_1(I,R, {ni,I}pk(R) );
|
||||
send_2(R,I, {ni,nr}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
claim_r3(R,Niagree);
|
||||
claim_r4(R,Nisynch);
|
||||
claim_r3(R,Alive);
|
||||
claim_r4(R,Niagree);
|
||||
claim_r5(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -13,7 +13,7 @@ protocol nsl3-broken(I,R)
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {ni,R}pk(R) );
|
||||
read_2(R,I, {ni,nr,R}pk(I) );
|
||||
recv_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
@ -27,9 +27,9 @@ protocol nsl3-broken(I,R)
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
read_1(I,R, {ni,R}pk(R) );
|
||||
recv_1(I,R, {ni,R}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
|
@ -12,7 +12,7 @@ protocol nsl3(I,R)
|
||||
var nr: Nonce;
|
||||
|
||||
send_1(I,R, {ni,I}pk(R) );
|
||||
read_2(R,I, {ni,nr,R}pk(I) );
|
||||
recv_2(R,I, {ni,nr,R}pk(I) );
|
||||
send_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_i1(I,Secret,ni);
|
||||
@ -26,9 +26,9 @@ protocol nsl3(I,R)
|
||||
var ni: Nonce;
|
||||
fresh nr: Nonce;
|
||||
|
||||
read_1(I,R, {ni,I}pk(R) );
|
||||
recv_1(I,R, {ni,I}pk(R) );
|
||||
send_2(R,I, {ni,nr,R}pk(I) );
|
||||
read_3(I,R, {nr}pk(R) );
|
||||
recv_3(I,R, {nr}pk(R) );
|
||||
|
||||
claim_r1(R,Secret,ni);
|
||||
claim_r2(R,Secret,nr);
|
||||
|
@ -21,7 +21,6 @@ WOULD LIKE TO HAVE
|
||||
- Line numbering is needed for the editor window otherwise you cannot
|
||||
interpret attacks. Probably use wx.Py editor things.
|
||||
- Scyther executable should be able to be set by means of preferences.
|
||||
- Save attacks (dot/xml/png) to file.
|
||||
|
||||
IN AN IDEAL WORLD...
|
||||
|
||||
|
@ -2,12 +2,6 @@
|
||||
* Needham-Schroeder protocol
|
||||
*/
|
||||
|
||||
// PKI infrastructure
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol ns3(I,R)
|
||||
@ -44,3 +38,4 @@ protocol ns3(I,R)
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
@ -3,12 +3,6 @@
|
||||
* broken version (wrong role name in first message)
|
||||
*/
|
||||
|
||||
// PKI infrastructure
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol nsl3-broken(I,R)
|
||||
@ -44,9 +38,3 @@ protocol nsl3-broken(I,R)
|
||||
}
|
||||
}
|
||||
|
||||
// An untrusted agent, with leaked information
|
||||
|
||||
const Eve: Agent;
|
||||
untrusted Eve;
|
||||
compromised sk(Eve);
|
||||
|
||||
|
@ -3,12 +3,6 @@
|
||||
* broken version (wrong role name in first message)
|
||||
*/
|
||||
|
||||
// PKI infrastructure
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol nsl3-broken(I,R)
|
||||
@ -44,22 +38,10 @@ protocol nsl3-broken(I,R)
|
||||
}
|
||||
}
|
||||
|
||||
// An untrusted agent, with leaked information
|
||||
|
||||
const Eve: Agent;
|
||||
untrusted Eve;
|
||||
compromised sk(Eve);
|
||||
|
||||
/*
|
||||
* Needham-Schroeder-Lowe protocol
|
||||
*/
|
||||
|
||||
// PKI infrastructure
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol nsl3(I,R)
|
||||
@ -94,10 +76,3 @@ protocol nsl3(I,R)
|
||||
claim_r4(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
// An untrusted agent, with leaked information
|
||||
|
||||
const Eve: Agent;
|
||||
untrusted Eve;
|
||||
compromised sk(Eve);
|
||||
|
||||
|
@ -2,12 +2,6 @@
|
||||
* Needham-Schroeder-Lowe protocol
|
||||
*/
|
||||
|
||||
// PKI infrastructure
|
||||
|
||||
const pk: Function;
|
||||
secret sk: Function;
|
||||
inversekeys (pk,sk);
|
||||
|
||||
// The protocol description
|
||||
|
||||
protocol nsl3(I,R)
|
||||
@ -42,10 +36,3 @@ protocol nsl3(I,R)
|
||||
claim_r4(R,Nisynch);
|
||||
}
|
||||
}
|
||||
|
||||
// An untrusted agent, with leaked information
|
||||
|
||||
const Eve: Agent;
|
||||
untrusted Eve;
|
||||
compromised sk(Eve);
|
||||
|
||||
|
@ -1,6 +1,5 @@
|
||||
usertype Sessionkey;
|
||||
usertype Macseed;
|
||||
secret k: Function;
|
||||
const m: Function;
|
||||
secret unm: Function;
|
||||
const f: Function;
|
||||
@ -59,23 +58,3 @@ protocol boyd(I,R,S)
|
||||
}
|
||||
}
|
||||
|
||||
const Alice,Bob,Simon,Eve: Agent;
|
||||
|
||||
untrusted Eve;
|
||||
const ne: Nonce;
|
||||
const mcsde: Macseed;
|
||||
const ke: Sessionkey;
|
||||
compromised k(Eve,Eve);
|
||||
compromised k(Eve,Alice);
|
||||
compromised k(Eve,Bob);
|
||||
compromised k(Eve,Simon);
|
||||
compromised k(Alice,Eve);
|
||||
compromised k(Bob,Eve);
|
||||
compromised k(Simon,Eve);
|
||||
|
||||
run boyd.I(Agent,Agent,Simon);
|
||||
run boyd.R(Agent,Agent,Simon);
|
||||
run boyd.S(Agent,Agent,Simon);
|
||||
run boyd.I(Agent,Agent,Simon);
|
||||
run boyd.R(Agent,Agent,Simon);
|
||||
run boyd.S(Agent,Agent,Simon);
|
||||
|
@ -1816,8 +1816,6 @@ compute_prec_sets (const System sys)
|
||||
r2 = 0;
|
||||
while (r2 < sys->rolecount)
|
||||
{
|
||||
Roledef rd2;
|
||||
|
||||
ev2 = 0;
|
||||
rd = roledef_re (r2, ev2);
|
||||
while (rd != NULL)
|
||||
|
@ -48,7 +48,7 @@ void dependPopEvent ();
|
||||
|
||||
int getNode (const int n1, const int n2);
|
||||
void setNode (const int n1, const int n2);
|
||||
int isDependEvent (const int r1, const int e1, const int r2, const int e2);
|
||||
int isDependEvent (const int r1, const int e1, const int r2, const int e2); // r1,e1 before r2,e2
|
||||
void setDependEvent (const int r1, const int e1, const int r2, const int e2);
|
||||
|
||||
/*
|
||||
|
Loading…
Reference in New Issue
Block a user