cpsa-4.4.4: tst/dh-ca_hack-uniq_cert.tst

(herald dhca (algebra basic) (bound 12))

(comment "CPSA 4.4.4")
(comment "All input read from tst/dh-ca_hack-uniq_cert.scm")

(defprotocol dhca basic
  (defrole init
    (vars (gx h akey) (dhkey skey) (a b ca name) (n text))
    (trace (recv (enc gx a (privk ca)))
      (send (cat gx (enc gx a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))
      (send (enc "check" n (enc "dh" gx h dhkey))))
    (non-orig dhkey (privk ca)))
  (defrole resp
    (vars (gy h akey) (dhkey skey) (a b ca name) (n text))
    (trace (recv (enc gy b (privk ca)))
      (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey))))
    (non-orig dhkey (privk ca)))
  (defrole ca
    (vars (subject ca name) (gz akey))
    (trace (send (enc gz subject (privk ca))))
    (non-orig (invk gz))
    (uniq-orig gz))
  (defrole CDHcalc1
    (vars (gx gy akey) (dhkey skey))
    (trace (recv (cat gx (invk gy))) (send (enc "dh" gx gy dhkey))))
  (defrole CDHcalc2
    (vars (gx gy akey) (dhkey skey))
    (trace (recv (cat gy (invk gx))) (send (enc "dh" gx gy dhkey))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx h akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b)
    (ca ca))
  (non-orig dhkey (privk ca))
  (comment
    "Full initiator point-of-view.  No need to make extra assumptions.")
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))
      (send (enc "check" n (enc "dh" gx h dhkey)))))
  (label 0)
  (unrealized (0 0) (0 2))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx h akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (precedes ((1 0) (0 0)))
  (non-orig dhkey (invk gx) (privk ca))
  (uniq-orig gx)
  (operation encryption-test (added-strand ca 1) (enc gx a (privk ca))
    (0 0))
  (strand-map 0)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))
      (send (enc "check" n (enc "dh" gx h dhkey))))
    ((send (enc gx a (privk ca)))))
  (label 1)
  (parent 0)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (precedes ((1 0) (0 0)))
  (non-orig dhkey (invk gx) (privk ca))
  (uniq-orig gx)
  (operation encryption-test (displaced 2 1 ca 1) (enc h b (privk ca))
    (0 2))
  (strand-map 0 1)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx a (privk ca)))))
  (label 2)
  (parent 1)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx h akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand ca 1 (gz h) (subject b) (ca ca))
  (precedes ((1 0) (0 0)) ((2 0) (0 2)))
  (non-orig dhkey (invk gx) (invk h) (privk ca))
  (uniq-orig gx h)
  (operation encryption-test (added-strand ca 1) (enc h b (privk ca))
    (0 2))
  (strand-map 0 1)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))
      (send (enc "check" n (enc "dh" gx h dhkey))))
    ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca)))))
  (label 3)
  (parent 1)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a ca a-0 b ca-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a-0) (b b)
    (ca ca-0))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)))
  (non-orig dhkey (invk gx) (privk ca) (privk ca-0))
  (uniq-orig gx)
  (operation encryption-test (added-strand resp 3)
    (enc n (enc "dh" gx gx dhkey)) (0 2))
  (strand-map 0 1)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx a (privk ca))))
    ((recv (enc gx b (privk ca-0)))
      (recv (cat gx (enc gx a-0 (privk ca-0))))
      (send
        (cat gx (enc gx b (privk ca-0))
          (enc n (enc "dh" gx gx dhkey))))))
  (label 4)
  (parent 2)
  (unrealized (2 0) (2 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (deflistener (enc "dh" gx gx dhkey))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 2)))
  (non-orig dhkey (invk gx) (privk ca))
  (uniq-orig gx)
  (operation encryption-test (added-listener (enc "dh" gx gx dhkey))
    (enc n (enc "dh" gx gx dhkey)) (0 2))
  (strand-map 0 1)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx a (privk ca))))
    ((recv (enc "dh" gx gx dhkey)) (send (enc "dh" gx gx dhkey))))
  (label 5)
  (parent 2)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx h akey) (a b ca a-0 b-0 ca-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand ca 1 (gz h) (subject b) (ca ca))
  (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h gx) (a a-0) (b b-0)
    (ca ca-0))
  (precedes ((1 0) (0 0)) ((1 0) (3 1)) ((2 0) (3 0)) ((3 2) (0 2)))
  (non-orig dhkey (invk gx) (invk h) (privk ca) (privk ca-0))
  (uniq-orig gx h)
  (operation encryption-test (added-strand resp 3)
    (enc n (enc "dh" gx h dhkey)) (0 2))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))
      (send (enc "check" n (enc "dh" gx h dhkey))))
    ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca))))
    ((recv (enc h b-0 (privk ca-0)))
      (recv (cat gx (enc gx a-0 (privk ca-0))))
      (send
        (cat h (enc h b-0 (privk ca-0))
          (enc n (enc "dh" gx h dhkey))))))
  (label 6)
  (parent 3)
  (unrealized (3 0) (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx h akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand ca 1 (gz h) (subject b) (ca ca))
  (deflistener (enc "dh" gx h dhkey))
  (precedes ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (3 0)) ((3 1) (0 2)))
  (non-orig dhkey (invk gx) (invk h) (privk ca))
  (uniq-orig gx h)
  (operation encryption-test (added-listener (enc "dh" gx h dhkey))
    (enc n (enc "dh" gx h dhkey)) (0 2))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))
      (send (enc "check" n (enc "dh" gx h dhkey))))
    ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca))))
    ((recv (enc "dh" gx h dhkey)) (send (enc "dh" gx h dhkey))))
  (label 7)
  (parent 3)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a ca a-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a-0) (b a)
    (ca ca))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)))
  (non-orig dhkey (invk gx) (privk ca))
  (uniq-orig gx)
  (operation encryption-test (displaced 3 1 ca 1)
    (enc gx b (privk ca-0)) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx a (privk ca))))
    ((recv (enc gx a (privk ca)))
      (recv (cat gx (enc gx a-0 (privk ca))))
      (send
        (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey))))))
  (label 8)
  (parent 4)
  (unrealized (2 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx h akey) (a b ca a-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand ca 1 (gz h) (subject b) (ca ca))
  (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h gx) (a a-0) (b b)
    (ca ca))
  (precedes ((1 0) (0 0)) ((1 0) (3 1)) ((2 0) (3 0)) ((3 2) (0 2)))
  (non-orig dhkey (invk gx) (invk h) (privk ca))
  (uniq-orig gx h)
  (operation encryption-test (displaced 4 2 ca 1)
    (enc h b-0 (privk ca-0)) (3 0))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))
      (send (enc "check" n (enc "dh" gx h dhkey))))
    ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca))))
    ((recv (enc h b (privk ca))) (recv (cat gx (enc gx a-0 (privk ca))))
      (send
        (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))))
  (label 9)
  (parent 6)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b a)
    (ca ca))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)))
  (non-orig dhkey (invk gx) (privk ca))
  (uniq-orig gx)
  (operation encryption-test (displaced 3 1 ca 1)
    (enc gx a-0 (privk ca)) (2 1))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx a (privk ca))))
    ((recv (enc gx a (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey))))))
  (label 10)
  (parent 8)
  (realized)
  (shape)
  (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b a) (ca ca) (n n))))
  (origs (gx (1 0))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx h akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand ca 1 (gz h) (subject b) (ca ca))
  (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h gx) (a a) (b b)
    (ca ca))
  (precedes ((1 0) (0 0)) ((1 0) (3 1)) ((2 0) (3 0)) ((3 2) (0 2)))
  (non-orig dhkey (invk gx) (invk h) (privk ca))
  (uniq-orig gx h)
  (operation encryption-test (displaced 4 1 ca 1)
    (enc gx a-0 (privk ca)) (3 1))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))
      (send (enc "check" n (enc "dh" gx h dhkey))))
    ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca))))
    ((recv (enc h b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))))
  (label 11)
  (parent 9)
  (realized)
  (shape)
  (maps ((0) ((gx gx) (h h) (dhkey dhkey) (a a) (b b) (ca ca) (n n))))
  (origs (gx (1 0)) (h (2 0))))

(comment "Nothing left to do")

(defprotocol dhca basic
  (defrole init
    (vars (gx h akey) (dhkey skey) (a b ca name) (n text))
    (trace (recv (enc gx a (privk ca)))
      (send (cat gx (enc gx a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))
      (send (enc "check" n (enc "dh" gx h dhkey))))
    (non-orig dhkey (privk ca)))
  (defrole resp
    (vars (gy h akey) (dhkey skey) (a b ca name) (n text))
    (trace (recv (enc gy b (privk ca)))
      (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey))))
    (non-orig dhkey (privk ca)))
  (defrole ca
    (vars (subject ca name) (gz akey))
    (trace (send (enc gz subject (privk ca))))
    (non-orig (invk gz))
    (uniq-orig gz))
  (defrole CDHcalc1
    (vars (gx gy akey) (dhkey skey))
    (trace (recv (cat gx (invk gy))) (send (enc "dh" gx gy dhkey))))
  (defrole CDHcalc2
    (vars (gx gy akey) (dhkey skey))
    (trace (recv (cat gy (invk gx))) (send (enc "dh" gx gy dhkey))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (non-orig dhkey (privk ca))
  (uniq-orig n)
  (comment "Full responder point of view with freshly chosen n")
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey)))))
  (label 12)
  (unrealized (0 0) (0 1) (0 3))
  (origs (n (0 2)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((1 0) (0 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n gy)
  (operation encryption-test (added-strand ca 1) (enc gy b (privk ca))
    (0 0))
  (strand-map 0)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey))))
    ((send (enc gy b (privk ca)))))
  (label 13)
  (parent 12)
  (unrealized (0 1) (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((1 0) (0 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n gy)
  (operation encryption-test (displaced 2 1 ca 1) (enc h a (privk ca))
    (0 1))
  (strand-map 0 1)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (recv (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy b (privk ca)))))
  (label 14)
  (parent 13)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz h) (subject a) (ca ca))
  (precedes ((1 0) (0 0)) ((2 0) (0 1)))
  (non-orig dhkey (invk gy) (invk h) (privk ca))
  (uniq-orig n gy h)
  (operation encryption-test (added-strand ca 1) (enc h a (privk ca))
    (0 1))
  (strand-map 0 1)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey))))
    ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca)))))
  (label 15)
  (parent 13)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca a b-0 ca-0 name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0)
    (ca ca-0))
  (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 3) (0 3)))
  (non-orig dhkey (invk gy) (privk ca) (privk ca-0))
  (uniq-orig n gy)
  (operation encryption-test (added-strand init 4)
    (enc "check" n (enc "dh" gy gy dhkey)) (0 3))
  (strand-map 0 1)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (recv (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy b (privk ca))))
    ((recv (enc gy a (privk ca-0)))
      (send (cat gy (enc gy a (privk ca-0))))
      (recv
        (cat gy (enc gy b-0 (privk ca-0))
          (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey)))))
  (label 16)
  (parent 14)
  (unrealized (2 0) (2 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (deflistener (enc "dh" gy gy dhkey))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 3)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n gy)
  (operation encryption-test (added-listener (enc "dh" gy gy dhkey))
    (enc "check" n (enc "dh" gy gy dhkey)) (0 3))
  (strand-map 0 1)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (recv (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy b (privk ca))))
    ((recv (enc "dh" gy gy dhkey)) (send (enc "dh" gy gy dhkey))))
  (label 17)
  (parent 14)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 b-0 ca-0 name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz h) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b-0)
    (ca ca-0))
  (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((2 0) (3 0))
    ((3 3) (0 3)))
  (non-orig dhkey (invk gy) (invk h) (privk ca) (privk ca-0))
  (uniq-orig n gy h)
  (operation encryption-test (added-strand init 4)
    (enc "check" n (enc "dh" h gy dhkey)) (0 3))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey))))
    ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca))))
    ((recv (enc h a-0 (privk ca-0)))
      (send (cat h (enc h a-0 (privk ca-0))))
      (recv
        (cat gy (enc gy b-0 (privk ca-0))
          (enc n (enc "dh" h gy dhkey))))
      (send (enc "check" n (enc "dh" h gy dhkey)))))
  (label 18)
  (parent 15)
  (unrealized (3 0) (3 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz h) (subject a) (ca ca))
  (deflistener (enc "dh" h gy dhkey))
  (precedes ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 1)) ((2 0) (3 0))
    ((3 1) (0 3)))
  (non-orig dhkey (invk gy) (invk h) (privk ca))
  (uniq-orig n gy h)
  (operation encryption-test (added-listener (enc "dh" h gy dhkey))
    (enc "check" n (enc "dh" h gy dhkey)) (0 3))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey))))
    ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca))))
    ((recv (enc "dh" h gy dhkey)) (send (enc "dh" h gy dhkey))))
  (label 19)
  (parent 15)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0)
    (ca ca))
  (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 3) (0 3)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n gy)
  (operation encryption-test (displaced 3 1 ca 1)
    (enc gy a (privk ca-0)) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (recv (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy b (privk ca))))
    ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca))))
      (recv
        (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey)))))
  (label 20)
  (parent 16)
  (unrealized (2 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca b-0 name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz h) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a) (b b-0)
    (ca ca))
  (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((2 0) (3 0))
    ((3 3) (0 3)))
  (non-orig dhkey (invk gy) (invk h) (privk ca))
  (uniq-orig n gy h)
  (operation encryption-test (displaced 4 2 ca 1)
    (enc h a-0 (privk ca-0)) (3 0))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey))))
    ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca))))
    ((recv (enc h a (privk ca))) (send (cat h (enc h a (privk ca))))
      (recv
        (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (send (enc "check" n (enc "dh" h gy dhkey)))))
  (label 21)
  (parent 18)
  (unrealized (3 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b)
    (ca ca))
  (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 3) (0 3)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n gy)
  (operation encryption-test (displaced 3 1 ca 1)
    (enc gy b-0 (privk ca)) (2 2))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (recv (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy b (privk ca))))
    ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey)))))
  (label 22)
  (parent 20)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a b) (b b) (ca ca))))
  (origs (gy (1 0)) (n (0 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz h) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a) (b b)
    (ca ca))
  (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((2 0) (3 0))
    ((3 3) (0 3)))
  (non-orig dhkey (invk gy) (invk h) (privk ca))
  (uniq-orig n gy h)
  (operation encryption-test (displaced 4 1 ca 1)
    (enc gy b-0 (privk ca)) (3 2))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey))))
    ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca))))
    ((recv (enc h a (privk ca))) (send (cat h (enc h a (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (send (enc "check" n (enc "dh" h gy dhkey)))))
  (label 23)
  (parent 21)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h h) (dhkey dhkey) (a a) (b b) (ca ca))))
  (origs (gy (1 0)) (h (2 0)) (n (0 2))))

(comment "Nothing left to do")

(defprotocol dhca basic
  (defrole init
    (vars (gx h akey) (dhkey skey) (a b ca name) (n text))
    (trace (recv (enc gx a (privk ca)))
      (send (cat gx (enc gx a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))
      (send (enc "check" n (enc "dh" gx h dhkey))))
    (non-orig dhkey (privk ca)))
  (defrole resp
    (vars (gy h akey) (dhkey skey) (a b ca name) (n text))
    (trace (recv (enc gy b (privk ca)))
      (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey))))
    (non-orig dhkey (privk ca)))
  (defrole ca
    (vars (subject ca name) (gz akey))
    (trace (send (enc gz subject (privk ca))))
    (non-orig (invk gz))
    (uniq-orig gz))
  (defrole CDHcalc1
    (vars (gx gy akey) (dhkey skey))
    (trace (recv (cat gx (invk gy))) (send (enc "dh" gx gy dhkey))))
  (defrole CDHcalc2
    (vars (gx gy akey) (dhkey skey))
    (trace (recv (cat gy (invk gx))) (send (enc "dh" gx gy dhkey))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (deflistener n)
  (non-orig dhkey (privk ca))
  (uniq-orig n)
  (comment "Full responder point of view with freshly chosen n")
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n)))
  (label 24)
  (unrealized (0 0) (0 1) (0 3) (1 0))
  (preskeleton)
  (origs (n (0 2)))
  (comment "Not a skeleton"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (deflistener n)
  (precedes ((0 2) (1 0)))
  (non-orig dhkey (privk ca))
  (uniq-orig n)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n)))
  (label 25)
  (parent 24)
  (unrealized (0 0) (0 1) (0 3) (1 0))
  (origs (n (0 2)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 b-0 ca-0 name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (deflistener n)
  (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b-0)
    (ca ca-0))
  (precedes ((0 2) (2 2)) ((2 3) (1 0)))
  (non-orig dhkey (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation nonce-test (added-strand init 4) n (1 0)
    (enc n (enc "dh" h gy dhkey)))
  (strand-map 0 1)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n))
    ((recv (enc h a-0 (privk ca-0)))
      (send (cat h (enc h a-0 (privk ca-0))))
      (recv
        (cat gy (enc gy b-0 (privk ca-0))
          (enc n (enc "dh" h gy dhkey))))
      (send (enc "check" n (enc "dh" h gy dhkey)))))
  (label 26)
  (parent 25)
  (unrealized (0 0) (0 1) (0 3) (1 0) (2 0) (2 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (deflistener n)
  (deflistener (enc "dh" h gy dhkey))
  (precedes ((0 2) (1 0)) ((2 1) (1 0)))
  (non-orig dhkey (privk ca))
  (uniq-orig n)
  (operation nonce-test (added-listener (enc "dh" h gy dhkey)) n (1 0)
    (enc n (enc "dh" h gy dhkey)))
  (strand-map 0 1)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n))
    ((recv (enc "dh" h gy dhkey)) (send (enc "dh" h gy dhkey))))
  (label 27)
  (parent 25)
  (unrealized (0 0) (0 1) (0 3) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 b-0 ca-0 name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (deflistener n)
  (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b-0)
    (ca ca-0))
  (defstrand ca 1 (gz h) (subject a-0) (ca ca-0))
  (precedes ((0 2) (2 2)) ((2 3) (1 0)) ((3 0) (0 1)) ((3 0) (2 0)))
  (non-orig dhkey (invk h) (privk ca) (privk ca-0))
  (uniq-orig n h)
  (operation encryption-test (added-strand ca 1)
    (enc h a-0 (privk ca-0)) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n))
    ((recv (enc h a-0 (privk ca-0)))
      (send (cat h (enc h a-0 (privk ca-0))))
      (recv
        (cat gy (enc gy b-0 (privk ca-0))
          (enc n (enc "dh" h gy dhkey))))
      (send (enc "check" n (enc "dh" h gy dhkey))))
    ((send (enc h a-0 (privk ca-0)))))
  (label 28)
  (parent 26)
  (unrealized (0 0) (0 1) (0 3) (1 0) (2 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (deflistener n)
  (deflistener (enc "dh" h gy dhkey))
  (defstrand CDHcalc1 2 (dhkey dhkey) (gx h) (gy gy))
  (precedes ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig dhkey (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand CDHcalc1 2)
    (enc "dh" h gy dhkey) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n))
    ((recv (enc "dh" h gy dhkey)) (send (enc "dh" h gy dhkey)))
    ((recv (cat h (invk gy))) (send (enc "dh" h gy dhkey))))
  (label 29)
  (parent 27)
  (unrealized (0 0) (0 1) (0 3))
  (dead)
  (comment "empty cohort"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (deflistener n)
  (deflistener (enc "dh" h gy dhkey))
  (defstrand CDHcalc2 2 (dhkey dhkey) (gx h) (gy gy))
  (precedes ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig dhkey (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand CDHcalc2 2)
    (enc "dh" h gy dhkey) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n))
    ((recv (enc "dh" h gy dhkey)) (send (enc "dh" h gy dhkey)))
    ((recv (cat gy (invk h))) (send (enc "dh" h gy dhkey))))
  (label 30)
  (parent 27)
  (unrealized (0 0) (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (h akey) (a b ca a-0 ca-0 name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy h) (h h) (a a) (b b)
    (ca ca))
  (deflistener n)
  (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h h) (a a-0) (b a-0)
    (ca ca-0))
  (defstrand ca 1 (gz h) (subject a-0) (ca ca-0))
  (precedes ((0 2) (2 2)) ((2 3) (1 0)) ((3 0) (0 0)) ((3 0) (2 0)))
  (non-orig dhkey (invk h) (privk ca) (privk ca-0))
  (uniq-orig n h)
  (operation encryption-test (displaced 4 3 ca 1)
    (enc gy b-0 (privk ca-0)) (2 2))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc h b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send (cat h (enc h b (privk ca)) (enc n (enc "dh" h h dhkey))))
      (recv (enc "check" n (enc "dh" h h dhkey)))) ((recv n) (send n))
    ((recv (enc h a-0 (privk ca-0)))
      (send (cat h (enc h a-0 (privk ca-0))))
      (recv
        (cat h (enc h a-0 (privk ca-0)) (enc n (enc "dh" h h dhkey))))
      (send (enc "check" n (enc "dh" h h dhkey))))
    ((send (enc h a-0 (privk ca-0)))))
  (label 31)
  (parent 28)
  (unrealized (0 0) (0 1) (0 3) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 b-0 ca-0 name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (deflistener n)
  (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b-0)
    (ca ca-0))
  (defstrand ca 1 (gz h) (subject a-0) (ca ca-0))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0))
  (precedes ((0 2) (2 2)) ((2 3) (1 0)) ((3 0) (0 1)) ((3 0) (2 0))
    ((4 0) (0 0)))
  (non-orig dhkey (invk gy) (invk h) (privk ca) (privk ca-0))
  (uniq-orig n gy h)
  (operation encryption-test (added-strand ca 1)
    (enc gy b-0 (privk ca-0)) (2 2))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n))
    ((recv (enc h a-0 (privk ca-0)))
      (send (cat h (enc h a-0 (privk ca-0))))
      (recv
        (cat gy (enc gy b-0 (privk ca-0))
          (enc n (enc "dh" h gy dhkey))))
      (send (enc "check" n (enc "dh" h gy dhkey))))
    ((send (enc h a-0 (privk ca-0))))
    ((send (enc gy b-0 (privk ca-0)))))
  (label 32)
  (parent 28)
  (unrealized (0 0) (0 1) (0 3) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (deflistener n)
  (deflistener (enc "dh" h gy dhkey))
  (defstrand CDHcalc2 2 (dhkey dhkey) (gx h) (gy gy))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 0) (0 0))
    ((4 0) (3 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n gy)
  (operation encryption-test (added-strand ca 1) (enc gy b (privk ca))
    (0 0))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n))
    ((recv (enc "dh" h gy dhkey)) (send (enc "dh" h gy dhkey)))
    ((recv (cat gy (invk h))) (send (enc "dh" h gy dhkey)))
    ((send (enc gy b (privk ca)))))
  (label 33)
  (parent 30)
  (unrealized (0 1) (0 3))
  (dead)
  (comment "empty cohort"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (h akey) (a b ca a-0 ca-0 name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy h) (h h) (a a) (b b)
    (ca ca))
  (deflistener n)
  (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h h) (a a-0) (b a-0)
    (ca ca-0))
  (defstrand ca 1 (gz h) (subject a-0) (ca ca-0))
  (deflistener (enc "dh" h h dhkey))
  (precedes ((0 2) (2 2)) ((2 3) (1 0)) ((3 0) (0 0)) ((3 0) (2 0))
    ((3 0) (4 0)) ((4 1) (1 0)))
  (non-orig dhkey (invk h) (privk ca) (privk ca-0))
  (uniq-orig n h)
  (operation nonce-test (added-listener (enc "dh" h h dhkey)) n (1 0)
    (enc n (enc "dh" h h dhkey)) (enc "check" n (enc "dh" h h dhkey)))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc h b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send (cat h (enc h b (privk ca)) (enc n (enc "dh" h h dhkey))))
      (recv (enc "check" n (enc "dh" h h dhkey)))) ((recv n) (send n))
    ((recv (enc h a-0 (privk ca-0)))
      (send (cat h (enc h a-0 (privk ca-0))))
      (recv
        (cat h (enc h a-0 (privk ca-0)) (enc n (enc "dh" h h dhkey))))
      (send (enc "check" n (enc "dh" h h dhkey))))
    ((send (enc h a-0 (privk ca-0))))
    ((recv (enc "dh" h h dhkey)) (send (enc "dh" h h dhkey))))
  (label 34)
  (parent 31)
  (unrealized (0 0) (0 1) (0 3) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 b-0 ca-0 name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b)
    (ca ca))
  (deflistener n)
  (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b-0)
    (ca ca-0))
  (defstrand ca 1 (gz h) (subject a-0) (ca ca-0))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0))
  (deflistener (enc "dh" h gy dhkey))
  (precedes ((0 2) (2 2)) ((2 3) (1 0)) ((3 0) (0 1)) ((3 0) (2 0))
    ((3 0) (5 0)) ((4 0) (0 0)) ((4 0) (5 0)) ((5 1) (1 0)))
  (non-orig dhkey (invk gy) (invk h) (privk ca) (privk ca-0))
  (uniq-orig n gy h)
  (operation nonce-test (added-listener (enc "dh" h gy dhkey)) n (1 0)
    (enc n (enc "dh" h gy dhkey)) (enc "check" n (enc "dh" h gy dhkey)))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n))
    ((recv (enc h a-0 (privk ca-0)))
      (send (cat h (enc h a-0 (privk ca-0))))
      (recv
        (cat gy (enc gy b-0 (privk ca-0))
          (enc n (enc "dh" h gy dhkey))))
      (send (enc "check" n (enc "dh" h gy dhkey))))
    ((send (enc h a-0 (privk ca-0)))) ((send (enc gy b-0 (privk ca-0))))
    ((recv (enc "dh" h gy dhkey)) (send (enc "dh" h gy dhkey))))
  (label 35)
  (parent 32)
  (unrealized (0 0) (0 1) (0 3) (5 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhca basic
  (defrole init
    (vars (gx h akey) (dhkey skey) (a b ca name) (n text))
    (trace (recv (enc gx a (privk ca)))
      (send (cat gx (enc gx a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))
      (send (enc "check" n (enc "dh" gx h dhkey))))
    (non-orig dhkey (privk ca)))
  (defrole resp
    (vars (gy h akey) (dhkey skey) (a b ca name) (n text))
    (trace (recv (enc gy b (privk ca)))
      (recv (cat h (enc h a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey))))
      (recv (enc "check" n (enc "dh" h gy dhkey))))
    (non-orig dhkey (privk ca)))
  (defrole ca
    (vars (subject ca name) (gz akey))
    (trace (send (enc gz subject (privk ca))))
    (non-orig (invk gz))
    (uniq-orig gz))
  (defrole CDHcalc1
    (vars (gx gy akey) (dhkey skey))
    (trace (recv (cat gx (invk gy))) (send (enc "dh" gx gy dhkey))))
  (defrole CDHcalc2
    (vars (gx gy akey) (dhkey skey))
    (trace (recv (cat gy (invk gx))) (send (enc "dh" gx gy dhkey))))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b)
    (ca ca))
  (non-orig dhkey (privk ca))
  (uniq-orig n)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (send (enc "check" n (enc "dh" gx gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (recv (enc "check" n (enc "dh" gx gy dhkey)))))
  (label 36)
  (unrealized (0 0) (0 2) (1 0) (1 1) (1 3))
  (preskeleton)
  (origs (n (1 2)))
  (comment "Not a skeleton"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b)
    (ca ca))
  (precedes ((1 2) (0 2)))
  (non-orig dhkey (privk ca))
  (uniq-orig n)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (send (enc "check" n (enc "dh" gx gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (recv (enc "check" n (enc "dh" gx gy dhkey)))))
  (label 37)
  (parent 36)
  (unrealized (0 0) (1 0) (1 1) (1 3))
  (origs (n (1 2)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((1 2) (0 2)) ((2 0) (1 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n gy)
  (operation encryption-test (added-strand ca 1) (enc gy b (privk ca))
    (1 0))
  (strand-map 0 1)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (send (enc "check" n (enc "dh" gx gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (recv (enc "check" n (enc "dh" gx gy dhkey))))
    ((send (enc gy b (privk ca)))))
  (label 38)
  (parent 37)
  (unrealized (0 0) (1 1) (1 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((1 2) (0 2)) ((2 0) (0 0)) ((2 0) (1 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n gy)
  (operation encryption-test (displaced 3 2 ca 1) (enc gx a (privk ca))
    (1 1))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (recv (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy b (privk ca)))))
  (label 39)
  (parent 38)
  (unrealized (1 3))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (precedes ((1 2) (0 2)) ((2 0) (1 0)) ((3 0) (0 0)) ((3 0) (1 1)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n gx gy)
  (operation encryption-test (added-strand ca 1) (enc gx a (privk ca))
    (1 1))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (send (enc "check" n (enc "dh" gx gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (recv (enc "check" n (enc "dh" gx gy dhkey))))
    ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))))
  (label 40)
  (parent 38)
  (unrealized (1 3))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((0 3) (1 3)) ((1 2) (0 2)) ((2 0) (0 0)) ((2 0) (1 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n gy)
  (operation encryption-test (displaced 3 0 init 4)
    (enc "check" n (enc "dh" gy gy dhkey)) (1 3))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (recv (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy b (privk ca)))))
  (label 41)
  (parent 39)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (gy (2 0)) (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca a b-0 ca-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0)
    (ca ca-0))
  (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (0 0)) ((2 0) (1 0))
    ((2 0) (3 0)) ((3 3) (1 3)))
  (non-orig dhkey (invk gy) (privk ca) (privk ca-0))
  (uniq-orig n gy)
  (operation encryption-test (added-strand init 4)
    (enc "check" n (enc "dh" gy gy dhkey)) (1 3))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (recv (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy b (privk ca))))
    ((recv (enc gy a (privk ca-0)))
      (send (cat gy (enc gy a (privk ca-0))))
      (recv
        (cat gy (enc gy b-0 (privk ca-0))
          (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey)))))
  (label 42)
  (parent 39)
  (unrealized (3 0) (3 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (deflistener (enc "dh" gy gy dhkey))
  (precedes ((1 2) (0 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((2 0) (3 0))
    ((3 1) (1 3)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n gy)
  (operation encryption-test (added-listener (enc "dh" gy gy dhkey))
    (enc "check" n (enc "dh" gy gy dhkey)) (1 3))
  (strand-map 0 1 2)
  (traces
    ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (recv (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy b (privk ca))))
    ((recv (enc "dh" gy gy dhkey)) (send (enc "dh" gy gy dhkey))))
  (label 43)
  (parent 39)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (precedes ((0 3) (1 3)) ((1 2) (0 2)) ((2 0) (1 0)) ((3 0) (0 0))
    ((3 0) (1 1)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n gx gy)
  (operation encryption-test (displaced 4 0 init 4)
    (enc "check" n (enc "dh" gx gy dhkey)) (1 3))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (send (enc "check" n (enc "dh" gx gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (recv (enc "check" n (enc "dh" gx gy dhkey))))
    ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))))
  (label 44)
  (parent 40)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (gx (3 0)) (gy (2 0)) (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (a b ca a-0 b-0 ca-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a-0) (b b-0)
    (ca ca-0))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (0 0))
    ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca) (privk ca-0))
  (uniq-orig n gx gy)
  (operation encryption-test (added-strand init 4)
    (enc "check" n (enc "dh" gx gy dhkey)) (1 3))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (send (enc "check" n (enc "dh" gx gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (recv (enc "check" n (enc "dh" gx gy dhkey))))
    ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca))))
    ((recv (enc gx a-0 (privk ca-0)))
      (send (cat gx (enc gx a-0 (privk ca-0))))
      (recv
        (cat gy (enc gy b-0 (privk ca-0))
          (enc n (enc "dh" gx gy dhkey))))
      (send (enc "check" n (enc "dh" gx gy dhkey)))))
  (label 45)
  (parent 40)
  (unrealized (4 0) (4 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (deflistener (enc "dh" gx gy dhkey))
  (precedes ((1 2) (0 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (0 0))
    ((3 0) (1 1)) ((3 0) (4 0)) ((4 1) (1 3)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n gx gy)
  (operation encryption-test (added-listener (enc "dh" gx gy dhkey))
    (enc "check" n (enc "dh" gx gy dhkey)) (1 3))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (send (enc "check" n (enc "dh" gx gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (recv (enc "check" n (enc "dh" gx gy dhkey))))
    ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca))))
    ((recv (enc "dh" gx gy dhkey)) (send (enc "dh" gx gy dhkey))))
  (label 46)
  (parent 40)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0)
    (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (0 0)) ((2 0) (1 0))
    ((2 0) (3 0)) ((3 3) (1 3)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n gy)
  (operation encryption-test (displaced 4 2 ca 1)
    (enc gy a (privk ca-0)) (3 0))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (recv (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy b (privk ca))))
    ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca))))
      (recv
        (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey)))))
  (label 47)
  (parent 42)
  (unrealized (3 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (a b ca b-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b-0)
    (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (0 0))
    ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n gx gy)
  (operation encryption-test (displaced 5 3 ca 1)
    (enc gx a-0 (privk ca-0)) (4 0))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (send (enc "check" n (enc "dh" gx gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (recv (enc "check" n (enc "dh" gx gy dhkey))))
    ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca))))
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (send (enc "check" n (enc "dh" gx gy dhkey)))))
  (label 48)
  (parent 45)
  (unrealized (4 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b)
    (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (0 0)) ((2 0) (1 0))
    ((2 0) (3 0)) ((3 3) (1 3)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n gy)
  (operation encryption-test (displaced 4 2 ca 1)
    (enc gy b-0 (privk ca)) (3 2))
  (strand-map 0 1 2 3)
  (traces
    ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (recv (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy b (privk ca))))
    ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey)))))
  (label 49)
  (parent 47)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (gy (2 0)) (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b)
    (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (0 0))
    ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n gx gy)
  (operation encryption-test (displaced 5 2 ca 1)
    (enc gy b-0 (privk ca)) (4 2))
  (strand-map 0 1 2 3 4)
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (send (enc "check" n (enc "dh" gx gy dhkey))))
    ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (recv (enc "check" n (enc "dh" gx gy dhkey))))
    ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca))))
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey))))
      (send (enc "check" n (enc "dh" gx gy dhkey)))))
  (label 50)
  (parent 48)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (gy (2 0)) (gx (3 0)) (n (1 2))))

(comment "Nothing left to do")