Began specifying the key chain

maude/examples/tesla.psl

 spec TESLA is
 Theory
-  types Nat Zero One NonZero Bool True False .
+  types Nat Zero One NonZero Bool True False Key KeyMAC.
   subtypes NonZero Zero Key < Nat .
   subtypes One < NonZero .
   subtypes True False < Bool .
@@ -32,9 +32,27 @@ Theory
   eq TInit(ZERO) = T0 .
   eq -(x,ZERO) = x .
   eq equals(y,y) = TRUE .
+  eq equals(z,z) = TRUE . // Do we need this ?
   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,N) = TRUE .
-  eq leq(tsrc,+(trcv + -(TR,TS))) = TRUE
+  eq leq(tsrc,+(trcv, -(TR,TS))) = TRUE .
+
+  // Sender setup 
+  op key_commit : -> Key .
+  op s : -> Nat . 			// Start time interval
+  op d : -> Nat .			// Delay
+  op f : Nat -> Key .
+  op g : Key -> KeyMAC . 
+  
+  op _^_ : Key Nat -> Key .
+  op _;_ : Msg Msg -> Msg .
+  
+  eq key_commit = f(s - d) .
+  eq f(x) = ^(f(N), -(N, x)) .
+  eq f(s - d) =  ^(f(x), -(+(i,d),s) . 
+  
+
+  
\ No newline at end of file