diff --git a/spdl/bkepk-ce.spdl b/spdl/bkepk-ce.spdl
index 6f0d59e..d19fdbc 100644
--- a/spdl/bkepk-ce.spdl
+++ b/spdl/bkepk-ce.spdl
@@ -40,13 +40,14 @@ protocol bkepk(A,B,testnonce)
 	{
 		var n: Nonce;
 
-		read_4 (A,A, n);
+		read_4 (testnonce,testnonce, n);
 	}
 }
 
 const Alice,Bob,Eve;
 
 compromised sk(Eve);
+untrusted Eve;
 
 
 run bkepk.A(Alice,Bob,Alice);
diff --git a/spdl/bkepk-ce2.spdl b/spdl/bkepk-ce2.spdl
index da398be..0e50a55 100644
--- a/spdl/bkepk-ce2.spdl
+++ b/spdl/bkepk-ce2.spdl
@@ -1,5 +1,5 @@
 /* 
-	Bilateral Key Exchange with Public Key protocol (BKEPK)
+	Bilateral Key Exchange with Public Key protocol (bkepkCE2)
 
 	Version from Corin/Etalle: An Improved Constraint-Based System for the Verification of Security Protocols.
 	Tried to stay as close as possible to compare timing results.
@@ -12,7 +12,7 @@ secret sk: Function;
 
 inversekeys (pk,sk);
 
-protocol bkepk(A,B,testnonce)
+protocol bkepkCE2(A,B,testnonce)
 {
 	role B
 	{
@@ -40,22 +40,23 @@ protocol bkepk(A,B,testnonce)
 	{
 		var n: Nonce;
 
-		read_4 (A,A, n);
+		read_4 (testnonce,testnonce, n);
 	}
 }
 
 const Alice,Bob,Eve;
 
 compromised sk(Eve);
+untrusted Eve;
 
 
-run bkepk.A(Alice,Bob,Alice);
-run bkepk.A(Alice,Bob,Alice);
-run bkepk.A(Alice,Bob,Alice);
-run bkepk.B(Alice,Bob,Alice);
-run bkepk.B(Alice,Bob,Alice);
-run bkepk.B(Alice,Bob,Alice);
+run bkepkCE2.A(Alice,Bob,Alice);
+run bkepkCE2.A(Alice,Bob,Alice);
+run bkepkCE2.A(Alice,Bob,Alice);
+run bkepkCE2.B(Alice,Bob,Alice);
+run bkepkCE2.B(Alice,Bob,Alice);
+run bkepkCE2.B(Alice,Bob,Alice);
 
-run bkepk.testnonce(Alice,Bob,Alice);
-run bkepk.testnonce(Alice,Bob,Alice);
-run bkepk.testnonce(Alice,Bob,Alice);
+run bkepkCE2.testnonce(Alice,Bob,Alice);
+run bkepkCE2.testnonce(Alice,Bob,Alice);
+run bkepkCE2.testnonce(Alice,Bob,Alice);
diff --git a/spdl/broken1.spdl b/spdl/broken1.spdl
index 819d615..800ca6a 100644
--- a/spdl/broken1.spdl
+++ b/spdl/broken1.spdl
@@ -22,7 +22,7 @@ protocol broken1(I,R,S)
 	{
 		read_3(S, R, {HelloWorld, S, I, R}k );
 		read_1(I, R, PlainSight, {HelloWorld, I, R}k );
-		claim(R, Secret, PlainSight);
+		claim_4(R, Secret, PlainSight);
 	}
 	role S
 	{
diff --git a/spdl/carkey-broken-limited.spdl b/spdl/carkey-broken-limited.spdl
index a2f3e5a..c5f4305 100644
--- a/spdl/carkey-broken-limited.spdl
+++ b/spdl/carkey-broken-limited.spdl
@@ -9,7 +9,6 @@ protocol carkeybroken(I,R)
 		const ni: Nonce;
 
 		send_1(I,R, I,R );
-		claim_3(I,Nisynch);
 	}	
 	
 	role R
diff --git a/spdl/carkey-broken.spdl b/spdl/carkey-broken.spdl
index cba0666..a0e0ba5 100644
--- a/spdl/carkey-broken.spdl
+++ b/spdl/carkey-broken.spdl
@@ -9,7 +9,6 @@ protocol carkeybroken(I,R)
 		const ni: Nonce;
 
 		send_1(I,R, {ni}sk(I) );
-		claim_3(I,Nisynch);
 	}	
 	
 	role R
diff --git a/spdl/carkey-ni.spdl b/spdl/carkey-ni.spdl
index 6d9245c..ed189b4 100644
--- a/spdl/carkey-ni.spdl
+++ b/spdl/carkey-ni.spdl
@@ -9,7 +9,6 @@ protocol carkeyni(I,R)
 		const ni: Nonce;
 
 		send_1(I,R, {R,ni}sk(I) );
-		claim_3(I,Nisynch);
 	}	
 	
 	role R
diff --git a/spdl/carkey-ni2.spdl b/spdl/carkey-ni2.spdl
index 8d40deb..5c7802a 100644
--- a/spdl/carkey-ni2.spdl
+++ b/spdl/carkey-ni2.spdl
@@ -10,7 +10,6 @@ protocol carkeyni(I,R)
 
 		send_1(I,R, {R,ni}sk(I) );
 		send_2(I,R, {R,ni}sk(I) );
-		claim_5(I,Nisynch);
 	}	
 	
 	role R
diff --git a/spdl/five-run-bound.spdl b/spdl/five-run-bound.spdl
index 5ff6f2d..f3cd1e9 100644
--- a/spdl/five-run-bound.spdl
+++ b/spdl/five-run-bound.spdl
@@ -4,20 +4,6 @@ inversekeys (pk,sk);
 
 protocol r5bound(I,R)
 {
-	role I
-	{
-		const k1: Nonce;
-		const ni: Nonce;
-		var k2: Nonce;
-
-		send_1 (I,R, ni );
-		read_2 (R,I, { ni }sk(R) );
-		send_3 (I,R, {{{ {k1}pk(R) }sk(I)}sk(I)}sk(I) );
-		read_4 (R,I, {k2}k1 );
-
-		claim_5 (I, Secret, k2);
-	}
-	
 	role R
 	{
 		var k1: Nonce;
@@ -34,18 +20,13 @@ protocol r5bound(I,R)
 }
 
 const Alice, Bob: Agent;
+const ne: Nonce;
 
-run r5bound.I(Agent,Agent);
-run r5bound.R(Agent,Agent);
-run r5bound.I(Agent,Agent);
-run r5bound.R(Agent,Agent);
+run r5bound.R(Agent);
+run r5bound.R(Agent);
 
-run r5bound.I(Agent,Agent);
-run r5bound.R(Agent,Agent);
-run r5bound.I(Agent,Agent);
-run r5bound.R(Agent,Agent);
+run r5bound.R(Agent);
+run r5bound.R(Agent);
 
-run r5bound.I(Agent,Agent);
-run r5bound.R(Agent,Agent);
-run r5bound.I(Agent,Agent);
-run r5bound.R(Agent,Agent);
+run r5bound.R(Agent);
+run r5bound.R(Agent);
diff --git a/spdl/helloworld.spdl b/spdl/helloworld.spdl
index eaff92e..597a308 100644
--- a/spdl/helloworld.spdl
+++ b/spdl/helloworld.spdl
@@ -6,7 +6,7 @@ protocol hw(initiator,world)
 	role initiator
 	{
 		send_1(initiator, world, HelloWorld);
-		claim_2(initiator, Secret, HelloWorld);
+		/* claim_2(initiator, Secret, HelloWorld); */
 	}
 }
 
diff --git a/spdl/ns3-brutus.spdl b/spdl/ns3-brutus.spdl
index 2021fc0..e207556 100644
--- a/spdl/ns3-brutus.spdl
+++ b/spdl/ns3-brutus.spdl
@@ -2,7 +2,7 @@ const pk: Function;
 secret sk: Function;
 inversekeys (pk,sk);
 
-protocol ns3(I,R)
+protocol ns3brutus(I,R)
 {
 	role I
 	{
@@ -12,7 +12,7 @@ protocol ns3(I,R)
 		send_1(I,R, {I,ni}pk(R) );
 		read_2(R,I, {ni,nr}pk(I) );
 		send_3(I,R, {nr}pk(R) );
-		claim(I,Secret,nr);
+		claim_4(I,Secret,nr);
 	}	
 	
 	role R
@@ -23,7 +23,7 @@ protocol ns3(I,R)
 		read_1(I,R, {I,ni}pk(R) );
 		send_2(R,I, {ni,nr}pk(I) );
 		read_3(I,R, {nr}pk(R) );
-		claim(I,Secret,ni);
+		claim_5(I,Secret,ni);
 	}
 }
 
@@ -38,13 +38,13 @@ compromised sk(Eve);
 /* pre-defined 10 runs, limit using --max-runs parameters */
 /* to be nice to brutus, stupid scenario :( */
 
-run ns3.R(Agent,Bob);
-  run ns3.I(Alice,Agent);
-run ns3.R(Agent,Bob);
-  run ns3.I(Alice,Agent);
-run ns3.R(Agent,Bob);
-  run ns3.I(Alice,Agent);
-run ns3.R(Agent,Bob);
-  run ns3.I(Alice,Agent);
-run ns3.R(Agent,Bob);
-  run ns3.I(Alice,Agent);
+run ns3brutus.R(Agent,Bob);
+  run ns3brutus.I(Alice,Agent);
+run ns3brutus.R(Agent,Bob);
+  run ns3brutus.I(Alice,Agent);
+run ns3brutus.R(Agent,Bob);
+  run ns3brutus.I(Alice,Agent);
+run ns3brutus.R(Agent,Bob);
+  run ns3brutus.I(Alice,Agent);
+run ns3brutus.R(Agent,Bob);
+  run ns3brutus.I(Alice,Agent);
diff --git a/spdl/ns3-nisynch.spdl b/spdl/ns3-nisynch.spdl
index 723bbab..06240e2 100644
--- a/spdl/ns3-nisynch.spdl
+++ b/spdl/ns3-nisynch.spdl
@@ -13,6 +13,7 @@ protocol ns3(I,R)
 		read_2(R,I, {ni,nr}pk(I) );
 		send_3(I,R, {nr}pk(R) );
 		claim_4(I,Nisynch);
+		claim_5(I,Secret, ni,nr);
 	}	
 	
 	role R
@@ -23,14 +24,15 @@ protocol ns3(I,R)
 		read_1(I,R, {I,ni}pk(R) );
 		send_2(R,I, {ni,nr}pk(I) );
 		read_3(I,R, {nr}pk(R) );
-		claim_5(R,Nisynch);
+		claim_6(R,Nisynch);
+		claim_7(R,Secret, ni,nr);
 	}
 }
 
 const Alice,Bob,Eve: Agent;
 
 untrusted Eve;
-const nc: Nonce;
+const ne: Nonce;
 compromised sk(Eve);
 
 run ns3.I(Agent,Agent);
diff --git a/spdl/ns3-var.spdl b/spdl/ns3-var.spdl
index 1db4f8f..142d673 100644
--- a/spdl/ns3-var.spdl
+++ b/spdl/ns3-var.spdl
@@ -2,7 +2,7 @@ const pk: Function;
 secret sk: Function;
 inversekeys (pk,sk);
 
-protocol ns3(I,R)
+protocol ns3var(I,R)
 {
 	role I
 	{
@@ -12,7 +12,7 @@ protocol ns3(I,R)
 		send_1(I,R, {I,ni}pk(R) );
 		read_2(R,I, {ni,nr}pk(I) );
 		send_3(I,R, {nr}pk(R) );
-		claim(I,Secret,ni,nr);
+		claim_4(I,Secret,ni,nr);
 	}	
 	
 	role R
@@ -23,7 +23,7 @@ protocol ns3(I,R)
 		read_1(I,R, {I,ni}pk(R) );
 		send_2(R,I, {ni,nr}pk(I) );
 		read_3(I,R, {nr}pk(R) );
-		claim(R,Secret,ni,nr);
+		claim_5(R,Secret,ni,nr);
 	}
 }
 
@@ -33,5 +33,5 @@ untrusted Eve;
 const nc: Nonce;
 compromised sk(Eve);
 
-run ns3.I(Agent,Agent);
-run ns3.R(Agent,Agent);
+run ns3var.I(Agent,Agent);
+run ns3var.R(Agent,Agent);
diff --git a/spdl/nsl3-nisynch.spdl b/spdl/nsl3-nisynch.spdl
index 23fd05d..b973537 100644
--- a/spdl/nsl3-nisynch.spdl
+++ b/spdl/nsl3-nisynch.spdl
@@ -13,6 +13,7 @@ protocol nsl3(I,R)
 		read_2(R,I, {ni,nr,R}pk(I) );
 		send_3(I,R, {nr}pk(R) );
 		claim_4(I,Nisynch);
+		claim_5(I,Secret,ni,nr);
 	}	
 	
 	role R
@@ -23,14 +24,15 @@ protocol nsl3(I,R)
 		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_5(R,Nisynch);
+		claim_6(R,Nisynch);
+		claim_7(R,Secret,ni,nr);
 	}
 }
 
 const Alice,Bob,Eve: Agent;
 
 untrusted Eve;
-const nc: Nonce;
+const ne: Nonce;
 compromised sk(Eve);
 
 run nsl3.I(Agent,Agent);
diff --git a/spdl/nsl3-var.spdl b/spdl/nsl3-var.spdl
index e586431..78e05a0 100644
--- a/spdl/nsl3-var.spdl
+++ b/spdl/nsl3-var.spdl
@@ -12,7 +12,7 @@ protocol nsl3(I,R)
 		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(I,Secret,ni,nr);
+		claim_4(I,Secret,ni,nr);
 	}	
 	
 	role R
@@ -23,7 +23,7 @@ protocol nsl3(I,R)
 		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(I,Secret,ni,nr);
+		claim_5(I,Secret,ni,nr);
 	}
 }
 
diff --git a/spdl/nsl7.spdl b/spdl/nsl7.spdl
index 3609e23..736e646 100644
--- a/spdl/nsl7.spdl
+++ b/spdl/nsl7.spdl
@@ -12,11 +12,11 @@ protocol nsl7(I,R)
 		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(I,Secret,nr,ni);
+		claim_4(I,Secret,nr,ni);
 	}
 }
 
 const Alice,Bob;
 
-run nsl3.R(Alice,Bob);
-run nsl3.R(Alice,Bob);
+run nsl7.R(Alice,Bob);
+run nsl7.R(Alice,Bob);
diff --git a/spdl/onetrace.spdl b/spdl/onetrace.spdl
index 26ba9c1..5901396 100644
--- a/spdl/onetrace.spdl
+++ b/spdl/onetrace.spdl
@@ -12,6 +12,7 @@ protocol onetrace(I)
 		read_1(I,I, input);
 		send_2(I,I, Hallo);
 		read_3(I,I, input);
+		claim_4(I, Secret, input);
 	}
 }
 
diff --git a/spdl/simplest.spdl b/spdl/simplest.spdl
index 22f3f62..d96633f 100644
--- a/spdl/simplest.spdl
+++ b/spdl/simplest.spdl
@@ -10,8 +10,9 @@ protocol simplest(I)
 		var x: Nonce;
 		const n: Nonce;
 
-		read(I,I, x);
-		send(I,I, n, {n, x}k );
+		read_1(I,I, x);
+		send_2(I,I, n, {n, x}k );
+		claim_3(I, Secret, n);
 	}
 }
 
diff --git a/spdl/soph.spdl b/spdl/soph.spdl
index 905dc61..174f9e1 100644
--- a/spdl/soph.spdl
+++ b/spdl/soph.spdl
@@ -10,7 +10,7 @@ protocol soph(I,R)
 
 		send_1(I,R, {I,ni}pk(R) );
 		read_2(R,I, ni );
-		claim_4(I,Niagree);
+		claim_3(I,Niagree);
 	}	
 	
 	role R
diff --git a/spdl/speedtest.spdl b/spdl/speedtest.spdl
index 1d760f9..ace7cf3 100644
--- a/spdl/speedtest.spdl
+++ b/spdl/speedtest.spdl
@@ -2,7 +2,7 @@ const pk: Function;
 secret sk: Function;
 inversekeys (pk,sk);
 
-protocol ns3(I,R)
+protocol ns3speedtest(I,R)
 {
 	role I
 	{
@@ -12,7 +12,7 @@ protocol ns3(I,R)
 		send_1(I,R, {I,ni}pk(R) );
 		read_2(R,I, {ni,nr}pk(I) );
 		send_3(I,R, {nr}pk(R) );
-		claim(I,Secret,nr);
+		claim_4(I,Secret,nr);
 	}	
 	
 	role R
@@ -23,7 +23,7 @@ protocol ns3(I,R)
 		read_1(I,R, {I,ni}pk(R) );
 		send_2(R,I, {ni,nr}pk(I) );
 		read_3(I,R, {nr}pk(R) );
-		claim(I,Secret,ni);
+		claim_5(I,Secret,ni);
 	}
 }
 
@@ -37,13 +37,13 @@ compromised sk(Eve);
 
 /* pre-defined 10 runs, limit using --max-runs parameters */
 
-run ns3.I(Alice,Bob);
-	run ns3.R(Alice,Bob);
-run ns3.I(Alice,Eve);
-	run ns3.R(Eve,Bob);
-run ns3.I(Bob,Alice);
-	run ns3.R(Bob,Alice);
-run ns3.I(Bob,Eve);
-	run ns3.R(Eve,Alice);
-run ns3.I(Alice,Alice);
-	run ns3.R(Bob,Bob);
+run ns3speedtest.I(Alice,Bob);
+	run ns3speedtest.R(Alice,Bob);
+run ns3speedtest.I(Alice,Eve);
+	run ns3speedtest.R(Eve,Bob);
+run ns3speedtest.I(Bob,Alice);
+	run ns3speedtest.R(Bob,Alice);
+run ns3speedtest.I(Bob,Eve);
+	run ns3speedtest.R(Eve,Alice);
+run ns3speedtest.I(Alice,Alice);
+	run ns3speedtest.R(Bob,Bob);
diff --git a/spdl/woolam-ce.spdl b/spdl/woolam-ce.spdl
index 5d67606..5bbcc65 100644
--- a/spdl/woolam-ce.spdl
+++ b/spdl/woolam-ce.spdl
@@ -29,7 +29,7 @@ protocol woolamce(A,B,S)
    		send_6(B,A, { B,(Na,(Nb,Kab)) }Kas, { Na,Nb }Kab );
 		read_7(A,B, { Nb }Kab );	
 
-		claim(B,Secret,authToken);
+		claim_8(B,Secret,authToken);
 	}
 }