Commit f86f416c authored by Kayla Mesh's avatar Kayla Mesh

Merge branch 'master' of https://gitlab.cs.ksu.edu/joydeep/verifytesla

Updated tesla-kayla.psl
parents 233a9d36 6c9d716c
......@@ -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