From 939ece7500f565e53ad2c4a931c6c6c4201c07f4 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Fri, 27 Aug 2004 19:08:31 +0000
Subject: [PATCH] - Improvements in the scenarios.

---
 spdl/ns3.spdl              |  2 ++
 spdl/nsl3-nisynch-rep.spdl | 10 ++++++----
 spdl/nsl3-nisynch.spdl     |  2 +-
 spdl/nsl3.spdl             |  2 +-
 4 files changed, 10 insertions(+), 6 deletions(-)

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);
 	}
 }