Update tesla.scm

cpsa/tesla.scm

@@ -2,32 +2,37 @@
 
 (defprotocol tesla basic
   (defrole bcast
-    (vars (mj text) (k1 k0 kmac-1 kmac-2 skey) (x id data))
+    (vars (mj text) (k1 k0 kmac-1 kmac-2 skey) (v0 v1 data))
     (trace
      (send (cat mj (enc mj kmac-1) k0))
-     (send (cat mj (enc mj kmac-2) k1))))
+     (obsv (cat v0 v1))
+     (send (cat mj (enc mj kmac-2) k1)))
+     (eq k1 (key-of v1))
+     (lt k0 k1))
   (defrole resp
-    (vars (mj text) (k1 k0 kmac-1 kmac-2 skey) (x id data))
+    (vars (mj text) (k1 k0 kmac-1 kmac-2 skey) (v data))
     (trace
      (recv (cat mj (enc mj kmac-1) k0))
-     (recv (cat mj (enc mj kmac-2) k1))))
+     (obsv (cat v0 v1))
+     (recv (cat mj (enc mj kmac-2) k1))
+     (eq k1 (key-of v1))
+     (lt k0 k1)))
   (defrole initialize
-    (vars (v data) (key0 skey))
-    (trace (init (cat v key0)))
+    (vars (v v0 data) (key0 skey))
+    (trace (init (cat v v0)))
     (uniq-gen v)
-    (fn-of (v-id (v "v"))))
+    (fn-of (key-of (v0 key0))))
   (defrole successor
-    (vars (v data) (key skey))
-    (trace (tran (cat v key) (cat v #(key))))
-    (lt key #(key))))
+    (vars (v v0 data) (key0 key skey))
+    (trace (tran (cat v v0) (cat v v0 (hash v0))))
+    (fn-of (key-of (v0 key0) ((hash v0) key)))
+    (lt key0 key1)))
 
 (defskeleton tesla
   (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)))
+  (defstrand bcast 2 (mj mj) (k0 k0) (k1 k1) (kmac-1 kmac-1) (kmac-2 kmac-2)))
 
 
 (defskeleton tesla
-  (vars (mj text) (ki-d ki kmac-i skey))
-  (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)))
+  (vars (mj text) (k1 k0 kmac-1 kmac-2 skey))
+  (defstrand resp 2 (mj mj) (k0 k0) (k1 k1) (kmac-1 kmac-1) (kmac-2 kmac-2)))