diff --git a/spdl/ns3.spdl b/spdl/ns3.spdl
index 3c250ac..0c305d3 100644
--- a/spdl/ns3.spdl
+++ b/spdl/ns3.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,Secret,ni,nr);
+		claim_6(I,Nisynch);
 	}	
 	
 	role R
@@ -24,6 +25,7 @@ protocol ns3(I,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);
 	}
 }
 
diff --git a/spdl/nsl3-nisynch-rep.spdl b/spdl/nsl3-nisynch-rep.spdl
index e826154..2471e72 100644
--- a/spdl/nsl3-nisynch-rep.spdl
+++ b/spdl/nsl3-nisynch-rep.spdl
@@ -10,10 +10,11 @@ protocol nsl3(I,R)
 		var nr: Nonce;
 
 		send_1(I,R, {I,ni}pk(R) );
+		send_6(I,R, {I,ni}pk(R) );
 		read_2(R,I, {ni,nr,R}pk(I) );
-		read_6(R,I, {ni,nr,R}pk(I) );
 		send_3(I,R, {nr}pk(R) );
-		claim_4(I,Nisynch);
+		claim_4(I,Niagree);
+		claim_7(I,Nisynch);
 	}	
 	
 	role R
@@ -22,10 +23,11 @@ protocol nsl3(I,R)
 		const nr: Nonce;
 
 		read_1(I,R, {I,ni}pk(R) );
+		read_6(I,R, {I,ni}pk(R) );
 		send_2(R,I, {ni,nr,R}pk(I) );
-		send_6(R,I, {ni,nr,R}pk(I) );
 		read_3(I,R, {nr}pk(R) );
-		claim_5(I,Nisynch);
+		claim_5(R,Niagree);
+		claim_8(R,Nisynch);
 	}
 }
 
diff --git a/spdl/nsl3-nisynch.spdl b/spdl/nsl3-nisynch.spdl
index 2baa020..23fd05d 100644
--- a/spdl/nsl3-nisynch.spdl
+++ b/spdl/nsl3-nisynch.spdl
@@ -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_5(I,Nisynch);
+		claim_5(R,Nisynch);
 	}
 }
 
diff --git a/spdl/nsl3.spdl b/spdl/nsl3.spdl
index b74ae11..b85ef9e 100644
--- a/spdl/nsl3.spdl
+++ b/spdl/nsl3.spdl
@@ -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_5(I,Secret,ni,nr);
+		claim_5(R,Secret,ni,nr);
 	}
 }