- Add @ to swapkey, to disable it in classification

- Modify key Compromise for protocols that contain a timestamp to make the
  key compromise disclose a timestamp with a different type, namely 
  ExpiredTimeStamp so that they will not be accepted as timestamps in a new
  session, thereby simulating that they are expired.

spdl/SPORE/andrew-ban-concrete.spdl

@@ -21,7 +21,7 @@ secret k: Function;
 const Fresh: Function;
 const Compromised: Function;
 
-protocol swapkey(X)
+protocol @swapkey(X)
 {
     # Protocol added to work around the symmetry problems where k(I,R) != k(R,I)
     role X

spdl/SPORE/denning-sacco-lowe.spdl

@@ -14,6 +14,7 @@
 usertype Key;
 usertype SessionKey;
 usertype TimeStamp;
+usertype ExpiredTimeStamp;
 secret k: Function;
 usertype PseudoFunction;
 const dec: PseudoFunction;
@@ -27,7 +28,7 @@ protocol denningSaccoLoweSessionKeyCompromise(C)
     role C {
         const Ni,Nr: Nonce;
         const Kir: SessionKey;
-        const T: TimeStamp;
+        const T: ExpiredTimeStamp;
         var I,R,S: Agent;
 
         read_C1(C,C,    I,R,S);

spdl/SPORE/denning-sacco.spdl

@@ -11,6 +11,7 @@
 usertype Key;
 usertype SessionKey;
 usertype TimeStamp;
+usertype ExpiredTimeStamp;
 secret k: Function;
 const Fresh: Function;
 const Compromised: Function;
@@ -22,7 +23,7 @@ protocol denningSaccoSessionKeyCompromise(C)
     role C {
         const Ni,Nr: Nonce;
         const Kir: SessionKey;
-        const T: TimeStamp;
+        const T: ExpiredTimeStamp;
         var I,R,S: Agent;
 
         read_C1(C,C,    I,R,S);

spdl/SPORE/kaochow-v3.spdl

@@ -9,7 +9,8 @@
 #
 
 usertype SessionKey;
-usertype Timestamp;
+usertype ExpiredTimeStamp;
+usertype TimeStamp;
 secret k: Function;
 const Fresh: Function;
 const Compromised: Function;
@@ -21,7 +22,7 @@ protocol kaochow3SessionKeyCompromise(C)
     role C {
         const Ni,Nr: Nonce;
         const Kir,Kt: SessionKey;
-        const T2: Timestamp;
+        const T2: ExpiredTimeStamp;
         var I,R,S: Agent;
 
         read_C1(C,C,    I,R,S);
@@ -65,7 +66,7 @@ protocol kaochow3(I,R,S)
         const nr: Nonce;
         var kir,kt: SessionKey;
         var T: Ticket;
-        const tr: Timestamp;
+        const tr: TimeStamp;
 
         read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S)  ); 
         send_3 (R,I, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) );

spdl/SPORE/ksl-lowe.spdl

@@ -11,7 +11,8 @@
 # According to SPORE there are no attacks on this protocol, scyther
 # finds one however. This has to be investigated further.
 
-usertype Server, SessionKey, GeneralizedTimestamp, TicketKey;
+usertype Server, SessionKey, TimeStamp, TicketKey;
+usertype ExpiredTimeStamp;
 secret k: Function;
 
 const a, b, e: Agent;
@@ -33,7 +34,7 @@ protocol kslLoweSessionKeyCompromise(C)
         const Ni,Nr,Nc,Ma,Mb: Nonce;
         const Kir: SessionKey;
         const Kbb: TicketKey;
-        const Tr: GeneralizedTimestamp;
+        const Tr: ExpiredTimeStamp;
         var I,R,S: Agent;
 
         read_C1(C,C,    I,R,S);
@@ -82,7 +83,7 @@ protocol kslLowe(A,B,S)
         const Nb,Nc,Mb: Nonce;
         var Kab: SessionKey;
         const Kbb: TicketKey;
-        const Tb: GeneralizedTimestamp;
+        const Tb: TimeStamp;
         var T: Ticket;
         
         read_1(A,B, Na, A);

spdl/SPORE/ksl.spdl

@@ -9,7 +9,8 @@
 #
 
 
-usertype Server, SessionKey, GeneralizedTimestamp, TicketKey;
+usertype Server, SessionKey, TimeStamp, TicketKey;
+usertype ExpiredTimeStamp;
 secret k: Function;
 
 const a, b, e: Agent;
@@ -30,7 +31,7 @@ protocol kslSessionKeyCompromise(C)
         const Ni,Nr,Nc,Ma,Mb: Nonce;
         const Kir: SessionKey;
         const Kbb: TicketKey;
-        const Tr: GeneralizedTimestamp;
+        const Tr: ExpiredTimeStamp;
         var I,R,S: Agent;
 
         read_C1(C,C,    I,R,S);
@@ -80,7 +81,7 @@ protocol ksl(A,B,S)
         const Nb,Nc,Mb: Nonce;
         var Kab: SessionKey;
         const Kbb: TicketKey;
-        const Tb: GeneralizedTimestamp;
+        const Tb: TimeStamp;
         var T: Ticket;
         
         read_1(A,B, Na, A);

spdl/SPORE/neumannstub-hwang.spdl

@@ -13,6 +13,7 @@
 
 
 usertype Server, SessionKey, TimeStamp, TicketKey;
+usertype ExpiredTimeStamp;
 secret k: Function;
 
 const a, b, e: Agent;
@@ -32,7 +33,7 @@ protocol neustubHwangSessionKeyCompromise(C)
     role C {
         const Ni,Nr,Mi,Mr: Nonce;
         const Kir: SessionKey;
-        const Tr: TimeStamp;
+        const Tr: ExpiredTimeStamp;
         var I,R,S: Agent;
 
         read_C1(C,C,    I,R,S);

spdl/SPORE/neumannstub.spdl

@@ -12,8 +12,8 @@
 # different protocols (the key establishment protocol and the repeated
 # authentication protocol)
 
-
 usertype Server, SessionKey, TimeStamp, TicketKey;
+usertype ExpiredTimeStamp;
 secret k: Function;
 
 const Alice, Bob, Simon, Eve: Agent;
@@ -32,7 +32,7 @@ protocol neustubSessionKeyCompromise(C)
     role C {
         const Ni,Nr,Mi,Mr: Nonce;
         const Kir: SessionKey;
-        const Tr: TimeStamp;
+        const Tr: ExpiredTimeStamp;
         var I,R,S: Agent;
 
         read_C1(C,C,    I,R,S);
@@ -50,7 +50,7 @@ protocol neustubSessionKeyCompromise(C)
     }
 }
 
-protocol neustubRepeat(I,R,S)
+protocol @neustubRepeat(I,R,S)
 {
     const Kir: SessionKey;
 

spdl/SPORE/wmf-lowe.spdl

@@ -11,6 +11,7 @@
 
 usertype SessionKey;
 usertype TimeStamp;
+usertype ExpiredTimeStamp;
 const succ,pred: Function;
 inversekeys (succ,pred);
 const Fresh: Function;
@@ -25,7 +26,7 @@ protocol wmfLoweSessionKeyCompromise(C)
     role C {
         const Ni,Nr: Nonce;
         const Kir: SessionKey;
-        const Ti,Ts: TimeStamp;
+        const Ti,Ts: ExpiredTimeStamp;
         var I,R,S: Agent;
 
         read_C1(C,C,    I,R,S);