diff --git a/gui/Gui/Scytherthread.py b/gui/Gui/Scytherthread.py index 233318f..6b76257 100644 --- a/gui/Gui/Scytherthread.py +++ b/gui/Gui/Scytherthread.py @@ -275,6 +275,7 @@ class ResultWindow(wx.Frame): titlebar(0,"Claim",4) titlebar(4,"Status",2) + titlebar(6,"Comments",1) self.lastprot = None self.lastrole = None @@ -298,16 +299,19 @@ class ResultWindow(wx.Frame): # protocol, role, label prot = str(cl.protocol) - showPR = False + showP = False + showR = False if prot != self.lastprot: self.lastprot = prot - showPR = True + showP = True + showR = True role = str(cl.role) if role != self.lastrole: self.lastrole = role - showPR = True - if showPR: + showR = True + if showP: addtxt(prot,xpos) + if showR: addtxt(role,xpos+1) xpos += 2 @@ -358,7 +362,7 @@ class ResultWindow(wx.Frame): else: # some attacks/states within bounds remark = "At least %i %s" % (n,atxt) - if not self.state: + if not cl.state: vstatus = "Falsified" else: if n == 0: diff --git a/gui/Scyther/__init__.py b/gui/Scyther/__init__.py index e69de29..ece72c2 100644 --- a/gui/Scyther/__init__.py +++ b/gui/Scyther/__init__.py @@ -0,0 +1,9 @@ +# +# Init this module +# +# The most important thing is to get the base directory right, in +# order to correctly find the executables +# +import Scyther + +Scyther.init(__path__[0]) diff --git a/gui/mpa.spdl b/gui/mpa.spdl new file mode 100644 index 0000000..e159f9d --- /dev/null +++ b/gui/mpa.spdl @@ -0,0 +1,102 @@ +/* + * Needham-Schroeder protocol + */ + +// PKI infrastructure + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +// The protocol description + +protocol ns3(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + read_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); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + + read_1(I,R, {I,ni}pk(R) ); + send_2(R,I, {ni,nr}pk(I) ); + read_3(I,R, {nr}pk(R) ); + + claim_r1(R,Secret,ni); + claim_r2(R,Secret,nr); + claim_r3(R,Niagree); + claim_r4(R,Nisynch); + } +} + +// 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) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + read_2(R,I, {ni,nr,R}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); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + + 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_r1(R,Secret,ni); + claim_r2(R,Secret,nr); + claim_r3(R,Niagree); + claim_r4(R,Nisynch); + } +} + +// An untrusted agent, with leaked information + +const Eve: Agent; +untrusted Eve; +compromised sk(Eve); +