diff --git a/spdl/2r890-ex3-a.spdl b/spdl/2r890-ex3-a.spdl
index 24ec0af..bd124d0 100644
--- a/spdl/2r890-ex3-a.spdl
+++ b/spdl/2r890-ex3-a.spdl
@@ -19,9 +19,9 @@ protocol course2r890year0405ex3(X,Y,I)
 		const ny: Nonce;
 
 		send_1(I,X, nx );
-		read_2(X,I, { nx,I }sk(X) );
+		read_2(X,I, { I,nx }sk(X) );
 		send_3(I,Y, ny );
-		read_4(Y,I, { I,ny }sk(Y) );
+		read_4(Y,I, { ny,I }sk(Y) );
 
 		claim_i1(I,Niagree);
 		claim_i2(I,Nisynch);
@@ -32,7 +32,7 @@ protocol course2r890year0405ex3(X,Y,I)
 		var nx: Nonce;
 
 		read_1(I,X, nx );
-		send_2(X,I, { nx,I }sk(X) );
+		send_2(X,I, { I,nx }sk(X) );
 	}
 
 	role Y
@@ -40,7 +40,7 @@ protocol course2r890year0405ex3(X,Y,I)
 		var ny: Nonce;
 
 		read_3(I,Y, ny );
-		send_4(Y,I, { I,ny }sk(Y) );
+		send_4(Y,I, { ny,I }sk(Y) );
 	}
 }
 
diff --git a/spdl/2r890-ex3-b.spdl b/spdl/2r890-ex3-b.spdl
index 191782f..8620998 100644
--- a/spdl/2r890-ex3-b.spdl
+++ b/spdl/2r890-ex3-b.spdl
@@ -18,9 +18,9 @@ protocol course2r890year0405ex3(X,Y,I)
 		const ni: Nonce;
 
 		send_1(I,X, ni );
-		read_2(X,I, { ni,I }sk(X) );
+		read_2(X,I, { I,ni }sk(X) );
 		send_3(I,Y, ni );
-		read_4(Y,I, { I,ni }sk(Y) );
+		read_4(Y,I, { ni,I }sk(Y) );
 
 		claim_i1(I,Niagree);
 		claim_i2(I,Nisynch);
@@ -31,7 +31,7 @@ protocol course2r890year0405ex3(X,Y,I)
 		var nx: Nonce;
 
 		read_1(I,X, nx );
-		send_2(X,I, { nx,I }sk(X) );
+		send_2(X,I, { I,nx }sk(X) );
 	}
 
 	role Y
@@ -39,7 +39,7 @@ protocol course2r890year0405ex3(X,Y,I)
 		var ny: Nonce;
 
 		read_3(I,Y, ny );
-		send_4(Y,I, { I,ny }sk(Y) );
+		send_4(Y,I, { ny,I }sk(Y) );
 	}
 }
 
diff --git a/spdl/ns3.spdl b/spdl/ns3.spdl
index c957d2a..44cb490 100644
--- a/spdl/ns3.spdl
+++ b/spdl/ns3.spdl
@@ -56,4 +56,12 @@ compromised sk(Eve);
 
 run ns3.I(Agent,Agent);
 run ns3.R(Agent,Agent);
+run ns3.I(Agent,Agent);
+run ns3.R(Agent,Agent);
+run ns3.I(Agent,Agent);
+run ns3.R(Agent,Agent);
+run ns3.I(Agent,Agent);
+run ns3.R(Agent,Agent);
+run ns3.I(Agent,Agent);
+run ns3.R(Agent,Agent);
 
diff --git a/spdl/tls-paulson.cpp b/spdl/tls-paulson.cpp
index c722605..87ffd6a 100644
--- a/spdl/tls-paulson.cpp
+++ b/spdl/tls-paulson.cpp
@@ -36,7 +36,8 @@ protocol tlspaulson(a,b)
 		send_7( a,b, { F }CLIENTK );
 		read_8( b,a, { F }SERVERK );
 
-		claim_9(a, Secret,CLIENTK, SERVERK);
+		claim_9a(a, Secret, SERVERK);
+		claim_9b(a, Secret, CLIENTK);
 
 	}	
 	
@@ -57,7 +58,8 @@ protocol tlspaulson(a,b)
 		read_7( a,b, { F }CLIENTK );
 		send_8( b,a, { F }SERVERK );
 
-		claim_10(b, Secret,CLIENTK, SERVERK);
+		claim_10a(b, Secret, SERVERK);
+		claim_10b(b, Secret, CLIENTK);
 	}
 }