packages feed

cpsa-4.4.1: coq/Examples/ltk.scm

(herald ltk)

(defprotocol ltk basic
  (defrole rho
    (vars (ch chan) (a b name) (k akey))
    (trace
     (recv ch (enc a b (ltk a b) k))
     (send ch (enc a b (ltk a b))))
    (inputs ch (invk k))))