- More fixes for beta5

gui/README.txt

@@ -2,14 +2,14 @@
 
 				Scyther
 
-			       1.0-beta4
+			       1.0-beta5
 
-	  a automatic verification tool for security protocols
+	  an automatic verification tool for security protocols
 			     by Cas Cremers
 
 			Microsoft Windows binary
 				  and
-	   Linux binary compiled for Linux i686 environments
+	   Linux binary (compiled for Linux i686 environments)
 
 ------------------------------------------------------------------------
 
@@ -23,7 +23,7 @@ Note: This is a BETA release, and therefore the usual warnings apply.
 
 For more information, see:
 
-  http://www.win.tue.nl/~ccremers/scyther
+  http://people.inf.ethz.ch/cremersc/scyther/index.html
 
 
 2. Starting out
@@ -41,14 +41,11 @@ SPORE directory.
 3. Citing Scyther
 ===========================
 
-For now, there is no official journal paper to cite yet, but you can use
-the following information:
-
-@misc{wwwscyther,
-  Author = "C.J.F. Cremers",
-  Title  = "The Scyther Tool : Automated Verification of Security Protocols",
-  Note   = "\url{http://www.win.tue.nl/~ccremers/scyther}",
-  url    = "http://www.win.tue.nl/~ccremers/scyther"
+@phdthesis{cremers06,
+  Author    = "Cas Cremers",
+  Title     = "Scyther - Semantics and Verification of Security Protocols",
+  school    = "Eindhoven University of Technology",
+  publisher = "University Press Eindhoven",
+  year      = "2006",
 }
 
-

gui/mpa.py

@@ -129,7 +129,7 @@ if __name__ == '__main__':
     Simple test case with a few protocols
     """
 
-    list = ['me.spdl','ns3.spdl','nsl3.spdl']
+    list = ['nsl3-broken.spdl','ns3.spdl','nsl3.spdl']
     print "Performing multi-protocol analysis for the following protocols:", list
     print
     findAllMPA(list)

gui/nsl3-broken.spdl

@@ -0,0 +1,52 @@
+/* 
+ * Needham-Schroeder-Lowe protocol,
+ * 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)
+{
+	role I
+	{
+		const ni: Nonce;
+		var nr: Nonce;
+
+		send_1(I,R, {R,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, {R,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);
+