From 9b0915441f123a0315e92f82f4c8f1af51605de7 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Wed, 25 Apr 2012 17:03:51 +0200 Subject: [PATCH] Synchronising MPA branch with compromise branch where possible. --- gui/Changelog.txt | 2 +- gui/Gui/Makeimage.py | 1 + gui/Gui/Preference.py | 12 ++++++++++++ gui/Gui/Scytherthread.py | 3 +++ gui/Scyther/Misc.py | 14 ++++++++++++-- gui/Scyther/Scyther.py | 2 +- gui/Scyther/Trace.py | 2 +- gui/mpa.spdl | 12 ++++++------ gui/ns3.spdl | 16 +++++++++------- gui/nsl3-broken.spdl | 6 +++--- gui/nsl3.spdl | 6 +++--- gui/todo.txt | 1 - protocols/Demo/ns3.spdl | 7 +------ protocols/Demo/nsl3-broken.spdl | 12 ------------ protocols/Demo/nsl3-updated-both.spdl | 25 ------------------------- protocols/Demo/nsl3.spdl | 13 ------------- protocols/misc/boyd.spdl | 21 --------------------- src/compiler.c | 2 -- src/depend.h | 2 +- 19 files changed, 54 insertions(+), 105 deletions(-) diff --git a/gui/Changelog.txt b/gui/Changelog.txt index ef5f8e1..a72997e 100644 --- a/gui/Changelog.txt +++ b/gui/Changelog.txt @@ -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; diff --git a/gui/Gui/Makeimage.py b/gui/Gui/Makeimage.py index 0015937..c6f7a73 100644 --- a/gui/Gui/Makeimage.py +++ b/gui/Gui/Makeimage.py @@ -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: diff --git a/gui/Gui/Preference.py b/gui/Gui/Preference.py index 7869ff4..d82a031 100644 --- a/gui/Gui/Preference.py +++ b/gui/Gui/Preference.py @@ -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 diff --git a/gui/Gui/Scytherthread.py b/gui/Gui/Scytherthread.py index 645961d..1ce35f6 100644 --- a/gui/Gui/Scytherthread.py +++ b/gui/Gui/Scytherthread.py @@ -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 diff --git a/gui/Scyther/Misc.py b/gui/Scyther/Misc.py index 1a8a273..27609da 100644 --- a/gui/Scyther/Misc.py +++ b/gui/Scyther/Misc.py @@ -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 diff --git a/gui/Scyther/Scyther.py b/gui/Scyther/Scyther.py index c7a9c39..2206a40 100755 --- a/gui/Scyther/Scyther.py +++ b/gui/Scyther/Scyther.py @@ -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 diff --git a/gui/Scyther/Trace.py b/gui/Scyther/Trace.py index 3aa2310..856f276 100644 --- a/gui/Scyther/Trace.py +++ b/gui/Scyther/Trace.py @@ -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 diff --git a/gui/mpa.spdl b/gui/mpa.spdl index 99d3ed6..4913029 100644 --- a/gui/mpa.spdl +++ b/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); diff --git a/gui/ns3.spdl b/gui/ns3.spdl index e78c1a7..b7904bf 100644 --- a/gui/ns3.spdl +++ b/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); } } diff --git a/gui/nsl3-broken.spdl b/gui/nsl3-broken.spdl index b84b5c2..3681cd9 100644 --- a/gui/nsl3-broken.spdl +++ b/gui/nsl3-broken.spdl @@ -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); diff --git a/gui/nsl3.spdl b/gui/nsl3.spdl index af99579..a4bfef5 100644 --- a/gui/nsl3.spdl +++ b/gui/nsl3.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); diff --git a/gui/todo.txt b/gui/todo.txt index 91d0181..60e05af 100644 --- a/gui/todo.txt +++ b/gui/todo.txt @@ -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... diff --git a/protocols/Demo/ns3.spdl b/protocols/Demo/ns3.spdl index 5dc5fee..7b3e6ba 100644 --- a/protocols/Demo/ns3.spdl +++ b/protocols/Demo/ns3.spdl @@ -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) } + diff --git a/protocols/Demo/nsl3-broken.spdl b/protocols/Demo/nsl3-broken.spdl index a0cf88e..458e306 100644 --- a/protocols/Demo/nsl3-broken.spdl +++ b/protocols/Demo/nsl3-broken.spdl @@ -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); - diff --git a/protocols/Demo/nsl3-updated-both.spdl b/protocols/Demo/nsl3-updated-both.spdl index e465424..e8c6bf0 100644 --- a/protocols/Demo/nsl3-updated-both.spdl +++ b/protocols/Demo/nsl3-updated-both.spdl @@ -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); - diff --git a/protocols/Demo/nsl3.spdl b/protocols/Demo/nsl3.spdl index 04d02a0..e448499 100644 --- a/protocols/Demo/nsl3.spdl +++ b/protocols/Demo/nsl3.spdl @@ -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); - diff --git a/protocols/misc/boyd.spdl b/protocols/misc/boyd.spdl index adcf26e..ace3bd7 100644 --- a/protocols/misc/boyd.spdl +++ b/protocols/misc/boyd.spdl @@ -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); diff --git a/src/compiler.c b/src/compiler.c index d203b53..4180f45 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -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) diff --git a/src/depend.h b/src/depend.h index 1fce191..b0b01ce 100644 --- a/src/depend.h +++ b/src/depend.h @@ -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); /*