resolved merge conflicts

cpsa/tesla.scm

@@ -2,19 +2,32 @@
 
 (defprotocol tesla basic
   (defrole bcast
-    (vars (mj text) (ki-d ki kmac-i skey) (x id data))
+    (vars (mj text) (k1 k0 kmac-1 kmac-2 skey) (x id data))
     (trace
-     (send (cat mj (enc mj kmac-i) ki-d))))
+     (send (cat mj (enc mj kmac-1) k0))
+     (send (cat mj (enc mj kmac-2) k1))))
   (defrole resp
-    (vars (mj text) (ki-d ki kmac-i skey) (x id data))
+    (vars (mj text) (k1 k0 kmac-1 kmac-2 skey) (x id data))
     (trace
-     (recv (cat mj (enc mj kmac-i) ki-d)))))
+     (recv (cat mj (enc mj kmac-1) k0))
+     (recv (cat mj (enc mj kmac-2) k1))))
+  (defrole initialize
+    (vars (v data) (key0 skey))
+    (trace (init (cat v key0)))
+    (uniq-gen v)
+    (fn-of (v-id (v "v"))))
+  (defrole successor
+    (vars (v data) (key skey))
+    (trace (tran (cat v key) (cat v #(key))))
+    (lt key #(key))))
 
 (defskeleton tesla
-  (vars (mj text) (ki-d kmac-i ki skey))
-  (defstrand bcast 1 (mj mj) (ki-d ki-d) (kmac-i kmac-i) (ki ki)))
+  (vars (mj text) (k1 k0 kmac-1 kmac-2 skey))
+  (defstrand bcast 2 (mj mj) (k0 k0) (k1 k1) (kmac-1 kmac-1) (kmac-2 kmac-2))
+  (non-orig (privk ki-d) (privk ki) (privk mac-i)))
 
 
 (defskeleton tesla
   (vars (mj text) (ki-d ki kmac-i skey))
-  (defstrand resp 1 (mj mj) (ki-d ki-d) (kmac-i kmac-i) (ki ki)))
+  (defstrand resp 2 (mj mj) (k0 k0) (k1 k1) (kmac-1 kmac-1) (kmac-2 kmac-2))
+  (non-orig (privk ki-d) (privk ki) (privk mac-i)))

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 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 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 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
 
-  op mac : Key Msg -> Mac .
-  //op mac : KeyMac Msg -> Mac .
-  op _^_ : Key Nat -> Key .
-  op _;_ : Msg Msg -> Msg [gather (e E)].		// Message concatenation
+  vars x y z w i : Nat .
 
-  // 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 .
+  //Additional properties of operators
   eq -(x,ZERO) = x .
   eq equals(y,y) = TRUE .
   eq equals(y,z) = FALSE .