cpsa-4.4.1: coq/Examples/invk.scm
(herald invk)
(defprotocol invk basic
(defrole rho
(vars (ch chan) (a name) (k akey))
(trace
(recv ch (cat a (invk k)))
(send ch (enc a k)))
(inputs ch k)))
(herald invk)
(defprotocol invk basic
(defrole rho
(vars (ch chan) (a name) (k akey))
(trace
(recv ch (cat a (invk k)))
(send ch (enc a k)))
(inputs ch k)))