From b2bc575447ef9ed9a26a82b8457328c6cd41d683 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Wed, 9 Aug 2006 11:36:33 +0000
Subject: [PATCH] - Some fixes.

---
 gui/Gui/Scytherthread.py |  14 ++++--
 gui/Scyther/__init__.py  |   9 ++++
 gui/mpa.spdl             | 102 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 120 insertions(+), 5 deletions(-)
 create mode 100644 gui/mpa.spdl

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