- Some fixes.

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
+            showR = True
-        if showPR:
+        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:

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])

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