diff --git a/spdl/bke-ordertest.spdl b/spdl/bke-ordertest.spdl
deleted file mode 100644
index 05a600a..0000000
--- a/spdl/bke-ordertest.spdl
+++ /dev/null
@@ -1,58 +0,0 @@
-/* 
-	Bilateral Key Exchange with Public Key protocol (BKEPK)
-*/
-
-usertype Key;
-
-const pk,hash: Function;
-secret sk,unhash: Function;
-
-inversekeys (pk,sk);
-inversekeys (hash,unhash);
-
-protocol bkepk(I,R)
-{
-	role I
-	{
-		const ni: Nonce;
-		var nr: Nonce;
-		var kir: Key;
-
-		send_1 (I,R, { ni,I }pk(R) );
-		read_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
-		send_3 (I,R, { hash(nr) }kir );
-		claim_4 (I, Secret, kir );
-	}
-
-	role R
-	{
-		var ni: Nonce;
-		const nr: Nonce;
-		const kir: Key;
-
-		read_1 (I,R, { ni,I }pk(R) );
-		send_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
-		read_3 (I,R, { hash(nr) }kir );
-		claim_5 (R, Secret, kir );
-	}
-}
-
-const a,b,e: Agent;
-
-untrusted e;
-compromised sk(e);
-const ne: Nonce;
-
-run bkepk.I(a,Agent);
-run bkepk.I(a,Agent);
-run bkepk.R(Agent,b);
-run bkepk.R(Agent,b);
-
-run bkepk.I(a,Agent);
-run bkepk.R(Agent,b);
-run bkepk.I(a,Agent);
-run bkepk.R(Agent,b);
-
-run bkepk.I(a,Agent);
-run bkepk.R(Agent,b);
-
diff --git a/spdl/ns3-extreme.spdl b/spdl/ns3-extreme.spdl
deleted file mode 100644
index a7b8c94..0000000
--- a/spdl/ns3-extreme.spdl
+++ /dev/null
@@ -1,47 +0,0 @@
-const pk: Function;
-secret sk: Function;
-inversekeys (pk,sk);
-
-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_4(I,Secret,ni,nr);
-	}	
-	
-	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_5(R,Secret,ni,nr);
-	}
-}
-
-const Alice,Bob,Eve: Agent;
-
-/* something like this will later on all be implied by 'untrusted Eve' */
-
-untrusted Eve;
-const nc: Nonce;
-compromised sk(Eve);
-
-/* pre-defined 10 runs, limit using --max-runs parameters */
-
-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/ns3-nisynch.spdl b/spdl/ns3-nisynch.spdl
deleted file mode 100644
index 06240e2..0000000
--- a/spdl/ns3-nisynch.spdl
+++ /dev/null
@@ -1,41 +0,0 @@
-const pk: Function;
-secret sk: Function;
-inversekeys (pk,sk);
-
-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_4(I,Nisynch);
-		claim_5(I,Secret, ni,nr);
-	}	
-	
-	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_6(R,Nisynch);
-		claim_7(R,Secret, ni,nr);
-	}
-}
-
-const Alice,Bob,Eve: Agent;
-
-untrusted Eve;
-const ne: Nonce;
-compromised sk(Eve);
-
-run ns3.I(Agent,Agent);
-run ns3.R(Agent,Agent);
-run ns3.I(Agent,Agent);
-run ns3.R(Agent,Agent);
diff --git a/spdl/ns3-var.spdl b/spdl/ns3-var.spdl
deleted file mode 100644
index 142d673..0000000
--- a/spdl/ns3-var.spdl
+++ /dev/null
@@ -1,37 +0,0 @@
-const pk: Function;
-secret sk: Function;
-inversekeys (pk,sk);
-
-protocol ns3var(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_4(I,Secret,ni,nr);
-	}	
-	
-	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_5(R,Secret,ni,nr);
-	}
-}
-
-const Alice,Bob,Eve : Agent;
-
-untrusted Eve;
-const nc: Nonce;
-compromised sk(Eve);
-
-run ns3var.I(Agent,Agent);
-run ns3var.R(Agent,Agent);
diff --git a/spdl/ns3.spdl b/spdl/ns3.spdl
index 0c305d3..ec5f2db 100644
--- a/spdl/ns3.spdl
+++ b/spdl/ns3.spdl
@@ -12,8 +12,9 @@ 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_4(I,Secret,ni,nr);
-		claim_6(I,Nisynch);
+		claim_i1(I,Secret,ni,nr);
+		claim_i2(I,Niagree);
+		claim_i3(I,Nisynch);
 	}	
 	
 	role R
@@ -24,16 +25,17 @@ 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,Secret,ni,nr);
-		claim_7(R,Nisynch);
+		claim_r1(R,Secret,ni,nr);
+		claim_r2(R,Niagree);
+		claim_r3(R,Nisynch);
 	}
 }
 
 const Alice,Bob,Eve: Agent;
 
 untrusted Eve;
-const nc: Nonce;
+const ne: Nonce;
 compromised sk(Eve);
 
-run ns3.I(Alice,Eve);
-run ns3.R(Alice,Bob);
+run ns3.I(Agent,Agent);
+run ns3.R(Agent,Agent);
diff --git a/spdl/nsl3-2m.spdl b/spdl/nsl3-2m.spdl
deleted file mode 100644
index 471db45..0000000
--- a/spdl/nsl3-2m.spdl
+++ /dev/null
@@ -1,35 +0,0 @@
-const pk: Function;
-secret sk: Function;
-inversekeys (pk,sk);
-
-protocol nsl3x2m(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) );
-		claim_4(I,Secret,ni,nr);
-	}	
-	
-	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) );
-		claim_5(R,Secret,ni,nr);
-	}
-}
-
-const Alice,Bob,Eve: Agent;
-
-untrusted Eve;
-const nc: Nonce;
-compromised sk(Eve);
-
-run nsl3x2m.I(Agent,Agent);
-run nsl3x2m.R(Alice,Bob);
diff --git a/spdl/nsl3-nisynch.spdl b/spdl/nsl3-nisynch.spdl
deleted file mode 100644
index b973537..0000000
--- a/spdl/nsl3-nisynch.spdl
+++ /dev/null
@@ -1,41 +0,0 @@
-const pk: Function;
-secret sk: Function;
-inversekeys (pk,sk);
-
-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_4(I,Nisynch);
-		claim_5(I,Secret,ni,nr);
-	}	
-	
-	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_6(R,Nisynch);
-		claim_7(R,Secret,ni,nr);
-	}
-}
-
-const Alice,Bob,Eve: Agent;
-
-untrusted Eve;
-const ne: Nonce;
-compromised sk(Eve);
-
-run nsl3.I(Agent,Agent);
-run nsl3.R(Agent,Agent);
-run nsl3.I(Agent,Agent);
-run nsl3.R(Agent,Agent);
diff --git a/spdl/nsl3-var.spdl b/spdl/nsl3-var.spdl
deleted file mode 100644
index 78e05a0..0000000
--- a/spdl/nsl3-var.spdl
+++ /dev/null
@@ -1,37 +0,0 @@
-const pk: Function;
-secret sk: Function;
-inversekeys (pk,sk);
-
-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_4(I,Secret,ni,nr);
-	}	
-	
-	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_5(I,Secret,ni,nr);
-	}
-}
-
-const Alice,Bob,Eve: Agent;
-
-untrusted Eve;
-const nc: Nonce;
-compromised sk(Eve);
-
-run nsl3.I(Agent,Agent);
-run nsl3.R(Agent,Agent);
diff --git a/spdl/nsl3.spdl b/spdl/nsl3.spdl
index 524aa79..74e9149 100644
--- a/spdl/nsl3.spdl
+++ b/spdl/nsl3.spdl
@@ -12,8 +12,9 @@ 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_4(I,Secret,ni,nr);
-		claim_6(I,Nisynch);
+		claim_i1(I,Secret,ni,nr);
+		claim_i2(I,Niagree);
+		claim_i3(I,Nisynch);
 	}	
 	
 	role R
@@ -24,16 +25,17 @@ 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,Secret,ni,nr);
-		claim_7(R,Nisynch);
+		claim_r1(R,Secret,ni,nr);
+		claim_r2(R,Niagree);
+		claim_r3(R,Nisynch);
 	}
 }
 
 const Alice,Bob,Eve: Agent;
 
 untrusted Eve;
-const nc: Nonce;
+const ne: Nonce;
 compromised sk(Eve);
 
 run nsl3.I(Agent,Agent);
-run nsl3.R(Alice,Bob);
+run nsl3.R(Agent,Agent);
diff --git a/spdl/nsl7.spdl b/spdl/nsl7.spdl
index 736e646..34449f4 100644
--- a/spdl/nsl7.spdl
+++ b/spdl/nsl7.spdl
@@ -16,7 +16,10 @@ protocol nsl7(I,R)
 	}
 }
 
-const Alice,Bob;
+const Alice,Bob,Eve;
+const ne;
+untrusted Eve;
+compromised sk(Eve);
 
-run nsl7.R(Alice,Bob);
-run nsl7.R(Alice,Bob);
+run nsl7.R(Agent,Agent);
+run nsl7.R(Agent,Agent);