diff --git a/spdl/SPORE/andrew-ban-concrete.spdl b/spdl/SPORE/andrew-ban-concrete.spdl
index ae03021..91f95ea 100644
--- a/spdl/SPORE/andrew-ban-concrete.spdl
+++ b/spdl/SPORE/andrew-ban-concrete.spdl
@@ -18,17 +18,21 @@
 
 usertype SessionKey;
 secret k: Function;
+const Fresh: Function;
 
-protocol andrewConcrete(I,R,X)
+protocol swapkey(X)
 {
-    
-    # Role added to work around the symmetry problems where k(I,R) != k(R,I)
+    # Protocol added to work around the symmetry problems where k(I,R) != k(R,I)
     role X
     {
-        var T: Ticket;
-        read_X1(X,X, {T}k(I,R));
-        send_X2(X,X, {T}k(R,I));
+        var I,R: Agent;
+        var T:Ticket;
+        read_X1(X,X,I,R,{T}k(I,R));
+        send_X2(X,X,{T}k(R,I));
     }
+}
+protocol andrewConcrete(I,R)
+{
     
     role I
     {
@@ -39,8 +43,9 @@ protocol andrewConcrete(I,R,X)
         send_1(I,R, I,ni );
         read_2(R,I, {ni,kir}k(I,R) );
         send_3(I,R, {ni}kir);
-        claim_4(I,Secret,kir);
-        claim_5(I,Nisynch);
+        claim_I1(I,Secret,kir);
+        claim_I2(I,Nisynch);
+        claim_I3(I,Empty,(Fresh,kir));
         read_6(R,I, nr);
     }    
     
@@ -54,8 +59,9 @@ protocol andrewConcrete(I,R,X)
         send_2(R,I, {ni,kir}k(I,R) );
         read_3(I,R, {ni}kir);
         send_6(R,I, nr);
-        claim_7(R,Secret,kir);
-        claim_8(R,Nisynch);
+        claim_R1(R,Secret,kir);
+        claim_R2(R,Nisynch);
+        claim_R3(R,Empty,(Fresh,kir));
     }
 }
 
diff --git a/spdl/SPORE/andrew-ban.spdl b/spdl/SPORE/andrew-ban.spdl
index dee1d2f..ad11d78 100644
--- a/spdl/SPORE/andrew-ban.spdl
+++ b/spdl/SPORE/andrew-ban.spdl
@@ -13,6 +13,7 @@
 #
 usertype SessionKey;
 secret k: Function;
+const Fresh: Function;
 
 protocol andrewBan(I,R)
 {
@@ -26,10 +27,11 @@ protocol andrewBan(I,R)
         read_2(R,I, {ni,nr}k(I,R) );
         send_3(I,R, {nr}k(I,R) );
         read_4(R,I, {kir,nr2,ni}k(I,R) );
-        claim_5(I,Nisynch);
-        claim_5b(I,Niagree);
-        claim_6(I,Secret, kir);
-        claim_7(I,Secret, k(I,R));
+        claim_I1(I,Nisynch);
+        claim_I2(I,Niagree);
+        claim_I3(I,Secret, kir);
+        claim_I4(I,Secret, k(I,R));
+        claim_I5(I,Empty, (Fresh,kir));
     }    
     
     role R
@@ -42,10 +44,11 @@ protocol andrewBan(I,R)
         send_2(R,I, {ni,nr}k(I,R) );
         read_3(I,R, {nr}k(I,R) );
         send_4(R,I, {kir,nr2,ni}k(I,R) );
-        claim_8(R,Nisynch);
-        claim_8b(R,Niagree);
-        claim_9(R,Secret, kir);
-        claim_10(R,Secret, k(I,R));
+        claim_R1(R,Nisynch);
+        claim_R2(R,Niagree);
+        claim_R3(R,Secret, kir);
+        claim_R4(R,Secret, k(I,R));
+        claim_R5(R,Empty, (Fresh,kir));
     }
 }
 
diff --git a/spdl/SPORE/andrew-lowe-ban.spdl b/spdl/SPORE/andrew-lowe-ban.spdl
index bbb0468..c183ef4 100644
--- a/spdl/SPORE/andrew-lowe-ban.spdl
+++ b/spdl/SPORE/andrew-lowe-ban.spdl
@@ -20,6 +20,7 @@
 
 usertype SessionKey;
 secret k: Function;
+const Fresh: Function;
 
 protocol andrewLoweBan(I,R)
 {
@@ -32,8 +33,9 @@ protocol andrewLoweBan(I,R)
         send_1(I,R, I,ni );
         read_2(R,I, {ni,kir,R}k(I,R) );
         send_3(I,R, {ni}kir );
-        claim_5(I,Nisynch);
-        claim_6(I,Secret, kir);
+        claim_I1(I,Nisynch);
+        claim_I2(I,Secret, kir);
+        claim_I3(I,Empty, (Fresh,kir));
         read_4(R,I, nr );
     }    
     
@@ -47,8 +49,9 @@ protocol andrewLoweBan(I,R)
         send_2(R,I, {ni,kir,R}k(I,R) );
         read_3(I,R, {ni}kir );
         send_4(R,I, nr );
-        claim_8(R,Nisynch);
-        claim_9(R,Secret, kir);
+        claim_R1(R,Nisynch);
+        claim_R2(R,Secret, kir);
+        claim_R3(R,Empty, (Fresh,kir));
     }
 }
 
diff --git a/spdl/SPORE/andrew.spdl b/spdl/SPORE/andrew.spdl
index bd88ebd..abaad45 100644
--- a/spdl/SPORE/andrew.spdl
+++ b/spdl/SPORE/andrew.spdl
@@ -12,6 +12,7 @@
 usertype SessionKey;
 secret k: Function;
 const succ: Function;
+const Fresh: Function;
 
 protocol andrew(I,R)
 {
@@ -25,8 +26,10 @@ protocol andrew(I,R)
         read_2(R,I, {succ(ni),nr}k(I,R) );
         send_3(I,R, {succ(nr)}k(I,R) );
         read_4(R,I, {kir,nr2}k(I,R) );
-        claim_5(I,Secret,kir);
-        claim_6(I,Nisynch);
+        claim_I1(I,Secret,kir);
+        claim_I2(I,Nisynch);
+        claim_I3(I,Niagree);
+        claim_I4(I,Empty,(Fresh,kir));
     }    
     
     role R
@@ -39,8 +42,10 @@ protocol andrew(I,R)
         send_2(R,I, {succ(ni),nr}k(I,R) );
         read_3(I,R, {succ(nr)}k(I,R) );
         send_4(R,I, {kir,nr2}k(I,R) );
-        claim_7(R,Secret,kir);
-        claim_8(R,Nisynch);
+        claim_R1(R,Secret,kir);
+        claim_R2(R,Nisynch);
+        claim_R3(R,Niagree);
+        claim_R4(R,Empty,(Fresh,kir));
     }
 }
 
diff --git a/spdl/SPORE/denning-sacco-lowe.spdl b/spdl/SPORE/denning-sacco-lowe.spdl
index 00af7e8..ccd4181 100644
--- a/spdl/SPORE/denning-sacco-lowe.spdl
+++ b/spdl/SPORE/denning-sacco-lowe.spdl
@@ -17,6 +17,7 @@ usertype TimeStamp;
 secret k: Function;
 usertype PseudoFunction;
 const dec: PseudoFunction;
+const Fresh: Function;
 
 protocol denningSaccoLowe(I,R,S)
 {
@@ -32,7 +33,10 @@ protocol denningSaccoLowe(I,R,S)
         send_3(I,R, W);
         read_4(R,I, {Nr}Kir);
         send_5(I,R, {{Nr}dec}Kir);
-        claim_6(I,Niagree);
+        claim_I1(I,Niagree);
+        claim_I2(I,Nisynch);
+        claim_I3(I,Secret,Kir);
+        claim_I4(I,Empty,(Fresh,Kir));
     }    
     
     role R
@@ -44,7 +48,10 @@ protocol denningSaccoLowe(I,R,S)
         read_3(I,R, {Kir,I,T}k(R,S));
         send_4(R,I, {Nr}Kir);
         read_5(I,R, {{Nr}dec}Kir);
-        claim_8(R,Niagree);
+        claim_R1(R,Niagree);
+        claim_R2(R,Nisynch);
+        claim_R3(R,Secret,Kir);
+        claim_R4(R,Empty,(Fresh,Kir));
     }
     
     role S
diff --git a/spdl/SPORE/denning-sacco.spdl b/spdl/SPORE/denning-sacco.spdl
index 45af828..c489434 100644
--- a/spdl/SPORE/denning-sacco.spdl
+++ b/spdl/SPORE/denning-sacco.spdl
@@ -12,6 +12,7 @@ usertype Key;
 usertype SessionKey;
 usertype TimeStamp;
 secret k: Function;
+const Fresh: Function;
 
 protocol denningSacco(I,R,S)
 {
@@ -26,6 +27,8 @@ protocol denningSacco(I,R,S)
         send_3(I,R, W);
         claim_I1(I,Niagree);
         claim_I2(I,Nisynch);
+        claim_I3(I,Secret,Kir);
+        claim_I4(I,Empty, (Fresh,Kir));
     }    
     
     role R
@@ -36,7 +39,8 @@ protocol denningSacco(I,R,S)
         read_3(I,R, {Kir,I,T}k(R,S));
         claim_R1(R,Niagree);
         claim_R2(R,Nisynch);
-
+        claim_R3(R,Secret,Kir);
+        claim_R4(R,Empty, (Fresh,Kir));
     }
     
     role S
diff --git a/spdl/SPORE/kaochow-v2.spdl b/spdl/SPORE/kaochow-v2.spdl
index 447e6e6..cd44372 100644
--- a/spdl/SPORE/kaochow-v2.spdl
+++ b/spdl/SPORE/kaochow-v2.spdl
@@ -10,6 +10,7 @@
 
 usertype Sessionkey;
 secret k: Function;
+const Fresh: Function;
 
 protocol kaochow2(I,R,S)
 {
@@ -23,9 +24,10 @@ protocol kaochow2(I,R,S)
         read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr );
         send_4 (I,R, {nr,kir}kt );
 
-        claim_5 (I, Nisynch);
-        claim_6 (I, Niagree);
-        claim_7 (I, Secret, kir);
+        claim_I1 (I, Nisynch);
+        claim_I2 (I, Niagree);
+        claim_I3 (I, Secret, kir);
+        claim_I4 (I, Empty, (Fresh,kir));
     }    
     
     role R
@@ -39,9 +41,10 @@ protocol kaochow2(I,R,S)
         send_3 (R,I, R, T, {ni, kir}kt, nr );
         read_4 (I,R, {nr,kir}kt );
 
-        claim_8 (R, Nisynch);
-        claim_9 (R, Niagree);
-        claim_10 (R, Secret, kir);
+        claim_R1 (R, Nisynch);
+        claim_R2 (R, Niagree);
+        claim_R3 (R, Secret, kir);
+        claim_R4 (R, Empty, (Fresh,kir));
     }
 
     role S
diff --git a/spdl/SPORE/kaochow-v3.spdl b/spdl/SPORE/kaochow-v3.spdl
index a01c8d8..ef2329e 100644
--- a/spdl/SPORE/kaochow-v3.spdl
+++ b/spdl/SPORE/kaochow-v3.spdl
@@ -11,6 +11,7 @@
 usertype Sessionkey;
 usertype Timestamp;
 secret k: Function;
+const Fresh: Function;
 
 protocol kaochow3(I,R,S)
 {
@@ -25,9 +26,10 @@ protocol kaochow3(I,R,S)
         read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 );
         send_4 (I,R, {nr,kir}kt, T2 );
 
-        claim_5 (I, Nisynch);
-        claim_6 (I, Niagree);
-        claim_7 (I, Secret, kir);
+        claim_I1 (I, Nisynch);
+        claim_I2 (I, Niagree);
+        claim_I3 (I, Secret, kir);
+        claim_I4 (I, Empty, (Fresh,kir));
     }    
     
     role R
@@ -42,9 +44,10 @@ protocol kaochow3(I,R,S)
         send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) );
         read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) );
 
-        claim_8 (R, Nisynch);
-        claim_9 (R, Niagree);
-        claim_10 (R, Secret, kir);
+        claim_R1 (R, Nisynch);
+        claim_R2 (R, Niagree);
+        claim_R3 (R, Secret, kir);
+        claim_R4 (R, Empty, (Fresh,kir));
     }
 
     role S
diff --git a/spdl/SPORE/kaochow.spdl b/spdl/SPORE/kaochow.spdl
index 55b1bb3..c50147e 100644
--- a/spdl/SPORE/kaochow.spdl
+++ b/spdl/SPORE/kaochow.spdl
@@ -10,6 +10,7 @@
 
 usertype Sessionkey;
 secret k: Function;
+const Fresh: Function;
 
 protocol kaochow(I,R,S)
 {
@@ -23,9 +24,10 @@ protocol kaochow(I,R,S)
         read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr );
         send_4 (I,R, {nr}kir );
 
-        claim_5 (I, Nisynch);
-        claim_6 (I, Niagree);
-        claim_7 (I, Secret, kir);
+        claim_I1 (I, Nisynch);
+        claim_I2 (I, Niagree);
+        claim_I3 (I, Secret, kir);
+        claim_I4 (I, Empty, (Fresh,kir));
     }    
     
     role R
@@ -39,9 +41,10 @@ protocol kaochow(I,R,S)
         send_3 (R,I, T, {ni}kir, nr );
         read_4 (I,R, {nr}kir );
 
-        claim_8 (R, Nisynch);
-        claim_9 (R, Niagree);
-        claim_10 (R, Secret, kir);
+        claim_R1 (R, Nisynch);
+        claim_R2 (R, Niagree);
+        claim_R3 (R, Secret, kir);
+        claim_R4 (R, Empty, (Fresh,kir));
     }
 
     role S
diff --git a/spdl/SPORE/ksl-lowe.spdl b/spdl/SPORE/ksl-lowe.spdl
index 001bc59..463f79e 100644
--- a/spdl/SPORE/ksl-lowe.spdl
+++ b/spdl/SPORE/ksl-lowe.spdl
@@ -16,6 +16,7 @@ secret k: Function;
 
 const a, b, e: Agent;
 const s: Server;
+const Fresh: Function;
 
 
 const ne: Nonce;
@@ -43,6 +44,7 @@ protocol kslLowe(A,B,S)
         claim_A1(A,Secret, Kab);
         claim_A2(A,Niagree);
         claim_A3(A,Nisynch);
+        claim_A4(A,Empty, (Fresh,Kab));
     }
 
     role B
@@ -67,6 +69,7 @@ protocol kslLowe(A,B,S)
         claim_B1(B,Secret, Kab);
         claim_B2(B,Niagree);
         claim_B3(B,Nisynch);
+        claim_B4(B,Empty, (Fresh,Kab));
     }
 
     role S
diff --git a/spdl/SPORE/ksl.spdl b/spdl/SPORE/ksl.spdl
index 196bd36..dbd73cc 100644
--- a/spdl/SPORE/ksl.spdl
+++ b/spdl/SPORE/ksl.spdl
@@ -14,6 +14,7 @@ secret k: Function;
 
 const a, b, e: Agent;
 const s: Server;
+const Fresh: Function;
 
 const ne: Nonce;
 const kee: SessionKey;
@@ -40,6 +41,7 @@ protocol ksl(A,B,S)
         claim_A1(A,Secret, Kab);
         claim_A2(A,Niagree);
         claim_A3(A,Nisynch);
+        claim_A4(A,Empty, (Fresh, Kab));
     }
 
     role B
@@ -64,6 +66,7 @@ protocol ksl(A,B,S)
         claim_B1(B,Secret, Kab);
         claim_B2(B,Niagree);
         claim_B3(B,Nisynch);
+        claim_B4(B,Empty,(Fresh,Kab));
     }
 
     role S
diff --git a/spdl/SPORE/needham-schroeder-sk-amend.spdl b/spdl/SPORE/needham-schroeder-sk-amend.spdl
index b25fdec..d18d0f1 100644
--- a/spdl/SPORE/needham-schroeder-sk-amend.spdl
+++ b/spdl/SPORE/needham-schroeder-sk-amend.spdl
@@ -19,6 +19,7 @@ secret k: Function;
 const dec,inc: Function;
 inversekeys(dec,inc);
 usertype SessionKey;
+const Fresh: Function;
 
 protocol needhamschroederskamend(I,R,S)
 {
@@ -39,6 +40,7 @@ protocol needhamschroederskamend(I,R,S)
         
         claim_I2(I,Secret,Kir);
         claim_I3(I,Nisynch);
+        claim_I4(I,Empty,(Fresh,Kir));
     }    
     
     role R
@@ -53,6 +55,7 @@ protocol needhamschroederskamend(I,R,S)
         read_7(I,R,{{Nr}dec}Kir);
         claim_R1(R,Secret,Nr);
         claim_R3(R,Nisynch);
+        claim_R4(R,Empty,(Fresh,Kir));
     }
 
     role S
diff --git a/spdl/SPORE/needham-schroeder-sk.spdl b/spdl/SPORE/needham-schroeder-sk.spdl
index 3ef425d..08288ed 100644
--- a/spdl/SPORE/needham-schroeder-sk.spdl
+++ b/spdl/SPORE/needham-schroeder-sk.spdl
@@ -15,6 +15,7 @@ secret k: Function;
 const dec,inc: Function;
 inversekeys(dec,inc);
 usertype SessionKey;
+const Fresh: Function;
 
 protocol needhamschroedersk(I,R,S)
 {
@@ -32,6 +33,7 @@ protocol needhamschroedersk(I,R,S)
         send_5(I,R,{{Nr}dec}Kir);
         claim_I2(I,Secret,Kir);
         claim_I3(I,Nisynch);
+        claim_I4(I,Empty,(Fresh,Kir));
     }    
     
     role R
@@ -44,6 +46,7 @@ protocol needhamschroedersk(I,R,S)
         read_5(I,R,{{Nr}dec}Kir);
         claim_R1(R,Secret,Kir);
         claim_R3(R,Nisynch);
+        claim_R4(R,Empty,(Fresh,Kir));
     }
 
     role S
diff --git a/spdl/SPORE/neumannstub-hwang.spdl b/spdl/SPORE/neumannstub-hwang.spdl
index 42d9f02..8b44c7c 100644
--- a/spdl/SPORE/neumannstub-hwang.spdl
+++ b/spdl/SPORE/neumannstub-hwang.spdl
@@ -17,6 +17,7 @@ secret k: Function;
 
 const a, b, e: Agent;
 const s: Server;
+const Fresh: Function;
 
 const ne: Nonce;
 const kee: SessionKey;
@@ -43,6 +44,7 @@ protocol neustubHwang(I,R,S)
         claim_I1(I,Secret, Kir);
         claim_I2(I,Niagree);
         claim_I3(I,Nisynch);
+        claim_I4(I,Empty,(Fresh,Kir));
     }
 
     role R
@@ -63,6 +65,7 @@ protocol neustubHwang(I,R,S)
         claim_R1(R,Secret, Kir);
         claim_R2(R,Niagree);
         claim_R3(R,Nisynch);
+        claim_R4(R,Empty,(Fresh,Kir));
     }
 
     role S
diff --git a/spdl/SPORE/neumannstub.spdl b/spdl/SPORE/neumannstub.spdl
index d3edd95..fd810b2 100644
--- a/spdl/SPORE/neumannstub.spdl
+++ b/spdl/SPORE/neumannstub.spdl
@@ -14,6 +14,7 @@ secret k: Function;
 
 const a, b, e: Agent;
 const s: Server;
+const Fresh: Function;
 
 const ne: Nonce;
 const kee: SessionKey;
@@ -40,6 +41,7 @@ protocol neustub(I,R,S)
         claim_I1(I,Secret, Kir);
         claim_I2(I,Niagree);
         claim_I3(I,Nisynch);
+        claim_I4(I,Empty,(Fresh,Kir));
     }
 
     role R
@@ -60,6 +62,7 @@ protocol neustub(I,R,S)
         claim_R1(R,Secret, Kir);
         claim_R2(R,Niagree);
         claim_R3(R,Nisynch);
+        claim_R4(R,Empty,(Fresh,Kir));
     }
 
     role S
diff --git a/spdl/SPORE/otwayrees.spdl b/spdl/SPORE/otwayrees.spdl
index 5700104..b32455f 100644
--- a/spdl/SPORE/otwayrees.spdl
+++ b/spdl/SPORE/otwayrees.spdl
@@ -11,6 +11,7 @@
 
 
 secret const k : Function;
+const Fresh: Function;
 
 usertype String,SessionKey;
 
@@ -26,7 +27,8 @@ protocol otwayrees(I,R,S)
         read_4(R,I, M,{Ni,Kir}k(I,S) );
 
         claim_I1(I, Secret,Kir);
-        #claim_I2(I, Nisynch);
+        claim_I2(I, Nisynch);
+        claim_I3(I, Empty, (Fresh,Kir));
     }
 
     role R
@@ -42,7 +44,8 @@ protocol otwayrees(I,R,S)
         send_4(R,I, M, T2 );
 
         claim_R1(R, Secret,Kir);
-        #claim_R2(R, Nisynch);
+        claim_R2(R, Nisynch);
+        claim_R3(R, Empty, (Fresh,Kir));
     }
 
     role S
diff --git a/spdl/SPORE/tmn.spdl b/spdl/SPORE/tmn.spdl
index f3934a0..1109925 100644
--- a/spdl/SPORE/tmn.spdl
+++ b/spdl/SPORE/tmn.spdl
@@ -3,12 +3,16 @@
 # Modelled after the description in the SPORE library
 # http://www.lsv.ens-cachan.fr/spore/tmn.html
 #
+# Note:
+# According to Boyd and Mathuria Kb is the session key this is not clear
+# from the description in SPORE
 
 usertype Key;
 
 const pk: Function;
 secret sk: Function;
 inversekeys(pk,sk);
+const Fresh: Function;
 
 protocol tmn(I,R,S)
 {
@@ -20,8 +24,9 @@ protocol tmn(I,R,S)
         send_1(I,S, R,{Ki}pk(S) );
         read_4(S,I, R,{Kr}Ki );
 
-        claim_I1(I,Secret,Ki);
-        claim_I2(I,Secret,Kr);
+        claim_I1(I,Secret,Kr);
+        claim_I2(I,Nisynch);
+        claim_I3(I,Empty,(Fresh,Kr));
     }    
     
     role R
@@ -32,6 +37,8 @@ protocol tmn(I,R,S)
         send_3(R,S, I, { Kr }pk(S) );
 
         claim_R1(R,Secret,Kr);
+        claim_R2(R,Nisynch);
+        claim_R3(R,Empty,(Fresh,Kr));
     }
 
     role S
diff --git a/spdl/SPORE/wmf-lowe.spdl b/spdl/SPORE/wmf-lowe.spdl
index 66c992d..b902ec2 100644
--- a/spdl/SPORE/wmf-lowe.spdl
+++ b/spdl/SPORE/wmf-lowe.spdl
@@ -13,6 +13,7 @@ usertype Key;
 usertype TimeStamp;
 const succ,pred: Function;
 inversekeys (succ,pred);
+const Fresh: Function;
 
 secret k: Function;
 
@@ -31,6 +32,7 @@ protocol wmfLowe(I,R,S)
 
         claim_I1(I,Secret,Kir);
         claim_I2(I,Nisynch);
+        claim_I3(I,Empty,(Fresh,Kir));
     }    
     
     role R
@@ -45,6 +47,7 @@ protocol wmfLowe(I,R,S)
 
         claim_R1(R,Secret,Kir);
         claim_R2(R,Nisynch);
+        claim_R3(R,Empty,(Fresh,Kir));
     }
 
     role S
diff --git a/spdl/SPORE/wmf.spdl b/spdl/SPORE/wmf.spdl
index 0a01f83..b9ed62b 100644
--- a/spdl/SPORE/wmf.spdl
+++ b/spdl/SPORE/wmf.spdl
@@ -8,6 +8,7 @@ usertype Key;
 usertype TimeStamp;
 
 secret k: Function;
+const Fresh: Function;
 
 protocol wmf(I,R,S)
 {
@@ -20,6 +21,7 @@ protocol wmf(I,R,S)
         send_1(I,S, I, {Ti, R, Kir}k(I,S)); 
 
         claim_I1(I,Secret,Kir);
+        claim_I2(I,Empty,(Fresh,Kir));
     }    
     
     role R
@@ -31,6 +33,7 @@ protocol wmf(I,R,S)
 
         claim_R1(R,Secret,Kir);
         claim_R2(R,Nisynch);
+        claim_R3(R,Empty,(Fresh,Kir));
     }
 
     role S
diff --git a/spdl/SPORE/woo-lam.spdl b/spdl/SPORE/woo-lam.spdl
index b20a259..4fdfe9e 100644
--- a/spdl/SPORE/woo-lam.spdl
+++ b/spdl/SPORE/woo-lam.spdl
@@ -12,6 +12,7 @@
 usertype Key;
 
 secret k: Function;
+const Fresh: Function;
 
 protocol woolam(I,R,S)
 {
@@ -30,6 +31,7 @@ protocol woolam(I,R,S)
 
         claim_I1(I,Secret,Kir);
         claim_I2(I,Nisynch);
+        claim_I3(I,Empty,(Fresh,Kir));
     }    
     
     role R
@@ -49,6 +51,7 @@ protocol woolam(I,R,S)
         
         claim_R1(R,Secret,Kir);
         claim_R2(R,Nisynch);
+        claim_R3(R,Empty,(Fresh,Kir));
     }
 
     role S
diff --git a/spdl/SPORE/yahalom-ban.spdl b/spdl/SPORE/yahalom-ban.spdl
index bc973b7..27a7137 100644
--- a/spdl/SPORE/yahalom-ban.spdl
+++ b/spdl/SPORE/yahalom-ban.spdl
@@ -11,6 +11,7 @@
 secret k : Function;
 
 usertype Key;
+const Fresh: Function;
 
 
 protocol yahalomBAN(I,R,S)
@@ -28,6 +29,7 @@ protocol yahalomBAN(I,R,S)
 
         claim_I1(I, Secret,Kir);
         claim_I2(I, Nisynch);
+        claim_I3(I, Empty, (Fresh,Kir));
     }
 
     role R
@@ -43,6 +45,7 @@ protocol yahalomBAN(I,R,S)
 
         claim_R1(R, Secret,Kir);
         claim_R2(R, Nisynch);
+        claim_R3(R, Empty, (Fresh,Kir));
     }
 
     role S
diff --git a/spdl/SPORE/yahalom-paulson.spdl b/spdl/SPORE/yahalom-paulson.spdl
index c2340a5..cc852db 100644
--- a/spdl/SPORE/yahalom-paulson.spdl
+++ b/spdl/SPORE/yahalom-paulson.spdl
@@ -9,6 +9,7 @@
 #
 
 secret k : Function;
+const Fresh: Function;
 
 usertype Key;
 
@@ -28,6 +29,7 @@ protocol yahalomPaulson(I,R,S)
 
         claim_I1(I, Secret,Kir);
         claim_I2(I, Nisynch);
+        claim_I3(I, Empty, (Fresh,Kir));
     }
 
     role R
@@ -43,6 +45,7 @@ protocol yahalomPaulson(I,R,S)
 
         claim_R1(R, Secret,Kir);
         claim_R2(R, Nisynch);
+        claim_R3(R, Empty, (Fresh,Kir));
     }
 
     role S
diff --git a/spdl/SPORE/yahalom.spdl b/spdl/SPORE/yahalom.spdl
index 46ee432..5cb6f6d 100644
--- a/spdl/SPORE/yahalom.spdl
+++ b/spdl/SPORE/yahalom.spdl
@@ -11,6 +11,7 @@
 secret k : Function;
 
 usertype Key;
+const Fresh: Function;
 
 
 protocol yahalom(I,R,S)
@@ -28,6 +29,7 @@ protocol yahalom(I,R,S)
 
         claim_I1(I, Secret,Kir);
         claim_I2(I, Nisynch);
+        claim_I3(I, Empty, (Fresh,Kir));
     }
 
     role R
@@ -43,6 +45,7 @@ protocol yahalom(I,R,S)
 
         claim_R1(R, Secret,Kir);
         claim_R2(R, Nisynch);
+        claim_R3(R, Empty, (Fresh,Kir));
     }
 
     role S