- Fixed ns/nsl and mpa example.

gui/mpa.spdl

@@ -1,54 +1,3 @@
-/* 
- * 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
  */
@@ -68,7 +17,7 @@ protocol nsl3(I,R)
 		const ni: Nonce;
 		var nr: Nonce;
 
-		send_1(I,R, {I,ni}pk(R) );
+		send_1(I,R, {ni,I}pk(R) );
 		read_2(R,I, {ni,nr,R}pk(I) );
 		send_3(I,R, {nr}pk(R) );
 
@@ -83,7 +32,59 @@ protocol nsl3(I,R)
 		var ni: Nonce;
 		const nr: Nonce;
 
-		read_1(I,R, {I,ni}pk(R) );
+		read_1(I,R, {ni,I}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);
+
+/* 
+ * 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, {ni,R}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, {ni,R}pk(R) );
 		send_2(R,I, {ni,nr,R}pk(I) );
 		read_3(I,R, {nr}pk(R) );
 

gui/ns3.spdl

@@ -17,7 +17,7 @@ protocol ns3(I,R)
 		const ni: Nonce;
 		var nr: Nonce;
 
-		send_1(I,R, {I,ni}pk(R) );
+		send_1(I,R, {ni,I}pk(R) );
 		read_2(R,I, {ni,nr}pk(I) );
 		send_3(I,R, {nr}pk(R) );
 
@@ -32,7 +32,7 @@ protocol ns3(I,R)
 		var ni: Nonce;
 		const nr: Nonce;
 
-		read_1(I,R, {I,ni}pk(R) );
+		read_1(I,R, {ni,I}pk(R) );
 		send_2(R,I, {ni,nr}pk(I) );
 		read_3(I,R, {nr}pk(R) );
 

gui/nsl3-broken.spdl

@@ -18,7 +18,7 @@ protocol nsl3-broken(I,R)
 		const ni: Nonce;
 		var nr: Nonce;
 
-		send_1(I,R, {R,ni}pk(R) );
+		send_1(I,R, {ni,R}pk(R) );
 		read_2(R,I, {ni,nr,R}pk(I) );
 		send_3(I,R, {nr}pk(R) );
 
@@ -33,7 +33,7 @@ protocol nsl3-broken(I,R)
 		var ni: Nonce;
 		const nr: Nonce;
 
-		read_1(I,R, {R,ni}pk(R) );
+		read_1(I,R, {ni,R}pk(R) );
 		send_2(R,I, {ni,nr,R}pk(I) );
 		read_3(I,R, {nr}pk(R) );
 

gui/nsl3.spdl

@@ -17,7 +17,7 @@ protocol nsl3(I,R)
 		const ni: Nonce;
 		var nr: Nonce;
 
-		send_1(I,R, {I,ni}pk(R) );
+		send_1(I,R, {ni,I}pk(R) );
 		read_2(R,I, {ni,nr,R}pk(I) );
 		send_3(I,R, {nr}pk(R) );
 
@@ -32,7 +32,7 @@ protocol nsl3(I,R)
 		var ni: Nonce;
 		const nr: Nonce;
 
-		read_1(I,R, {I,ni}pk(R) );
+		read_1(I,R, {ni,I}pk(R) );
 		send_2(R,I, {ni,nr,R}pk(I) );
 		read_3(I,R, {nr}pk(R) );