From 658f4f392a79b1d22657f5e4496e7970e4c378fa Mon Sep 17 00:00:00 2001
From: gijs <gijs@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Thu, 23 Jun 2005 12:49:34 +0000
Subject: [PATCH] - Add Compromised claim to test my new definition of
 freshness in combination   with key compromise (appears to be working pretty
 well)

---
 spdl/SPORE/key-compromise/needham-schroeder-sk.spdl | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl b/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl
index b61f053..d648798 100644
--- a/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl
+++ b/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl
@@ -15,6 +15,8 @@ secret k: Function;
 const dec,inc: Function;
 inversekeys(dec,inc);
 usertype SessionKey;
+const Fresh: Function;
+const Compromised: Function;
 
 protocol needhamschroederSessionKeyCompromise(C)
 {
@@ -33,6 +35,7 @@ protocol needhamschroederSessionKeyCompromise(C)
                         {{Nr}dec}Kir,
                         Kir
                );
+        claim_C3(C,Empty, (Compromised,Kir));
     }
 }
 
@@ -52,6 +55,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
@@ -64,6 +68,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