start modeling the protocol

maude/examples/tesla.psl

 spec TESLA is
 Theory
-  types Nat Zero One NonZero Bool True False Key KeyMAC.
+  types Name Nat Zero One NonZero Bool True False Key KeyMAC Enc .
+  type SecretKey .
   subtypes NonZero Zero Key < Nat .
   subtypes One < NonZero .
   subtypes True False < Bool .
@@ -12,6 +13,9 @@ Theory
   op TRUE : -> True .
   op FALSE : -> False .
 
+  op enc : SecretKey Msg -> Enc .
+  op dec : SecretKey Enc -> Msg .
+
   op _+_ : Nat Nat -> Nat [assoc comm id: ZERO] .
   op _-_ : Nat Nat -> Nat .
   op _*_ : Nat Nat -> Nat [assoc comm id: ONE] .
@@ -22,17 +26,29 @@ Theory
   op Tfinal : Nat -> NonZero .
   op TInit : Nat -> Nat .
 
+  op START : -> Nat . 			// Start time interval
+  op DELAY : -> Nat .			// Delay
+  op f : Nat -> Key .
+  op g : Key -> KeyMAC .
+
+  op _^_ : Key Nat -> Key .
+  op _;_ : Msg Msg -> Msg .
   var u : NonZero .
-  vars x y z : Nat .
+  vars w x y z : Nat .
   var v : Nat .
   vars tsrc trcv : Nat .
+  var m : Msg .
+  var sec : SecretKey .
+
+  //equation about symmetric encryption
+  eq dec(sec,enc(sec,m)) = m
 
+  //equations about time
   eq Tfinal(x) = +(T0,*(x,D)) .
   eq TInit(u) = +(-(*(u,D),D)) .
   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) .
@@ -40,19 +56,26 @@ Theory
   eq leq(x,N) = 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) . 
-  
+  //equations about key chain
+  eq geq(x,w) = FALSE .
+  eq leq(w,N) = TRUE .
+  eq f(x) = ^(f(w), -(w, x)) .
+
+  //eq f(START - DELAY) =  ^(f(x), -(+(i,DELAY),START) . //Think about this later
+
+Protocol
+  vars SName RName S1Name R1Name : Name .
+  var i : Nat .
+  var sk : SecretKey
+  var em : Enc .
+  roles Sender Receiver .
+
+  In(Receiver) = RName sk .
+  In(Sender) = SName, RName, sk .
+
+  Def(Sender) = sched1 := D ; START ; TInit(START) ; N ,
+                sched2 := DELAY ,
+                sched3 := f(i) .
 
-  
\ No newline at end of file
+  1 . Sender -> Receiver : SName ; RName ; enc(sk, sched1 ; sched2 ; sched3) |- S1Name ; RNAME ; em .
+  2.  Receiver -> Sender : S1Name ; RName