Refined protocol spec for checking if key is safe, began intruder spec

maude/examples/tesla-kayla.psl

 spec TESLA is
 Theory
-  types Name Nat Zero One NonZero Bool True False Key KeyMac Mac.
+  types Name Nat Zero One NonZero Bool True False Key Mac.
   subtypes NonZero Zero Key < Nat .
   subtypes One < NonZero .
   subtypes True False < Bool .
 
   ops T0 ZERO : -> Zero .
   op ONE : -> One .
-  ops TS TR : -> Nat .
+  ops TS TR : -> Nat .     // Initial time at source and receiver respectively
   op TRUE : -> True .
   op FALSE : -> False .
-
+  
+  // Sender setup 
+  op DELAY : -> Nat .	   // Disclosure delay		
+  op KEY_COMMIT : -> Key . // Key commitment to the key chain
+  op T_START : -> Nat .    // Time of sender at the starting interval
+  op START : -> Nat .      // Starting interval of the 
+  op DUR : -> Nat .		   // Duration of an interval
+  op N : -> Nat .		   // Length of key chain
+  op T_RCV : -> Nat .      // Time of receiver at setup
+ 
   op _+_ : Nat Nat -> Nat [assoc comm id: ZERO] .
   op _-_ : Nat Nat -> Nat .
   op _*_ : Nat Nat -> Nat [assoc comm id: ONE] .
+  op _^_ : Key Nat -> Key .
+  op _;_ : Msg Msg -> Msg [gather (e E)].		// Message concatenation
   op leq : Nat Nat -> Bool [assoc] .
   op equals : Nat Nat -> Bool [assoc comm] .
   op geq : Nat Nat -> Bool [assoc] .
-
-  op Tfinal : Nat -> NonZero .
-  op TInit : Nat -> Nat .
-
-  // operations for sender setup
-  op DUR : -> NonZero . 		// Duration of interval
-  op LEN : -> NonZero . 		// Length of interval
-  op START : -> Nat . 			// Start time interval
-  op DELAY : -> Nat .			// Delay
-  op KEY_COMMIT : -> Key .		// Key commitment
-  
-  // operations for key chain
-  op f : Nat -> Key .
-  op g : Key -> KeyMac .
-
+  op intSrc : Nat -> Nat    // An operator that takes a time interval and returns a time interval
+  op f : Nat -> Key .       // f is a mapping from time intervals to keys
+  op g : Key -> Nat .       // g is a mapping from key to time intervals
   op mac : Key Msg -> Mac .
-  //op mac : KeyMac Msg -> Mac .
-  op _^_ : Key Nat -> Key .
-  op _;_ : Msg Msg -> Msg [gather (e E)].		// Message concatenation
-  
-  // variables for time
-  var u : NonZero .
-  vars w x y z : Nat .
-  var v : Nat .
-  vars tsrc trcv : Nat .
-  var m : Msg .
 
-  //equations about time
-  eq Tfinal(x) = +(T0,*(x,DUR)) .
-  eq TInit(u) = +(-(*(u,DUR),DUR)) .
-  eq TInit(ZERO) = T0 .
+  op curInt : Key Bool Nat -> Nat . // Gets the current interval from a disclosed key
+  op safeKey : Key -> Key .		    // Returns the disclosed key f(i - DELAY) if the f(i) is still secret
+  op curRcvTime : Nat -> Nat .		// Gets the receiver's current time
+    
+  vars x y z w i : Nat .
+
+  //Additional properties of operators
   eq -(x,ZERO) = x .
   eq equals(y,y) = TRUE .
   eq equals(y,z) = FALSE .
   eq leq(y,z) = equals(y,+(z,v)) .
   eq geq(y,z) = leq(z,y) .
   eq leq(ZERO,x) = TRUE .
-  eq leq(x,LEN) = TRUE .
-  eq leq(tsrc,+(trcv, -(TR,TS))) = TRUE .
-  eq geq(tsrc,+(TS, DELAY)) = FALSE .
-  
-  // question - should we show that the key disclosure delay must be longer 
-  // than the network propogation delay? (TR - TS)
 
-  //equations about key commitment
-  var c : Nat . // interval of the key commitment
-  eq geq(c, ZERO) = TRUE .
-  eq geq(c, START - DELAY) = FALSE .
-  eq KEY_COMMIT = f(c) .
-  
+  // key disclosure delay must be longer than the network propogation delay: (TR - TS)
+  eq leq(DELAY,-(TR,TS)) = FALSE .
+
+  //The time interval at source must be less than time interval at the receiver
+  eq geq(intSrc(i),+(i,DELAY)) = FALSE .
+
   //equations about key chain
-  eq leq(x,c) = FALSE .
-  eq geq(x,w) = FALSE . 
-  eq leq(w,N) = TRUE . 
-  eq f(x) = ^(f(w), -(w, x)) .
-  //eq g(x) = g(f(x)) .
+  eq geq(x,w) = FALSE .
+  eq geq(x, START - DELAY) = TRUE .		// START - DELAY < x
+  eq f(x) = ^(f(w), -(w, x)) .		    // Checks that the f(w) is in the key chain
+  eq KEY_COMMIT = f(START - DELAY) .
   
+  var k : Key .
+  var diff : Nat .  
+ 
+  // Checks that the key corresponding to current time interval is still secret 
+  eq curInt(k, TRUE, diff) = diff + START .
+  eq curInt(k, FALSE, diff) = curInt(KEY_COMMIT, f(k), equals(KEY_COMMIT, f(k)), diff + ONE) .
+  eq geq(+(T_START, *(i, DUR)), +(curInt(k, TRUE, diff), *(DELAY, DUR))) = FALSE .  
+  eq safeKey(k) = f(curInt(k, FALSE, ZERO) - DELAY) .  
+
 Protocol
   vars SName RName S1Name R1Name : Name .
-  // var i : Nat . i should be TS, i.e. the interval when the sender sends the packet
-  var m1 m2 : Msg .
-  var k1 k2 k3 : Key .
-  
+  var i : Nat .
+  vars m m1 m2 : Msg .
+  vars k1 k2 k3 : Key .
+  vars mac1 mac2 : Mac .
+
   roles Sender Receiver .
 
   In(Sender) = SName .
   In(Receiver) = RName .
 
-  // Sender sends packet in interval (or TS)
-  // Receiver uses f(TS - DELAY) to determine TS - how ?
-  // Receiver checks that tsrc < TS + DELAY (since DELAY > trcv - TR)
-  
-  1. Sender -> Receiver : SName ; R1Name ; m1 ; mac(f(TS), m1) ; f(TS - DELAY)
-					    |- S1Name ; RName ; m1 ; mac(k2, m1) ; k1 .
-	
-  // Receiver receives disclosed key f(TS) 
-  // Receiver checks that f(TS) is the latest key received to date
-  // Receiver checks that f(TS) is a legitimate key in the key chain
-  // Receiver verifies that mac(k2, m1) = mac(f(TS), m1)
+  // Sender sends packet in interval i
+  // Sender dicloses key f(i-DELAY)
+  // Receiver checks if f(i) is safe (still secret) by getting the current interval i from k1
+  // and ensuring the sender's current time (T_START + i * DUR) < i + (DELAY * DUR)
+  1. Sender -> Receiver : SName ; R1Name ; m1 ; mac(f(i), m1) ; f(i - DELAY)
+					   |- S1Name ; RName ; m1 ; mac(k2, m) ; safeKey(k1) .
+
+  // Sender sends packet in interval i+DELAY
+  // Sender dicloses key f(i)
+  // Receiver checks that the key is part of the key chain
+  // Receiver uses verifies that packet is safe
+  2. Sender -> Receiver : SName ; R1Name ; m2 ; mac(f(i + DELAY), m2) ; f(i)
+						|- S1Name ; RName ; m2 ; mac2 ; safeKey(k2) .
   
-  2. Sender -> Receiver : SName ; R1Name ; m2 ; mac(f(TS + DELAY), m2) ; f(TS)
-						|- S1Name ; RName ; m2 ; mac(k3, m2) ; k2 .
-						
   Out(Sender) = SName .
-  Out(Receiver) = RName, m1 .
+  //Receiver uses k2 to authenticate message m1
+  Out(Receiver) = RName, i, m1, mac(f(i), m1)) .
+
+Intruder  
+  var K : Key . 
+  vars M1 M2 : Msg .
+  
+  K, M1    => mac(K, M1) .
+  M1 ; M2 <=> M1, M2 .
+  
+Attack 
+  0.
+		B executes protocol . 
+		Subst(B) = S1Name |-> s, RName |-> r
\ No newline at end of file