From 49d314d0f5dc030baf47b0e7c0068d71af793761 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Sat, 19 Feb 2005 14:25:30 +0000
Subject: [PATCH] - Unfolded secrecy claims.

---
 spdl/bkepk.spdl        |  6 ++++--
 spdl/ccitt509-ban.spdl | 10 ++++++----
 spdl/gong-nonce-b.spdl |  8 +++++---
 spdl/gong-nonce.spdl   |  8 +++++---
 spdl/ns3.spdl          | 14 ++++++++------
 spdl/nsl3.spdl         | 14 ++++++++------
 spdl/nsl7.spdl         |  3 ++-
 spdl/tmn.spdl          |  3 ++-
 8 files changed, 40 insertions(+), 26 deletions(-)

diff --git a/spdl/bkepk.spdl b/spdl/bkepk.spdl
index d83c30c..a42d57f 100644
--- a/spdl/bkepk.spdl
+++ b/spdl/bkepk.spdl
@@ -23,7 +23,8 @@ protocol bkepk(A,B)
 		send_1 (B,A, B,{ nb,B }pk(A) );
 		read_2 (A,B, { hash(nb),na,A,kab }pk(B) );
 		send_3 (B,A, { hash(na) }kab );
-		claim_4 (B, Secret, na,nb );
+		claim_4 (B, Secret, na );
+		claim_5 (B, Secret, nb );
 	}
 
 	role A
@@ -35,7 +36,8 @@ protocol bkepk(A,B)
 		read_1 (B,A, B,{ nb,B }pk(A) );
 		send_2 (A,B, { hash(nb),na,A,kab }pk(B) );
 		read_3 (B,A, { hash(na) }kab );
-		claim_5 (A, Secret, na,nb );
+		claim_6 (A, Secret, na );
+		claim_7 (A, Secret, nb );
 	}
 }
 
diff --git a/spdl/ccitt509-ban.spdl b/spdl/ccitt509-ban.spdl
index 1e51f92..9f9ceda 100644
--- a/spdl/ccitt509-ban.spdl
+++ b/spdl/ccitt509-ban.spdl
@@ -16,8 +16,9 @@ protocol ccitt509(I,R)
 		read_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) );
 		send_3(I,R, I,{R,nr}sk(I) );
 
-		claim_4(I,Secret,yi,yr);
-		claim_5(I,Nisynch);
+		claim_4(I,Secret,yi);
+		claim_5(I,Secret,yr);
+		claim_6(I,Nisynch);
 	}	
 	
 	role R
@@ -31,8 +32,9 @@ protocol ccitt509(I,R)
 		send_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) );
 		read_3(I,R, I,{R,nr}sk(I) );
 
-		claim_7(R,Secret,yi,yr);
-		claim_8(R,Nisynch);
+		claim_7(R,Secret,yi);
+		claim_8(R,Secret,yr);
+		claim_9(R,Nisynch);
 	}
 }
 
diff --git a/spdl/gong-nonce-b.spdl b/spdl/gong-nonce-b.spdl
index 30839c0..fd1576b 100644
--- a/spdl/gong-nonce-b.spdl
+++ b/spdl/gong-nonce-b.spdl
@@ -23,7 +23,8 @@ protocol gongnonceb(I,R,S)
 		read_4 (S,I, { S,I,R,kr,I }k(I,S), { R,I,ni }f(ki,kr), nr );
 		send_5 (I,R, { I,R,nr }f(ki,kr) );
 
-		claim_6 (I, Secret, ki,kr);
+		claim_6 (I, Secret, ki);
+		claim_7 (I, Secret, kr);
 		claim_8 (I, Nisynch);
 	}	
 	
@@ -38,8 +39,9 @@ protocol gongnonceb(I,R,S)
 		send_3 (R,S, { R,S,R,kr,I }k(R,S), { R,I, ni }f(ki,kr), nr );
 		read_5 (I,R, { I,R,nr }f(ki,kr) );
 
-		claim_7 (R, Secret, ki,kr);
-		claim_9 (R, Nisynch);
+		claim_9 (R, Secret, ki);
+		claim_10 (R, Secret, kr);
+		claim_11 (R, Nisynch);
 	}
 
 	role S
diff --git a/spdl/gong-nonce.spdl b/spdl/gong-nonce.spdl
index 7c5b634..2b35cc7 100644
--- a/spdl/gong-nonce.spdl
+++ b/spdl/gong-nonce.spdl
@@ -15,7 +15,8 @@ protocol gongnonce(I,R,S)
 		read_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr);
 		send_4 (I,S, { I,S,I, ki, R, nr }k(I,S) );
 
-		claim_6 (I, Secret, ki,kr);
+		claim_6 (I, Secret, ki);
+		claim_7 (I, Secret, kr);
 		claim_8 (I, Nisynch);
 	}	
 	
@@ -30,8 +31,9 @@ protocol gongnonce(I,R,S)
 		send_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S));
 		read_5 (S,R, { S,R,I, ki, R, nr }k(R,S) );
 
-		claim_7 (R, Secret, ki,kr);
-		claim_9 (R, Nisynch);
+		claim_9 (R, Secret, ki);
+		claim_10 (R, Secret, kr);
+		claim_11 (R, Nisynch);
 	}
 
 	role S
diff --git a/spdl/ns3.spdl b/spdl/ns3.spdl
index ec5f2db..26b3081 100644
--- a/spdl/ns3.spdl
+++ b/spdl/ns3.spdl
@@ -12,9 +12,10 @@ 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_i1(I,Secret,ni,nr);
-		claim_i2(I,Niagree);
-		claim_i3(I,Nisynch);
+		claim_i1(I,Secret,ni);
+		claim_i2(I,Secret,nr);
+		claim_i3(I,Niagree);
+		claim_i4(I,Nisynch);
 	}	
 	
 	role R
@@ -25,9 +26,10 @@ 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_r1(R,Secret,ni,nr);
-		claim_r2(R,Niagree);
-		claim_r3(R,Nisynch);
+		claim_r1(R,Secret,ni);
+		claim_r2(R,Secret,nr);
+		claim_r3(R,Niagree);
+		claim_r4(R,Nisynch);
 	}
 }
 
diff --git a/spdl/nsl3.spdl b/spdl/nsl3.spdl
index 74e9149..8ccecde 100644
--- a/spdl/nsl3.spdl
+++ b/spdl/nsl3.spdl
@@ -12,9 +12,10 @@ 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_i1(I,Secret,ni,nr);
-		claim_i2(I,Niagree);
-		claim_i3(I,Nisynch);
+		claim_i1(I,Secret,ni);
+		claim_i2(I,Secret,nr);
+		claim_i3(I,Niagree);
+		claim_i4(I,Nisynch);
 	}	
 	
 	role R
@@ -25,9 +26,10 @@ 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_r1(R,Secret,ni,nr);
-		claim_r2(R,Niagree);
-		claim_r3(R,Nisynch);
+		claim_r1(R,Secret,ni);
+		claim_r2(R,Secret,nr);
+		claim_r3(R,Niagree);
+		claim_r4(R,Nisynch);
 	}
 }
 
diff --git a/spdl/nsl7.spdl b/spdl/nsl7.spdl
index 34449f4..1688a46 100644
--- a/spdl/nsl7.spdl
+++ b/spdl/nsl7.spdl
@@ -12,7 +12,8 @@ protocol nsl7(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_4(I,Secret,nr,ni);
+		claim_4(I,Secret,ni);
+		claim_5(I,Secret,nr);
 	}
 }
 
diff --git a/spdl/tmn.spdl b/spdl/tmn.spdl
index fb14a7a..bdd0dab 100644
--- a/spdl/tmn.spdl
+++ b/spdl/tmn.spdl
@@ -14,7 +14,8 @@ protocol tmn(A,B,S)
 		send_1(A,S, B,{Ka}pk(S) );
 		read_4(S,A, B,{Kb}Ka );
 
-		claim_5(A,Secret,Ka,Kb);
+		claim_5(A,Secret,Ka);
+		claim_8(A,Secret,Kb);
 	}	
 	
 	role B