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

cpsa/tesla.scm

+(herald "TESLA Broadcast Authentication Protocol")
+
+(defprotocol tesla basic
+  (defrole bcast
+    (vars (mj text) (ki-d ki kmac-i skey) (x id data))
+    (trace
+     (send mj (enc mj kmac-i) ki-d)))
+  (comment "this should be the Mj|MAC(k'i, Mj)|ki-d message")
+  (defrole recv
+    (vars (mj text) (ki-d ki kmac-i skey) (x id data))
+    (trace
+     (recv mj (enc mj kmac-i) ki-d))))
+
+(defskeleton tesla
+  (vars (mj text) (ki-d ki kmac-i skey))
+  (defstrand bcast 1 (mj mj) (ki-d ki-d) (ki ki) (kmac-i kmac-i))
+  (comment "TODO: add constraints")
+      
+(defskeleton tesla
+  (vars (ki-d ki kmac-i skey))
+  (defstrand recv 1 (ki-d ki-d) (ki ki) (kmac-i kmac-i))
+  (comment "TODO: add constraints")