cpsa-4.4.4: tst/kerberos-variant-guar.scm

(defprotocol kerberos-variant basic
  (defrole init
    (vars (a name) (b name) (ks name) (t n text) (t-prime text) (l text) (a-ks-lt k skey)
	  (ticket mesg))
    (trace
     (send (cat a b ks))
     (recv
      (cat (enc (cat t l k a b ks) a-ks-lt)
	   ticket))
     (send (cat (enc (cat a t n) k) ticket))
     (recv (enc n t-prime k))))
  (defrole resp
    (vars (a name) (b name) (ks name) (t n text) (t-prime text) (l text) (b-ks-lt k skey))
    (trace (recv (cat (enc (cat a t n) k) (enc (cat "ticket" t l k a b ks) b-ks-lt)))
      (send (enc n t-prime k))))
  (defrole keyserver
    (vars (a name) (b name) (ks name) (t text) (l text) (a-ks-lt b-ks-lt k skey))
    (trace
     (recv (cat a b ks))
     (guar (and (fact long-term a ks a-ks-lt)
		(fact long-term b ks b-ks-lt)))
     (send
      (cat (enc (cat t l k a b ks) a-ks-lt)
           (enc (cat "ticket" t l k a b ks) b-ks-lt))))
    (uniq-orig k))

  (defrule long-term-key-non
    (forall
     ((p ks name) (k-lt skey))
     (implies (fact long-term p ks k-lt)
	      (non k-lt)))))


(defskeleton kerberos-variant
  (vars (a name) (b name) (ks name) (t n text) (a-ks-lt b-ks-lt skey))
  (defstrand init 4 (a a) (b b) (ks ks) (n n) (a-ks-lt a-ks-lt)) 
  (non-orig a-ks-lt)
  (uniq-orig n))

(defskeleton kerberos-variant
  (vars (a name) (b name) (ks name) (b-ks-lt skey))
  (defstrand resp 2 (a a) (b b) (ks ks) (b-ks-lt b-ks-lt))
  (non-orig b-ks-lt))

(defskeleton kerberos-variant
  (vars (a name) (b name) (ks name) (a-ks-lt b-ks-lt skey))
  (defstrand keyserver 2 (a a) (b b) (ks ks)(a-ks-lt a-ks-lt) (b-ks-lt b-ks-lt))
  (non-orig a-ks-lt b-ks-lt))