cpsa-4.4.4: tst/dh-ca_hack_shapes.tst

(comment "CPSA 4.3.1")
(comment "Extracted shapes")

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

(comment "CPSA 4.3.1")

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

(comment "Strand count bounded at 12")

(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)))
  (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 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))
  (operation encryption-test (displaced 3 1 ca 1)
    (enc gx a-0 (privk ca)) (2 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 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 13)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b a) (ca ca) (n n))))
  (origs))

(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))
  (defstrand ca 1 (gz gx) (subject a-0) (ca ca))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)) ((3 0) (2 1)))
  (non-orig dhkey (invk gx) (privk ca))
  (operation encryption-test (added-strand ca 1) (enc gx a-0 (privk ca))
    (2 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 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)))))
    ((send (enc gx a-0 (privk ca)))))
  (label 14)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b a) (ca ca) (n n))))
  (origs))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a ca b 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 b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject b) (ca ca))
  (precedes ((1 0) (0 0)) ((1 0) (2 1)) ((2 2) (0 2)) ((3 0) (2 0)))
  (non-orig dhkey (invk gx) (privk ca))
  (operation encryption-test (displaced 4 1 ca 1)
    (enc gx a-0 (privk ca-0)) (2 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))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))))
    ((send (enc gx b (privk ca)))))
  (label 15)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b a) (ca ca) (n n))))
  (origs))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a ca 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 b) (b b)
    (ca ca-0))
  (defstrand ca 1 (gz gx) (subject b) (ca ca-0))
  (precedes ((1 0) (0 0)) ((2 2) (0 2)) ((3 0) (2 0)))
  (non-orig dhkey (invk gx) (privk ca) (privk ca-0))
  (operation encryption-test (displaced 4 3 ca 1)
    (enc gx a-0 (privk ca-0)) (2 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 b (privk ca-0))))
      (send
        (cat gx (enc gx b (privk ca-0))
          (enc n (enc "dh" gx gx dhkey)))))
    ((send (enc gx b (privk ca-0)))))
  (label 16)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b a) (ca ca) (n n))))
  (origs))

(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))
  (defstrand ca 1 (gz gx) (subject b) (ca ca-0))
  (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0))
  (precedes ((1 0) (0 0)) ((2 2) (0 2)) ((3 0) (2 0)) ((4 0) (2 1)))
  (non-orig dhkey (invk gx) (privk ca) (privk ca-0))
  (operation encryption-test (added-strand ca 1)
    (enc gx a-0 (privk ca-0)) (2 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)))))
    ((send (enc gx b (privk ca-0)))) ((send (enc gx a-0 (privk ca-0)))))
  (label 17)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b a) (ca ca) (n n))))
  (origs))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand ca 1 (gz gx) (subject b) (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) (3 0)) ((2 0) (0 2)) ((3 2) (0 2)))
  (non-orig dhkey (invk gx) (privk ca))
  (operation encryption-test (displaced 4 1 ca 1)
    (enc gx a-0 (privk ca)) (3 1))
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx a (privk ca)))) ((send (enc gx b (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 18)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b b) (ca ca) (n n))))
  (origs))

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

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

(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))
  (operation encryption-test (displaced 4 1 ca 1)
    (enc gx a-0 (privk ca)) (3 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))))
    ((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 21)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((gx gx) (h h) (dhkey dhkey) (a a) (b b) (ca ca) (n n))))
  (origs))

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

(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))
  (defstrand ca 1 (gz gx) (subject a-0) (ca ca))
  (precedes ((1 0) (0 0)) ((2 0) (3 0)) ((3 2) (0 2)) ((4 0) (3 1)))
  (non-orig dhkey (invk gx) (invk h) (privk ca))
  (operation encryption-test (added-strand ca 1) (enc gx a-0 (privk ca))
    (3 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))))
    ((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)))))
    ((send (enc gx a-0 (privk ca)))))
  (label 23)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((gx gx) (h h) (dhkey dhkey) (a a) (b b) (ca ca) (n n))))
  (origs))

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

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx h akey) (a b ca b-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) (b b-0)
    (ca ca))
  (defstrand ca 1 (gz h) (subject b-0) (ca ca))
  (precedes ((1 0) (0 0)) ((1 0) (3 1)) ((2 0) (0 2)) ((3 2) (0 2))
    ((4 0) (3 0)))
  (non-orig dhkey (invk gx) (invk h) (privk ca))
  (operation encryption-test (displaced 5 1 ca 1)
    (enc gx a-0 (privk ca-0)) (3 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))))
    ((recv (enc h b-0 (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat h (enc h b-0 (privk ca)) (enc n (enc "dh" gx h dhkey)))))
    ((send (enc h b-0 (privk ca)))))
  (label 25)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((gx gx) (h h) (dhkey dhkey) (a a) (b b) (ca ca) (n n))))
  (origs))

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

(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))
  (defstrand ca 1 (gz h) (subject b-0) (ca ca-0))
  (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0))
  (precedes ((1 0) (0 0)) ((2 0) (0 2)) ((3 2) (0 2)) ((4 0) (3 0))
    ((5 0) (3 1)))
  (non-orig dhkey (invk gx) (invk h) (privk ca) (privk ca-0))
  (operation encryption-test (added-strand ca 1)
    (enc gx a-0 (privk ca-0)) (3 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))))
    ((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)))))
    ((send (enc h b-0 (privk ca-0))))
    ((send (enc gx a-0 (privk ca-0)))))
  (label 27)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((gx gx) (h h) (dhkey dhkey) (a a) (b b) (ca ca) (n n))))
  (origs))

(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)))
  (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 28)
  (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 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)
  (operation encryption-test (displaced 3 1 ca 1)
    (enc gy b-0 (privk ca)) (2 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 41)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a b) (b b) (ca ca))))
  (origs (n (0 2))))

(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))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca))
  (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 3) (0 3))
    ((3 0) (2 2)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca))
    (2 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))))
    ((send (enc gy b-0 (privk ca)))))
  (label 42)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a b) (b b) (ca ca))))
  (origs (n (0 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca a 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)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((2 3) (0 3)) ((3 0) (2 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 4 1 ca 1)
    (enc gy b-0 (privk ca-0)) (2 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 a (privk ca))) (send (cat gy (enc gy a (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))))
    ((send (enc gy a (privk ca)))))
  (label 43)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a b) (b b) (ca ca))))
  (origs (n (0 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca a 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 a)
    (ca ca-0))
  (defstrand ca 1 (gz gy) (subject a) (ca ca-0))
  (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((2 3) (0 3)) ((3 0) (2 0)))
  (non-orig dhkey (invk gy) (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation encryption-test (displaced 4 3 ca 1)
    (enc gy b-0 (privk ca-0)) (2 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 a (privk ca-0)))
      (send (cat gy (enc gy a (privk ca-0))))
      (recv
        (cat gy (enc gy a (privk ca-0)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy a (privk ca-0)))))
  (label 44)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a b) (b b) (ca ca))))
  (origs (n (0 2))))

(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))
  (defstrand ca 1 (gz gy) (subject a) (ca ca-0))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0))
  (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((2 3) (0 3)) ((3 0) (2 0))
    ((4 0) (2 2)))
  (non-orig dhkey (invk gy) (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1)
    (enc gy b-0 (privk ca-0)) (2 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 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))))
    ((send (enc gy a (privk ca-0)))) ((send (enc gy b-0 (privk ca-0)))))
  (label 45)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a b) (b b) (ca ca))))
  (origs (n (0 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b)
    (ca ca))
  (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 1))
    ((3 3) (0 3)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 4 1 ca 1)
    (enc gy b-0 (privk ca)) (3 2))
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (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)))) ((send (enc gy a (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 46)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a a) (b b) (ca ca))))
  (origs (n (0 2))))

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

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (a b ca b-0 name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca))
  (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 1))
    ((3 3) (0 3)) ((4 0) (3 2)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca))
    (3 2))
  (traces
    ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (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)))) ((send (enc gy a (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))))
    ((send (enc gy b-0 (privk ca)))))
  (label 48)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a a) (b b) (ca ca))))
  (origs (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)
  (operation encryption-test (displaced 4 1 ca 1)
    (enc gy b-0 (privk ca)) (3 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 (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 49)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h h) (dhkey dhkey) (a a) (b b) (ca ca))))
  (origs (n (0 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (h akey) (a b ca name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy h) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz h) (subject b) (ca ca))
  (defstrand ca 1 (gz h) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h h) (a a) (b a)
    (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 h) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 4 2 ca 1)
    (enc gy b-0 (privk ca)) (3 2))
  (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))))
    ((send (enc h 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 h (enc h a (privk ca)) (enc n (enc "dh" h h dhkey))))
      (send (enc "check" n (enc "dh" h h dhkey)))))
  (label 50)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy h) (h h) (dhkey dhkey) (a a) (b b) (ca ca))))
  (origs (n (0 2))))

(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))
  (defstrand ca 1 (gz gy) (subject 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)) ((4 0) (3 2)))
  (non-orig dhkey (invk gy) (invk h) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca))
    (3 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 (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))))
    ((send (enc gy b-0 (privk ca)))))
  (label 51)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h h) (dhkey dhkey) (a a) (b b) (ca ca))))
  (origs (n (0 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (h akey) (a b ca a-0 name))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy h) (h h) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz h) (subject b) (ca ca))
  (defstrand ca 1 (gz h) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h h) (a a-0) (b a)
    (ca ca))
  (defstrand ca 1 (gz h) (subject a-0) (ca ca))
  (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((3 3) (0 3))
    ((4 0) (3 0)))
  (non-orig dhkey (invk h) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 5 2 ca 1)
    (enc gy b-0 (privk ca-0)) (3 2))
  (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))))
    ((send (enc h b (privk ca)))) ((send (enc h a (privk ca))))
    ((recv (enc h a-0 (privk ca))) (send (cat h (enc h a-0 (privk ca))))
      (recv (cat h (enc h a (privk ca)) (enc n (enc "dh" h h dhkey))))
      (send (enc "check" n (enc "dh" h h dhkey))))
    ((send (enc h a-0 (privk ca)))))
  (label 52)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy h) (h h) (dhkey dhkey) (a a) (b b) (ca ca))))
  (origs (n (0 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy h akey) (a b ca a-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)
    (ca ca))
  (defstrand ca 1 (gz h) (subject a-0) (ca ca))
  (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((3 3) (0 3))
    ((4 0) (3 0)))
  (non-orig dhkey (invk gy) (invk h) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 5 1 ca 1)
    (enc gy b-0 (privk ca-0)) (3 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))) (send (cat h (enc h a-0 (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))))
    ((send (enc h a-0 (privk ca)))))
  (label 53)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h h) (dhkey dhkey) (a a) (b b) (ca ca))))
  (origs (n (0 2))))

(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))
  (defstrand ca 1 (gz h) (subject b) (ca ca))
  (defstrand ca 1 (gz h) (subject a) (ca ca))
  (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) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((3 3) (0 3))
    ((4 0) (3 0)))
  (non-orig dhkey (invk h) (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation encryption-test (displaced 5 4 ca 1)
    (enc gy b-0 (privk ca-0)) (3 2))
  (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))))
    ((send (enc h 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 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 54)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy h) (h h) (dhkey dhkey) (a a) (b b) (ca ca))))
  (origs (n (0 2))))

(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))
  (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) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((3 3) (0 3))
    ((4 0) (3 0)) ((5 0) (3 2)))
  (non-orig dhkey (invk gy) (invk h) (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1)
    (enc gy b-0 (privk ca-0)) (3 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))))
    ((send (enc h a-0 (privk ca-0))))
    ((send (enc gy b-0 (privk ca-0)))))
  (label 55)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((n n) (gy gy) (h h) (dhkey dhkey) (a a) (b b) (ca ca))))
  (origs (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)))
  (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 56)
  (unrealized (0 0) (0 1) (0 3) (1 0))
  (preskeleton)
  (origs (n (0 2)))
  (comment "Not a skeleton"))

(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)))
  (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 68)
  (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) (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)
  (operation encryption-test (displaced 3 2 ca 1) (enc gy b (privk ca))
    (0 0))
  (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 79)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(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 ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((0 3) (1 3)) ((1 2) (0 2)) ((2 0) (1 0)) ((3 0) (0 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gy b (privk ca))
    (0 0))
  (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)))) ((send (enc gy b (privk ca)))))
  (label 80)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (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))
  (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)
  (operation encryption-test (displaced 4 3 ca 1) (enc gx a (privk ca))
    (0 0))
  (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 84)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (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 ca 1 (gz gx) (subject a) (ca ca))
  (precedes ((0 3) (1 3)) ((1 2) (0 2)) ((2 0) (1 0)) ((3 0) (1 1))
    ((4 0) (0 0)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gx a (privk ca))
    (0 0))
  (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))))
    ((send (enc gx a (privk ca)))))
  (label 85)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(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)
  (operation encryption-test (displaced 4 2 ca 1) (enc gy b (privk ca))
    (0 0))
  (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 104)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(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))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((2 0) (3 0))
    ((3 3) (1 3)) ((4 0) (0 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gy b (privk ca))
    (0 0))
  (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))))
    ((send (enc gy b (privk ca)))))
  (label 105)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(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))
  (defstrand ca 1 (gz gy) (subject 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)) ((4 0) (3 2)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 5 2 ca 1) (enc gy b (privk ca))
    (0 0))
  (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))))
    ((send (enc gy b-0 (privk ca)))))
  (label 106)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(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))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((2 0) (3 0))
    ((3 3) (1 3)) ((4 0) (3 2)) ((5 0) (0 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gy b (privk ca))
    (0 0))
  (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))))
    ((send (enc gy b-0 (privk ca)))) ((send (enc gy b (privk ca)))))
  (label 108)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca a 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)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 3) (1 3)) ((4 0) (3 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 5 2 ca 1) (enc gy b (privk ca))
    (0 0))
  (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))) (send (cat gy (enc gy a (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))))
    ((send (enc gy a (privk ca)))))
  (label 109)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

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

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca a 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)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3))
    ((4 0) (3 0)) ((5 0) (0 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gy b (privk ca))
    (0 0))
  (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))) (send (cat gy (enc gy a (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))))
    ((send (enc gy a (privk ca)))) ((send (enc gy b (privk ca)))))
  (label 111)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca a 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 a)
    (ca ca-0))
  (defstrand ca 1 (gz gy) (subject a) (ca ca-0))
  (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 3) (1 3)) ((4 0) (3 0)))
  (non-orig dhkey (invk gy) (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation encryption-test (displaced 5 2 ca 1) (enc gy b (privk ca))
    (0 0))
  (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 a (privk ca-0)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy a (privk ca-0)))))
  (label 112)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (b ca a 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 a)
    (ca ca-0))
  (defstrand ca 1 (gz gy) (subject a) (ca ca-0))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3))
    ((4 0) (3 0)) ((5 0) (0 0)))
  (non-orig dhkey (invk gy) (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gy b (privk ca))
    (0 0))
  (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 a (privk ca-0)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy a (privk ca-0)))) ((send (enc gy b (privk ca)))))
  (label 113)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b a)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b a)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3))
    ((4 0) (0 0)) ((4 0) (3 0)) ((5 0) (3 2)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 6 4 ca 1)
    (enc gy b-0 (privk ca-0)) (0 0))
  (traces
    ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca))))
      (recv
        (cat gy (enc gy a (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey))))
    ((recv (enc gy a (privk ca))) (recv (cat gy (enc gy a (privk ca))))
      (send
        (cat gy (enc gy a (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (recv (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy a (privk ca))))
    ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (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))))
    ((send (enc gy a (privk ca)))) ((send (enc gy b (privk ca)))))
  (label 114)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b a) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (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))
  (defstrand ca 1 (gz gy) (subject a) (ca ca-0))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0))
  (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 3) (1 3)) ((4 0) (3 0)) ((5 0) (3 2)))
  (non-orig dhkey (invk gy) (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation encryption-test (displaced 6 2 ca 1) (enc gy b (privk ca))
    (0 0))
  (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))))
    ((send (enc gy a (privk ca-0)))) ((send (enc gy b-0 (privk ca-0)))))
  (label 115)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (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))
  (defstrand ca 1 (gz gy) (subject a) (ca ca-0))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3))
    ((4 0) (3 0)) ((5 0) (3 2)) ((6 0) (0 0)))
  (non-orig dhkey (invk gy) (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gy b (privk ca))
    (0 0))
  (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))))
    ((send (enc gy a (privk ca-0)))) ((send (enc gy b-0 (privk ca-0))))
    ((send (enc gy b (privk ca)))))
  (label 117)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (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) (4 2)) ((2 0) (1 0)) ((2 0) (4 0))
    ((3 0) (0 0)) ((3 0) (1 1)) ((4 3) (1 3)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 5 3 ca 1) (enc gy a (privk ca))
    (0 0))
  (traces
    ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (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 a (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)))) ((send (enc gy a (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 119)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0))
    ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (0 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gy a (privk ca))
    (0 0))
  (traces
    ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (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 a (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)))) ((send (enc gy a (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))))
    ((send (enc gy a (privk ca)))))
  (label 120)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

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

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b a)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0))
    ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (0 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gy a (privk ca))
    (0 0))
  (traces
    ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (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 a (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)))) ((send (enc gy a (privk ca))))
    ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca))))
      (recv
        (cat gy (enc gy a (privk ca)) (enc n (enc "dh" gy gy dhkey))))
      (send (enc "check" n (enc "dh" gy gy dhkey))))
    ((send (enc gy a (privk ca)))))
  (label 122)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (a b ca b-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0))
    ((3 0) (0 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 2)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 6 3 ca 1) (enc gy a (privk ca))
    (0 0))
  (traces
    ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (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 a (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)))) ((send (enc gy a (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))))
    ((send (enc gy b-0 (privk ca)))))
  (label 123)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gy akey) (a b ca b-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b) (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0)
    (ca ca))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca))
  (defstrand ca 1 (gz gy) (subject a) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0))
    ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 2)) ((6 0) (0 0)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gy a (privk ca))
    (0 0))
  (traces
    ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (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 a (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)))) ((send (enc gy a (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))))
    ((send (enc gy b-0 (privk ca)))) ((send (enc gy a (privk ca)))))
  (label 126)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (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)
  (operation encryption-test (displaced 5 3 ca 1) (enc gx a (privk ca))
    (0 0))
  (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 128)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (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))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1))
    ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (0 0)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gx a (privk ca))
    (0 0))
  (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))))
    ((send (enc gx a (privk ca)))))
  (label 129)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a)
    (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) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 5 3 ca 1) (enc gx a (privk ca))
    (0 0))
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (recv (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx 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 gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey)))))
  (label 130)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a b ca name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (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 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1))
    ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (0 0)))
  (non-orig dhkey (invk gx) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gx a (privk ca))
    (0 0))
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (recv (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx 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 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 131)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(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))
  (defstrand ca 1 (gz gy) (subject 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)) ((5 0) (4 2)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 6 3 ca 1) (enc gx a (privk ca))
    (0 0))
  (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))))
    ((send (enc gy b-0 (privk ca)))))
  (label 132)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(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))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1))
    ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (4 2)) ((6 0) (0 0)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gx a (privk ca))
    (0 0))
  (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))))
    ((send (enc gy b-0 (privk ca)))) ((send (enc gx a (privk ca)))))
  (label 135)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a b ca a-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a-0) (b a)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a-0) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (0 0))
    ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0)))
  (non-orig dhkey (invk gx) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 6 3 ca 1) (enc gx a (privk ca))
    (0 0))
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (recv (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx b (privk ca)))) ((send (enc gx a (privk ca))))
    ((recv (enc gx a-0 (privk ca)))
      (send (cat gx (enc gx a-0 (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-0 (privk ca)))))
  (label 136)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (b ca a name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (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 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1))
    ((4 3) (1 3)) ((5 0) (0 0)) ((5 0) (4 0)))
  (non-orig dhkey (invk gx) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 6 5 ca 1)
    (enc gx a-0 (privk ca)) (0 0))
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (recv (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx 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 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 138)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a b ca a-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a-0) (b a)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a-0) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1))
    ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (0 0)))
  (non-orig dhkey (invk gx) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gx a (privk ca))
    (0 0))
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (recv (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx b (privk ca)))) ((send (enc gx a (privk ca))))
    ((recv (enc gx a-0 (privk ca)))
      (send (cat gx (enc gx a-0 (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-0 (privk ca)))) ((send (enc gx a (privk ca)))))
  (label 139)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (a b ca a-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)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a-0) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (0 0))
    ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 6 3 ca 1) (enc gx a (privk ca))
    (0 0))
  (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)))
      (send (cat gx (enc gx a-0 (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))))
    ((send (enc gx a-0 (privk ca)))))
  (label 140)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (b ca a 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))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1))
    ((4 3) (1 3)) ((5 0) (0 0)) ((5 0) (4 0)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 6 5 ca 1)
    (enc gx a-0 (privk ca)) (0 0))
  (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))))
    ((send (enc gx a (privk ca)))))
  (label 141)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (a b ca a-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)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a-0) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1))
    ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (0 0)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gx a (privk ca))
    (0 0))
  (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)))
      (send (cat gx (enc gx a-0 (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))))
    ((send (enc gx a-0 (privk ca)))) ((send (enc gx a (privk ca)))))
  (label 142)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a b ca a-0 ca-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a-0) (b a-0)
    (ca ca-0))
  (defstrand ca 1 (gz gx) (subject a-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)) ((4 3) (1 3)) ((5 0) (4 0)))
  (non-orig dhkey (invk gx) (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation encryption-test (displaced 6 3 ca 1) (enc gx a (privk ca))
    (0 0))
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (recv (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx 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 gx (enc gx a-0 (privk ca-0))
          (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx a-0 (privk ca-0)))))
  (label 143)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx akey) (a b ca a-0 ca-0 name))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject b) (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a-0) (b a-0)
    (ca ca-0))
  (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1))
    ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (0 0)))
  (non-orig dhkey (invk gx) (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gx a (privk ca))
    (0 0))
  (traces
    ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca))))
      (recv
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca))))
      (send
        (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))
      (recv (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx 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 gx (enc gx a-0 (privk ca-0))
          (enc n (enc "dh" gx gx dhkey))))
      (send (enc "check" n (enc "dh" gx gx dhkey))))
    ((send (enc gx a-0 (privk ca-0)))) ((send (enc gx a (privk ca)))))
  (label 145)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey))))
  (origs (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))
  (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0))
  (defstrand ca 1 (gz gy) (subject 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)) ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (4 2)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation encryption-test (displaced 7 3 ca 1) (enc gx a (privk ca))
    (0 0))
  (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))))
    ((send (enc gx a-0 (privk ca-0))))
    ((send (enc gy b-0 (privk ca-0)))))
  (label 146)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(defskeleton dhca
  (vars (dhkey skey) (n text) (gx gy akey) (b a b-0 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-0)
    (ca ca))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1))
    ((4 3) (1 3)) ((5 0) (0 0)) ((5 0) (4 0)) ((6 0) (4 2)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca))
  (uniq-orig n)
  (operation encryption-test (displaced 7 5 ca 1)
    (enc gx a-0 (privk ca-0)) (0 0))
  (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))))
    ((send (enc gx a (privk ca)))) ((send (enc gy b-0 (privk ca)))))
  (label 148)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (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))
  (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0))
  (defstrand ca 1 (gz gx) (subject a) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1))
    ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (4 2)) ((7 0) (0 0)))
  (non-orig dhkey (invk gx) (invk gy) (privk ca) (privk ca-0))
  (uniq-orig n)
  (operation encryption-test (added-strand ca 1) (enc gx a (privk ca))
    (0 0))
  (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))))
    ((send (enc gx a-0 (privk ca-0))))
    ((send (enc gy b-0 (privk ca-0)))) ((send (enc gx a (privk ca)))))
  (label 150)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(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 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))
  (defstrand ca 1 (gz gy) (subject b-0) (ca ca))
  (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (4 2)))
  (non-orig dhkey (invk gy) (privk ca))
  (uniq-orig n)
  (operation generalization weakened ((3 0) (0 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)))) ((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))))
    ((send (enc gy b-0 (privk ca)))))
  (label 159)
  (parent 68)
  (realized)
  (shape)
  (maps
    ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey))))
  (origs (n (1 2))))

(comment "Nothing left to do")