cpsa-4.4.4: tst/example.scm

(herald example)

(defprotocol version-1 basic
  (defrole init ;; I'm B 
    (vars (a b name) (m text) (s skey))
    (trace
     (send (enc s (ltk a b)))
     (recv (enc m a s))))

  (defrole resp ;; I'm A 
    (vars (a b name) (m text) (s skey))
    (trace
     (recv (enc s (ltk a b)))
     (send (enc m a s)))))


(defskeleton version-1
  (vars (a b name) (m text) (s skey))
  (defstrand init 2 (a a) (b b) (m m) (s s))
  (non-orig (ltk a b))
  (uniq-orig s))

(defskeleton version-1
  (vars (a b name) (m text) (s skey))
  (defstrand resp 2 (a a) (b b) (m m) (s s))
  (non-orig (ltk a b))
  ;;  (uniq-orig s)
  )

(defskeleton version-1
  (vars (m text) (a b name) (s skey))
  (defstrand resp 2 (m m) (a a) (b b) (s s))
  (defstrand init 1 (a a) (b b) (s s))
  (deflistener m)
  (precedes ((1 0) (0 0)))
  (uniq-orig m s)
  (non-orig (ltk a b)))



(defskeleton version-1
  (vars (m text) (a b name) (s skey))
  (defstrand resp 2 (m m) (a a) (b b) (s s))
  (defstrand init 1 (a a) (b b) (s s))
  (deflistener m)
  (precedes ((1 0) (0 0)))
  (uniq-orig m ;; s
	     )
  (non-orig (ltk a b)))

(defprotocol version-2 basic
  (defrole init ;; I'm B 
    (vars (a b name) (m n1 n2 text) (s skey))
    (trace
     (send (enc s n1 (ltk a b)))
     (recv (enc m a n1 s))))

  (defrole resp ;; I'm A 
    (vars (a b name) (m n1 n2 text) (s skey))
    (trace
     (recv (enc s n1 (ltk a b)))
     (send (enc m a n1 s)))))


(defskeleton version-2
  (vars (a b name) (m text) (s skey))
  (defstrand init 2 (a a) (b b) (m m) (s s))
  (non-orig (ltk a b))
  (uniq-orig s))

(defskeleton version-2
  (vars (a b name) (m n1 n2 text) (s skey))
  (defstrand resp 2 (a a) (b b) (m m) (s s) (n1 n1))
  (non-orig (ltk a b))
  (uniq-orig n1)
  ;;  (uniq-orig s)
  )