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