tesls protocol refinement for maude-npa

maude/examples/tesla.psl

 spec TESLA is
 Theory
-  types Name Nat Zero One NonZero Bool True False Key KeyMAC .
+  types Name Nat Zero One NonZero Bool True False Key Mac.
   subtypes NonZero Zero Key < Nat .
   subtypes One < NonZero .
   subtypes True False < Bool .
 
-  ops D N : -> NonZero .
   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 .
+  op DELAY : -> Nat .			// Delay
 
   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 not : Bool -> Bool .
-  op and : Bool Bool -> Bool [assoc comm] .
-
-  op Tfinal : Nat -> NonZero .
-  op TInit : Nat -> Nat .
+  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 START : -> Nat . 			// Start time interval
-  op DELAY : -> NonZero .			// Delay
-  op KEY_COMMIT_INT : -> Nat .
-  op f : Nat -> Key .
-  op mac : Key Msg -> Msg .
-  op g : Key -> KeyMAC .
-
-  op _^_ : Key Nat -> Key .
-  op _;_ : Msg Msg -> Msg [gather (e E)] .
+  vars x y z w i : Nat .
 
-  var u : NonZero .
-  vars w x y z : Nat .
-  var v : Nat .
-  vars tsrc trcv : Nat .
-
-  //equations about time
-  eq Tfinal(x) = +(T0,*(x,D)) .
-  eq TInit(u) = +(-(*(u,D),D)) .
-  eq TInit(ZERO) = T0 .
+  //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,N) = TRUE .
-  eq leq(tsrc,+(trcv, -(TR,TS))) = TRUE .
-  eq geq(KEY_COMMIT_INT,-(START,DELAY)) = FALSE .
-  eq not(TRUE) = FALSE .
-  eq not(FALSE) = TRUE .
-  eq and(TRUE,TRUE) = TRUE .
-  eq and(TRUE,FALSE) = FALSE .
-  eq and(FALSE,TRUE) = FALSE .
-  eq and(FALSE,FALSE) = FALSE .
+
+  // 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 geq(x,w) = FALSE .
-  eq leq(w,N) = TRUE .
   eq f(x) = ^(f(w), -(w, x)) .
 
-
 Protocol
   vars SName RName S1Name R1Name : Name .
-  vars i x j : Nat .
-  var k : Key .
-  vars m m1 : Msg .
+  var i : Nat .
+  var m1 m2 : Msg .
+  var k1 k2 k3 : Key .
+
   roles Sender Receiver .
 
+  In(Sender) = SName .
   In(Receiver) = RName .
-  In(Sender) = SName, RName .
 
-  1 . Sender -> Receiver : SName  ; R1Name ; m ; mac(f(i),m); f(i-DELAY)
-            |- S1Name ; RName ; m ; m1; k .
+  // Sender sends packet in interval i
+  // Sender dicloses key f(i-DELAY)
+  // Receiver used operator g to compute interval i from key k1
+  // Receiver uses eq geq(intSrc(i),+(i,DELAY)) = FALSE to verify that packet is safe
+
+  1. Sender -> Receiver : SName ; R1Name ; m1 ; mac(f(i), m1) ; f(i - DELAY)
+					    |- S1Name ; RName ; m1 ; intSrc(g(k1)) ; mac(k2, m1) ; k1 .
+
+  // Sender sends packet in interval i+DELAY
+  // Sender dicloses key f(i)
+  // Receiver used operator g to compute interval i+DELAY from Key k2
+  // Receiver uses verifies that packet is safe
+
+  2. Sender -> Receiver : SName ; R1Name ; m2 ; mac(f(i + DELAY), m2) ; f(i)
+						|- S1Name ; RName ; m2 ; intSrc(g(k2)) ; mac(k3, m2) ; k2 .
 
-  Out(Sender) = SName, RName .
-  Out(Receiver) = i, and(TRUE,not(geq(x,+(i,DELAY)))),
-                  and(TRUE,not(geq(i,j))),
-                  and(TRUE,equals(k,f(i-DELAY))),
-                  and(TRUE,not(geq(v,i))),
-                  and(TRUE,equals(f(v),^(f(i), -(i, v)))) .
+  Out(Sender) = SName .
+  //Receiver uses k2 to authenticate message m1
+  Out(Receiver) = RName, mac(k2, m1) , k2 .