From 98dd606404e68b9eeee19c601730683178fb9f4d Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Wed, 25 Apr 2012 22:09:46 +0200
Subject: [PATCH] Adding agreement etc. to NS/NSL protocol.

---
 gui/ns3.spdl  | 24 ++++++++++++++----------
 gui/nsl3.spdl | 22 ++++++++++++++--------
 2 files changed, 28 insertions(+), 18 deletions(-)

diff --git a/gui/ns3.spdl b/gui/ns3.spdl
index b7904bf..04846ea 100644
--- a/gui/ns3.spdl
+++ b/gui/ns3.spdl
@@ -13,13 +13,15 @@ protocol ns3(I,R)
 
 		send_1(I,R, {ni,I}pk(R) );
 		recv_2(R,I, {ni,nr}pk(I) );
+		claim(I,Running,R,ni,nr);
 		send_3(I,R, {nr}pk(R) );
 
-		claim_i1(I,Secret,ni);
-		claim_i2(I,Secret,nr);
-		claim_i3(I,Alive);
-		claim_i4(I,Niagree);
-		claim_i5(I,Nisynch);
+		claim(I,Secret,ni);
+		claim(I,Secret,nr);
+		claim(I,Alive);
+		claim(I,Commit,R,ni,nr);
+		claim(I,Niagree);
+		claim(I,Nisynch);
 	}	
 	
 	role R
@@ -28,14 +30,16 @@ protocol ns3(I,R)
 		fresh nr: Nonce;
 
 		recv_1(I,R, {ni,I}pk(R) );
+		claim(R,Running,I,ni,nr);
 		send_2(R,I, {ni,nr}pk(I) );
 		recv_3(I,R, {nr}pk(R) );
 
-		claim_r1(R,Secret,ni);
-		claim_r2(R,Secret,nr);
-		claim_r3(R,Alive);
-		claim_r4(R,Niagree);
-		claim_r5(R,Nisynch);
+		claim(R,Secret,ni);
+		claim(R,Secret,nr);
+		claim(R,Alive);
+		claim(R,Commit,I,ni,nr);
+		claim(R,Niagree);
+		claim(R,Nisynch);
 	}
 }
 
diff --git a/gui/nsl3.spdl b/gui/nsl3.spdl
index a4bfef5..dfbaa68 100644
--- a/gui/nsl3.spdl
+++ b/gui/nsl3.spdl
@@ -13,12 +13,15 @@ protocol nsl3(I,R)
 
 		send_1(I,R, {ni,I}pk(R) );
 		recv_2(R,I, {ni,nr,R}pk(I) );
+		claim(I,Running,R,ni,nr);
 		send_3(I,R, {nr}pk(R) );
 
-		claim_i1(I,Secret,ni);
-		claim_i2(I,Secret,nr);
-		claim_i3(I,Niagree);
-		claim_i4(I,Nisynch);
+		claim(I,Secret,ni);
+		claim(I,Secret,nr);
+		claim(I,Alive);
+		claim(I,Commit,R,ni,nr);
+		claim(I,Niagree);
+		claim(I,Nisynch);
 	}	
 	
 	role R
@@ -27,13 +30,16 @@ protocol nsl3(I,R)
 		fresh nr: Nonce;
 
 		recv_1(I,R, {ni,I}pk(R) );
+		claim(R,Running,I,ni,nr);
 		send_2(R,I, {ni,nr,R}pk(I) );
 		recv_3(I,R, {nr}pk(R) );
 
-		claim_r1(R,Secret,ni);
-		claim_r2(R,Secret,nr);
-		claim_r3(R,Niagree);
-		claim_r4(R,Nisynch);
+		claim(R,Secret,ni);
+		claim(R,Secret,nr);
+		claim(R,Alive);
+		claim(R,Commit,I,ni,nr);
+		claim(R,Niagree);
+		claim(R,Nisynch);
 	}
 }