Commit 6c9d716c authored by bamoon's avatar bamoon

refactored to new variable names for clarity, added second message to get...

refactored to new variable names for clarity, added second message to get results, and added roles to start handling keychain.
parent 9f3371da
......@@ -2,21 +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)))
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment