diff --git a/spdl/ns-symmetric-amended.spdl b/spdl/ns-symmetric-amended.spdl
index 534a886..9231c85 100644
--- a/spdl/ns-symmetric-amended.spdl
+++ b/spdl/ns-symmetric-amended.spdl
@@ -51,6 +51,8 @@ protocol nssymmetricamended(A,S,B)
 		send_7(A,B, { {nb}succ }kab );
 
 		claim_8(A, Secret, kab);
+		claim_8a(A, Niagree);
+		claim_8b(A, Nisynch);
 	}
 
 	role S
@@ -75,5 +77,7 @@ protocol nssymmetricamended(A,S,B)
 		read_7(A,B, { {nb}succ }kab );
 
 		claim_9(B, Secret, kab);
+		claim_9a(B, Niagree);
+		claim_9b(B, Nisynch);
 	}
 }
diff --git a/spdl/otwayrees.spdl b/spdl/otwayrees.spdl
index b81e201..b26552a 100644
--- a/spdl/otwayrees.spdl
+++ b/spdl/otwayrees.spdl
@@ -18,6 +18,8 @@ protocol otwayrees(A,B,S)
 		read_4(B,A, M, { na,kab }k(A,S) );
 
 		claim_5(A, Secret,kab);
+		claim_5b(A, Niagree);
+		claim_5c(A, Nisynch);
 	}
 
 	role B
@@ -33,6 +35,8 @@ protocol otwayrees(A,B,S)
 		send_4(B,A, M, t2 );
 
 		claim_6(B, Secret,kab);
+		claim_6a(B, Niagree);
+		claim_6b(B, Nisynch);
 	}
 
 	role S