(herald dhca (algebra diffie-hellman))

(comment "CPSA 3.4.0")
(comment "All input read from dh-ca.scm")

(defprotocol dhca diffie-hellman
  (defrole init
    (vars (x expn) (a b ca name) (h base) (n text))
    (trace (send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (exp h x))))
      (send (enc "check" n (exp h x))))
    (non-orig (privk ca))
    (uniq-gen x))
  (defrole resp
    (vars (y expn) (a b ca name) (h base) (n text))
    (trace (send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat h (enc h a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp h y)))) (recv (enc "check" n (exp h y))))
    (non-orig (privk ca))
    (uniq-gen y))
  (defrole ca
    (vars (subject ca name) (h base))
    (trace (recv (enc "reg" h subject (privk subject)))
      (send (enc h subject (privk ca))))
    (non-orig (privk subject)))
  (comment A diffie-hellman exchange which uses a certificate authority
    to certify long-term DH values))

(defskeleton dhca
  (vars (n text) (a b ca name) (h base) (x expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h h) (x x))
  (non-orig (privk ca))
  (uniq-gen x)
  (comment Full initiator POV No need to make extra assumptions)
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (exp h x))))
      (send (enc "check" n (exp h x)))))
  (label 0)
  (unrealized (0 1) (0 3))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (h base) (x expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h h) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk ca))
  (uniq-gen x)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) x) a (privk ca)) (0 1))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (exp h x))))
      (send (enc "check" n (exp h x))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca)))))
  (label 1)
  (parent 0)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca name) (x expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) x)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk ca))
  (uniq-gen x)
  (operation encryption-test (displaced 2 1 ca 2) (enc h b (privk ca))
    (0 3))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))
          (enc n (exp (gen) (mul x x)))))
      (send (enc "check" n (exp (gen) (mul x x)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca)))))
  (label 2)
  (parent 1)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (h base) (x expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h h) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h h))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (0 3)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen x)
  (operation encryption-test (added-strand ca 2) (enc h b (privk ca))
    (0 3))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (exp h x))))
      (send (enc "check" n (exp h x))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" h b (privk b))) (send (enc h b (privk ca)))))
  (label 3)
  (parent 1)
  (unrealized (0 3) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca a-0 b ca-0 name) (x y expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) x)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca-0)
    (h (exp (gen) (mul x x (rec y)))) (y y))
  (precedes ((0 0) (1 0)) ((0 0) (2 2)) ((1 1) (0 1)) ((2 3) (0 3)))
  (non-orig (privk a) (privk ca) (privk ca-0))
  (uniq-gen x y)
  (operation encryption-test (added-strand resp 4)
    (enc n (exp (gen) (mul x x))) (0 3))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))
          (enc n (exp (gen) (mul x x)))))
      (send (enc "check" n (exp (gen) (mul x x)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca-0)))
      (recv
        (cat (exp (gen) (mul x x (rec y)))
          (enc (exp (gen) (mul x x (rec y))) a-0 (privk ca-0))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca-0))
          (enc n (exp (gen) (mul x x)))))))
  (label 4)
  (parent 2)
  (unrealized (2 1) (2 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca name) (x expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) x)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (deflistener (exp (gen) (mul x x)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
  (non-orig (privk a) (privk ca))
  (uniq-gen x)
  (operation encryption-test (added-listener (exp (gen) (mul x x)))
    (enc n (exp (gen) (mul x x))) (0 3))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))
          (enc n (exp (gen) (mul x x)))))
      (send (enc "check" n (exp (gen) (mul x x)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (exp (gen) (mul x x))) (send (exp (gen) (mul x x)))))
  (label 5)
  (parent 2)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca name) (y expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) y)) (x y))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
  (non-orig (privk a) (privk ca))
  (uniq-gen y)
  (operation encryption-test (displaced 3 0 resp 1)
    (enc "reg" (exp (gen) y-0) b (privk b)) (2 0))
  (traces
    ((send (enc "reg" (exp (gen) y) a (privk a)))
      (recv (enc (exp (gen) y) a (privk ca)))
      (send (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca)))))
  (label 6)
  (parent 3)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 1 (b b) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (0 3)) ((3 0) (2 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen x y)
  (operation encryption-test (added-strand resp 1)
    (enc "reg" (exp (gen) y) b (privk b)) (2 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))))
  (label 7)
  (parent 3)
  (unrealized (0 3))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca a-0 b ca-0 name) (x y expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) x)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca-0)
    (h (exp (gen) (mul x x (rec y)))) (y y))
  (defstrand ca 2 (subject b) (ca ca-0) (h (exp (gen) y)))
  (precedes ((0 0) (1 0)) ((0 0) (2 2)) ((1 1) (0 1)) ((2 0) (3 0))
    ((2 3) (0 3)) ((3 1) (2 1)))
  (non-orig (privk a) (privk ca) (privk b) (privk ca-0))
  (uniq-gen x y)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) y) b (privk ca-0)) (2 1))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))
          (enc n (exp (gen) (mul x x)))))
      (send (enc "check" n (exp (gen) (mul x x)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca-0)))
      (recv
        (cat (exp (gen) (mul x x (rec y)))
          (enc (exp (gen) (mul x x (rec y))) a-0 (privk ca-0))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca-0))
          (enc n (exp (gen) (mul x x))))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca-0)))))
  (label 8)
  (parent 4)
  (unrealized (2 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca name) (x expn) (w expr))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) x)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (deflistener (exp (gen) (mul x x)))
  (deflistener (cat (exp (gen) (mul x x (rec w))) w))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk ca))
  (uniq-gen x)
  (precur (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x x (rec w))) w))
    (exp (gen) (mul x x)) (2 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))
          (enc n (exp (gen) (mul x x)))))
      (send (enc "check" n (exp (gen) (mul x x)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (exp (gen) (mul x x))) (send (exp (gen) (mul x x))))
    ((recv (cat (exp (gen) (mul x x (rec w))) w))
      (send (cat (exp (gen) (mul x x (rec w))) w))))
  (label 9)
  (parent 5)
  (unrealized (3 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca a-0 b ca-0 name) (y y-0 expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) y)) (x y))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca-0)
    (h (exp (gen) (mul y y (rec y-0)))) (y y-0))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (3 2)) ((1 1) (0 1))
    ((2 1) (0 3)) ((3 3) (0 3)))
  (non-orig (privk a) (privk ca) (privk ca-0))
  (uniq-gen y y-0)
  (operation encryption-test (added-strand resp 4)
    (enc n (exp (gen) (mul y y))) (0 3))
  (traces
    ((send (enc "reg" (exp (gen) y) a (privk a)))
      (recv (enc (exp (gen) y) a (privk ca)))
      (send (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((send (enc "reg" (exp (gen) y-0) b (privk b)))
      (recv (enc (exp (gen) y-0) b (privk ca-0)))
      (recv
        (cat (exp (gen) (mul y y (rec y-0)))
          (enc (exp (gen) (mul y y (rec y-0))) a-0 (privk ca-0))))
      (send
        (cat (exp (gen) y-0) (enc (exp (gen) y-0) b (privk ca-0))
          (enc n (exp (gen) (mul y y)))))))
  (label 10)
  (parent 6)
  (unrealized (3 1) (3 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca name) (y expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) y)) (x y))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1))
    ((2 1) (0 3)) ((3 1) (0 3)))
  (non-orig (privk a) (privk ca))
  (uniq-gen y)
  (operation encryption-test (added-listener (exp (gen) (mul y y)))
    (enc n (exp (gen) (mul y y))) (0 3))
  (traces
    ((send (enc "reg" (exp (gen) y) a (privk a)))
      (recv (enc (exp (gen) y) a (privk ca)))
      (send (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y)))))
  (label 11)
  (parent 6)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca a-0 b ca-0 name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca-0) (h (exp (gen) x))
    (y y))
  (precedes ((0 0) (1 0)) ((0 0) (3 2)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 3) (0 3)))
  (non-orig (privk a) (privk ca) (privk b) (privk ca-0))
  (uniq-gen x y)
  (operation encryption-test (displaced 3 4 resp 4)
    (enc n (exp (gen) (mul x y-0))) (0 3))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca-0)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a-0 (privk ca-0))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca-0))
          (enc n (exp (gen) (mul x y)))))))
  (label 12)
  (parent 7)
  (unrealized (3 1) (3 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca a-0 b-0 ca-0 name) (x y y-0 expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 1 (b b) (y y))
  (defstrand resp 4 (n n) (a a-0) (b b-0) (ca ca-0)
    (h (exp (gen) (mul x y (rec y-0)))) (y y-0))
  (precedes ((0 0) (1 0)) ((0 0) (4 2)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (4 2)) ((4 3) (0 3)))
  (non-orig (privk a) (privk b) (privk ca) (privk ca-0))
  (uniq-gen x y y-0)
  (operation encryption-test (added-strand resp 4)
    (enc n (exp (gen) (mul x y))) (0 3))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b))))
    ((send (enc "reg" (exp (gen) y-0) b-0 (privk b-0)))
      (recv (enc (exp (gen) y-0) b-0 (privk ca-0)))
      (recv
        (cat (exp (gen) (mul x y (rec y-0)))
          (enc (exp (gen) (mul x y (rec y-0))) a-0 (privk ca-0))))
      (send
        (cat (exp (gen) y-0) (enc (exp (gen) y-0) b-0 (privk ca-0))
          (enc n (exp (gen) (mul x y)))))))
  (label 13)
  (parent 7)
  (unrealized (4 1) (4 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 1 (b b) (y y))
  (deflistener (exp (gen) (mul x y)))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 3)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen x y)
  (operation encryption-test (added-listener (exp (gen) (mul x y)))
    (enc n (exp (gen) (mul x y))) (0 3))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y)))))
  (label 14)
  (parent 7)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca a-0 b ca-0 name) (x y expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) x)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca-0)
    (h (exp (gen) (mul x x (rec y)))) (y y))
  (defstrand ca 2 (subject b) (ca ca-0) (h (exp (gen) y)))
  (defstrand ca 2 (subject a-0) (ca ca-0)
    (h (exp (gen) (mul x x (rec y)))))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 0) (3 0))
    ((2 0) (4 0)) ((2 3) (0 3)) ((3 1) (2 1)) ((4 1) (2 2)))
  (non-orig (privk a) (privk ca) (privk a-0) (privk b) (privk ca-0))
  (uniq-gen x y)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) (mul x x (rec y))) a-0 (privk ca-0)) (2 2))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))
          (enc n (exp (gen) (mul x x)))))
      (send (enc "check" n (exp (gen) (mul x x)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca-0)))
      (recv
        (cat (exp (gen) (mul x x (rec y)))
          (enc (exp (gen) (mul x x (rec y))) a-0 (privk ca-0))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca-0))
          (enc n (exp (gen) (mul x x))))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca-0))))
    ((recv (enc "reg" (exp (gen) (mul x x (rec y))) a-0 (privk a-0)))
      (send (enc (exp (gen) (mul x x (rec y))) a-0 (privk ca-0)))))
  (label 15)
  (parent 8)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a ca name) (x expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) x)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (deflistener (exp (gen) (mul x x)))
  (deflistener (cat (gen) (mul x x)))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk ca))
  (uniq-gen x)
  (precur (3 0))
  (operation nonce-test (contracted (x-0 x) (w (mul x x))) (gen) (3 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))
          (enc n (exp (gen) (mul x x)))))
      (send (enc "check" n (exp (gen) (mul x x)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (exp (gen) (mul x x))) (send (exp (gen) (mul x x))))
    ((recv (cat (gen) (mul x x))) (send (cat (gen) (mul x x)))))
  (label 16)
  (parent 9)
  (unrealized (2 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca name) (y expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) y)) (x y))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (exp (gen) y) y))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk ca))
  (precur (3 0))
  (uniq-gen y)
  (operation nonce-test (displaced 4 0 resp 1) (exp (gen) y-0) (3 0))
  (traces
    ((send (enc "reg" (exp (gen) y) a (privk a)))
      (recv (enc (exp (gen) y) a (privk ca)))
      (send (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (exp (gen) y) y)) (send (cat (exp (gen) y) y))))
  (label 17)
  (parent 9)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a ca b name) (x y expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) x)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (deflistener (exp (gen) (mul x x)))
  (deflistener (cat (exp (gen) y) (mul x x (rec y))))
  (defstrand resp 1 (b b) (y y))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 1) (2 0)) ((4 0) (3 0)))
  (non-orig (privk a) (privk ca))
  (precur (3 0))
  (uniq-gen x y)
  (operation nonce-test (added-strand resp 1) (exp (gen) y) (3 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))
          (enc n (exp (gen) (mul x x)))))
      (send (enc "check" n (exp (gen) (mul x x)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (exp (gen) (mul x x))) (send (exp (gen) (mul x x))))
    ((recv (cat (exp (gen) y) (mul x x (rec y))))
      (send (cat (exp (gen) y) (mul x x (rec y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))))
  (label 18)
  (parent 9)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a ca a-0 b ca-0 name) (y y-0 expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) y)) (x y))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca-0)
    (h (exp (gen) (mul y y (rec y-0)))) (y y-0))
  (defstrand ca 2 (subject b) (ca ca-0) (h (exp (gen) y-0)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (3 2)) ((1 1) (0 1))
    ((2 1) (0 3)) ((3 0) (4 0)) ((3 3) (0 3)) ((4 1) (3 1)))
  (non-orig (privk a) (privk ca) (privk b) (privk ca-0))
  (uniq-gen y y-0)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) y-0) b (privk ca-0)) (3 1))
  (traces
    ((send (enc "reg" (exp (gen) y) a (privk a)))
      (recv (enc (exp (gen) y) a (privk ca)))
      (send (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((send (enc "reg" (exp (gen) y-0) b (privk b)))
      (recv (enc (exp (gen) y-0) b (privk ca-0)))
      (recv
        (cat (exp (gen) (mul y y (rec y-0)))
          (enc (exp (gen) (mul y y (rec y-0))) a-0 (privk ca-0))))
      (send
        (cat (exp (gen) y-0) (enc (exp (gen) y-0) b (privk ca-0))
          (enc n (exp (gen) (mul y y))))))
    ((recv (enc "reg" (exp (gen) y-0) b (privk b)))
      (send (enc (exp (gen) y-0) b (privk ca-0)))))
  (label 19)
  (parent 10)
  (unrealized (3 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca name) (y expn) (w expr))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) y)) (x y))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (exp (gen) (mul y y (rec w))) w))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 3)) ((3 1) (0 3)) ((4 1) (3 0)))
  (non-orig (privk a) (privk ca))
  (uniq-gen y)
  (precur (4 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y y (rec w))) w))
    (exp (gen) (mul y y)) (3 0))
  (traces
    ((send (enc "reg" (exp (gen) y) a (privk a)))
      (recv (enc (exp (gen) y) a (privk ca)))
      (send (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (exp (gen) (mul y y (rec w))) w))
      (send (cat (exp (gen) (mul y y (rec w))) w))))
  (label 20)
  (parent 11)
  (unrealized (4 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca a-0 b name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((0 0) (3 2)) ((1 1) (0 1)) ((2 1) (3 1))
    ((3 0) (2 0)) ((3 3) (0 3)))
  (non-orig (privk a) (privk ca) (privk b))
  (uniq-gen x y)
  (operation encryption-test (displaced 4 2 ca 2)
    (enc (exp (gen) y) b (privk ca-0)) (3 1))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a-0 (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))))
  (label 21)
  (parent 12)
  (unrealized (3 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca a-0 b ca-0 name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca-0) (h (exp (gen) x))
    (y y))
  (defstrand ca 2 (subject b) (ca ca-0) (h (exp (gen) y)))
  (precedes ((0 0) (1 0)) ((0 0) (3 2)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (4 0)) ((3 3) (0 3)) ((4 1) (3 1)))
  (non-orig (privk a) (privk ca) (privk b) (privk ca-0))
  (uniq-gen x y)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) y) b (privk ca-0)) (3 1))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca-0)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a-0 (privk ca-0))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca-0))
          (enc n (exp (gen) (mul x y))))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca-0)))))
  (label 22)
  (parent 12)
  (unrealized (3 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca a-0 b-0 ca-0 name) (x y y-0 expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 1 (b b) (y y))
  (defstrand resp 4 (n n) (a a-0) (b b-0) (ca ca-0)
    (h (exp (gen) (mul x y (rec y-0)))) (y y-0))
  (defstrand ca 2 (subject b-0) (ca ca-0) (h (exp (gen) y-0)))
  (precedes ((0 0) (1 0)) ((0 0) (4 2)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (4 2)) ((4 0) (5 0)) ((4 3) (0 3))
    ((5 1) (4 1)))
  (non-orig (privk a) (privk b) (privk ca) (privk b-0) (privk ca-0))
  (uniq-gen x y y-0)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) y-0) b-0 (privk ca-0)) (4 1))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b))))
    ((send (enc "reg" (exp (gen) y-0) b-0 (privk b-0)))
      (recv (enc (exp (gen) y-0) b-0 (privk ca-0)))
      (recv
        (cat (exp (gen) (mul x y (rec y-0)))
          (enc (exp (gen) (mul x y (rec y-0))) a-0 (privk ca-0))))
      (send
        (cat (exp (gen) y-0) (enc (exp (gen) y-0) b-0 (privk ca-0))
          (enc n (exp (gen) (mul x y))))))
    ((recv (enc "reg" (exp (gen) y-0) b-0 (privk b-0)))
      (send (enc (exp (gen) y-0) b-0 (privk ca-0)))))
  (label 23)
  (parent 13)
  (unrealized (4 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn) (w expr))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 1 (b b) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) (mul x y (rec w))) w))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (5 0)) ((4 1) (0 3)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen x y)
  (precur (5 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x y (rec w))) w))
    (exp (gen) (mul x y)) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) (mul x y (rec w))) w))
      (send (cat (exp (gen) (mul x y (rec w))) w))))
  (label 24)
  (parent 14)
  (unrealized (5 0))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca name) (x expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) x)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (deflistener (exp (gen) (mul x x)))
  (deflistener (cat (gen) (mul x x)))
  (deflistener x)
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (non-orig (privk a) (privk ca))
  (uniq-gen x)
  (precur (3 0))
  (operation nonce-test (added-listener x) (mul x x) (3 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))
          (enc n (exp (gen) (mul x x)))))
      (send (enc "check" n (exp (gen) (mul x x)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (exp (gen) (mul x x))) (send (exp (gen) (mul x x))))
    ((recv (cat (gen) (mul x x))) (send (cat (gen) (mul x x))))
    ((recv x) (send x)))
  (label 25)
  (parent 16)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a ca a-0 b ca-0 name) (y y-0 expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) y)) (x y))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca-0)
    (h (exp (gen) (mul y y (rec y-0)))) (y y-0))
  (defstrand ca 2 (subject b) (ca ca-0) (h (exp (gen) y-0)))
  (defstrand ca 2 (subject a-0) (ca ca-0)
    (h (exp (gen) (mul y y (rec y-0)))))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (0 3)) ((3 0) (4 0)) ((3 0) (5 0)) ((3 3) (0 3))
    ((4 1) (3 1)) ((5 1) (3 2)))
  (non-orig (privk a) (privk ca) (privk a-0) (privk b) (privk ca-0))
  (uniq-gen y y-0)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) (mul y y (rec y-0))) a-0 (privk ca-0)) (3 2))
  (traces
    ((send (enc "reg" (exp (gen) y) a (privk a)))
      (recv (enc (exp (gen) y) a (privk ca)))
      (send (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((send (enc "reg" (exp (gen) y-0) b (privk b)))
      (recv (enc (exp (gen) y-0) b (privk ca-0)))
      (recv
        (cat (exp (gen) (mul y y (rec y-0)))
          (enc (exp (gen) (mul y y (rec y-0))) a-0 (privk ca-0))))
      (send
        (cat (exp (gen) y-0) (enc (exp (gen) y-0) b (privk ca-0))
          (enc n (exp (gen) (mul y y))))))
    ((recv (enc "reg" (exp (gen) y-0) b (privk b)))
      (send (enc (exp (gen) y-0) b (privk ca-0))))
    ((recv (enc "reg" (exp (gen) (mul y y (rec y-0))) a-0 (privk a-0)))
      (send (enc (exp (gen) (mul y y (rec y-0))) a-0 (privk ca-0)))))
  (label 26)
  (parent 19)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a ca name) (y expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) y)) (x y))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (gen) (mul y y)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 3)) ((3 1) (0 3)) ((4 1) (3 0)))
  (non-orig (privk a) (privk ca))
  (uniq-gen y)
  (precur (4 0))
  (operation nonce-test (contracted (y-0 y) (w (mul y y))) (gen) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) y) a (privk a)))
      (recv (enc (exp (gen) y) a (privk ca)))
      (send (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (gen) (mul y y))) (send (cat (gen) (mul y y)))))
  (label 27)
  (parent 20)
  (unrealized (3 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca name) (y expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) y)) (x y))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (exp (gen) y) y))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 3)) ((3 1) (0 3)) ((4 1) (3 0)))
  (non-orig (privk a) (privk ca))
  (precur (4 0))
  (uniq-gen y)
  (operation nonce-test (displaced 5 0 resp 1) (exp (gen) y-0) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) y) a (privk a)))
      (recv (enc (exp (gen) y) a (privk ca)))
      (send (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (exp (gen) y) y)) (send (cat (exp (gen) y) y))))
  (label 28)
  (parent 20)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a ca b name) (y y-0 expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) y)) (x y))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (exp (gen) y-0) (mul y y (rec y-0))))
  (defstrand resp 1 (b b) (y y-0))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 3)) ((3 1) (0 3)) ((4 1) (3 0)) ((5 0) (4 0)))
  (non-orig (privk a) (privk ca))
  (precur (4 0))
  (uniq-gen y y-0)
  (operation nonce-test (added-strand resp 1) (exp (gen) y-0) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) y) a (privk a)))
      (recv (enc (exp (gen) y) a (privk ca)))
      (send (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (exp (gen) y-0) (mul y y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y y (rec y-0)))))
    ((send (enc "reg" (exp (gen) y-0) b (privk b)))))
  (label 29)
  (parent 20)
  (unrealized (3 0) (4 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a ca b name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 4 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 2)) ((2 1) (3 1))
    ((3 0) (2 0)) ((3 3) (0 3)))
  (non-orig (privk a) (privk ca) (privk b))
  (uniq-gen x y)
  (operation encryption-test (displaced 4 1 ca 2)
    (enc (exp (gen) x) a-0 (privk ca)) (3 2))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))))
  (label 30)
  (parent 21)
  (unrealized)
  (shape)
  (maps ((0) ((x x) (a a) (b b) (ca ca) (h (exp (gen) y)) (n n))))
  (origs))

(defskeleton dhca
  (vars (n text) (a ca a-0 b name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject a-0) (ca ca) (h (exp (gen) x)))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (3 1))
    ((3 0) (2 0)) ((3 3) (0 3)) ((4 1) (3 2)))
  (non-orig (privk a) (privk ca) (privk a-0) (privk b))
  (uniq-gen x y)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) x) a-0 (privk ca)) (3 2))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a-0 (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y))))))
    ((recv (enc "reg" (exp (gen) x) a-0 (privk a-0)))
      (send (enc (exp (gen) x) a-0 (privk ca)))))
  (label 31)
  (parent 21)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca b name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 4 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 2)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (4 0)) ((3 3) (0 3)) ((4 1) (3 1)))
  (non-orig (privk a) (privk ca) (privk b))
  (uniq-gen x y)
  (operation encryption-test (displaced 5 1 ca 2)
    (enc (exp (gen) x) a-0 (privk ca-0)) (3 2))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y))))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca)))))
  (label 32)
  (parent 22)
  (seen 30)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca a-0 b ca-0 name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca-0) (h (exp (gen) x))
    (y y))
  (defstrand ca 2 (subject b) (ca ca-0) (h (exp (gen) y)))
  (defstrand ca 2 (subject a-0) (ca ca-0) (h (exp (gen) x)))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (4 0)) ((3 3) (0 3)) ((4 1) (3 1))
    ((5 1) (3 2)))
  (non-orig (privk a) (privk ca) (privk a-0) (privk b) (privk ca-0))
  (uniq-gen x y)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) x) a-0 (privk ca-0)) (3 2))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca-0)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a-0 (privk ca-0))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca-0))
          (enc n (exp (gen) (mul x y))))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca-0))))
    ((recv (enc "reg" (exp (gen) x) a-0 (privk a-0)))
      (send (enc (exp (gen) x) a-0 (privk ca-0)))))
  (label 33)
  (parent 22)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca a-0 b-0 ca-0 name) (x y y-0 expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 1 (b b) (y y))
  (defstrand resp 4 (n n) (a a-0) (b b-0) (ca ca-0)
    (h (exp (gen) (mul x y (rec y-0)))) (y y-0))
  (defstrand ca 2 (subject b-0) (ca ca-0) (h (exp (gen) y-0)))
  (defstrand ca 2 (subject a-0) (ca ca-0)
    (h (exp (gen) (mul x y (rec y-0)))))
  (precedes ((0 0) (1 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (6 0)) ((4 0) (5 0)) ((4 0) (6 0))
    ((4 3) (0 3)) ((5 1) (4 1)) ((6 1) (4 2)))
  (non-orig (privk a) (privk b) (privk ca) (privk a-0) (privk b-0)
    (privk ca-0))
  (uniq-gen x y y-0)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) (mul x y (rec y-0))) a-0 (privk ca-0)) (4 2))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b))))
    ((send (enc "reg" (exp (gen) y-0) b-0 (privk b-0)))
      (recv (enc (exp (gen) y-0) b-0 (privk ca-0)))
      (recv
        (cat (exp (gen) (mul x y (rec y-0)))
          (enc (exp (gen) (mul x y (rec y-0))) a-0 (privk ca-0))))
      (send
        (cat (exp (gen) y-0) (enc (exp (gen) y-0) b-0 (privk ca-0))
          (enc n (exp (gen) (mul x y))))))
    ((recv (enc "reg" (exp (gen) y-0) b-0 (privk b-0)))
      (send (enc (exp (gen) y-0) b-0 (privk ca-0))))
    ((recv (enc "reg" (exp (gen) (mul x y (rec y-0))) a-0 (privk a-0)))
      (send (enc (exp (gen) (mul x y (rec y-0))) a-0 (privk ca-0)))))
  (label 34)
  (parent 23)
  (unrealized (6 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 1 (b b) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (gen) (mul x y)))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (5 0)) ((4 1) (0 3)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen x y)
  (precur (5 0))
  (operation nonce-test (contracted (x-0 x) (y-0 y) (w (mul x y))) (gen)
    (5 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (gen) (mul x y))) (send (cat (gen) (mul x y)))))
  (label 35)
  (parent 24)
  (unrealized (4 0) (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y y-0 expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x y-0))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 1 (b b) (y y))
  (deflistener (exp (gen) (mul y y-0)))
  (deflistener (cat (exp (gen) y-0) y))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (5 0)) ((4 1) (0 3)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (precur (5 0))
  (uniq-gen y y-0)
  (operation nonce-test (displaced 6 0 resp 1) (exp (gen) y-1) (5 0))
  (traces
    ((send (enc "reg" (exp (gen) y-0) a (privk a)))
      (recv (enc (exp (gen) y-0) a (privk ca)))
      (send (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (send (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0))))
    ((recv (cat (exp (gen) y-0) y)) (send (cat (exp (gen) y-0) y))))
  (label 36)
  (parent 24)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 1 (b b) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (5 0)) ((4 1) (0 3)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (precur (5 0))
  (uniq-gen x y)
  (operation nonce-test (displaced 6 3 resp 1) (exp (gen) y-0) (5 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x))))
  (label 37)
  (parent 24)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca b-0 name) (x y y-0 expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 1 (b b) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y-0) (mul x y (rec y-0))))
  (defstrand resp 1 (b b-0) (y y-0))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (5 0)) ((4 1) (0 3)) ((5 1) (4 0))
    ((6 0) (5 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (precur (5 0))
  (uniq-gen x y y-0)
  (operation nonce-test (added-strand resp 1) (exp (gen) y-0) (5 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) y-0) (mul x y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul x y (rec y-0)))))
    ((send (enc "reg" (exp (gen) y-0) b-0 (privk b-0)))))
  (label 38)
  (parent 24)
  (unrealized (4 0) (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a ca name) (y expn))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (h (exp (gen) y)) (x y))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (gen) (mul y y)))
  (deflistener y)
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (0 3)) ((3 1) (0 3)) ((4 1) (3 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk ca))
  (uniq-gen y)
  (precur (4 0))
  (operation nonce-test (added-listener y) (mul y y) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) y) a (privk a)))
      (recv (enc (exp (gen) y) a (privk ca)))
      (send (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (gen) (mul y y))) (send (cat (gen) (mul y y))))
    ((recv y) (send y)))
  (label 39)
  (parent 27)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a ca b name) (y y-0 expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x y-0))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 4 (n n) (a a) (b b) (ca ca) (h (exp (gen) y-0)) (y y))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (3 1))
    ((3 0) (2 0)) ((3 3) (0 3)) ((4 1) (3 2)))
  (non-orig (privk a) (privk ca) (privk b))
  (uniq-gen y y-0)
  (operation encryption-test (displaced 5 0 resp 1)
    (enc "reg" (exp (gen) y-0) a-0 (privk a-0)) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) y-0) a (privk a)))
      (recv (enc (exp (gen) y-0) a (privk ca)))
      (send (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (send (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0))))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca)))))
  (label 40)
  (parent 31)
  (unrealized)
  (shape)
  (maps ((0) ((x y-0) (a a) (b b) (ca ca) (h (exp (gen) y)) (n n))))
  (origs))

(defskeleton dhca
  (vars (n text) (a ca b ca-0 name) (y y-0 expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x y-0))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand resp 4 (n n) (a a) (b b) (ca ca-0) (h (exp (gen) y-0))
    (y y))
  (defstrand ca 2 (subject b) (ca ca-0) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca-0) (h (exp (gen) y-0)))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (0 3))
    ((3 0) (2 0)) ((3 0) (4 0)) ((3 3) (0 3)) ((4 1) (3 1))
    ((5 1) (3 2)))
  (non-orig (privk a) (privk ca) (privk b) (privk ca-0))
  (uniq-gen y y-0)
  (operation encryption-test (displaced 6 0 resp 1)
    (enc "reg" (exp (gen) y-0) a-0 (privk a-0)) (5 0))
  (traces
    ((send (enc "reg" (exp (gen) y-0) a (privk a)))
      (recv (enc (exp (gen) y-0) a (privk ca)))
      (send (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (send (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca-0)))
      (recv (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca-0))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca-0))
          (enc n (exp (gen) (mul y y-0))))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca-0))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca-0)))))
  (label 41)
  (parent 33)
  (unrealized)
  (shape)
  (maps ((0) ((x y-0) (a a) (b b) (ca ca) (h (exp (gen) y)) (n n))))
  (origs))

(comment "Nothing left to do")

(defprotocol dhca diffie-hellman
  (defrole init
    (vars (x expn) (a b ca name) (h base) (n text))
    (trace (send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (exp h x))))
      (send (enc "check" n (exp h x))))
    (non-orig (privk ca))
    (uniq-gen x))
  (defrole resp
    (vars (y expn) (a b ca name) (h base) (n text))
    (trace (send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat h (enc h a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp h y)))) (recv (enc "check" n (exp h y))))
    (non-orig (privk ca))
    (uniq-gen y))
  (defrole ca
    (vars (subject ca name) (h base))
    (trace (recv (enc "reg" h subject (privk subject)))
      (send (enc h subject (privk ca))))
    (non-orig (privk subject)))
  (comment A diffie-hellman exchange which uses a certificate authority
    to certify long-term DH values))

(defskeleton dhca
  (vars (n text) (a b ca name) (h base) (y expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h h) (y y))
  (non-orig (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (comment Full responder point of view with freshly chosen n)
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat h (enc h a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp h y)))) (recv (enc "check" n (exp h y)))))
  (label 42)
  (unrealized (0 1) (0 2) (0 4))
  (origs (n (0 3)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (h base) (y expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h h) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk b) (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) y) b (privk ca)) (0 1))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat h (enc h a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp h y)))) (recv (enc "check" n (exp h y))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca)))))
  (label 43)
  (parent 42)
  (unrealized (0 2) (0 4))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk b) (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (operation encryption-test (displaced 2 1 ca 2) (enc h a (privk ca))
    (0 2))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca)))))
  (label 44)
  (parent 43)
  (unrealized (0 4))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (h base) (y expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h h) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h h))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (0 2)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2) (enc h a (privk ca))
    (0 2))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat h (enc h a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp h y)))) (recv (enc "check" n (exp h y))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" h a (privk a))) (send (enc h a (privk ca)))))
  (label 45)
  (parent 43)
  (unrealized (0 4) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0)
    (h (exp (gen) (mul y y (rec x)))) (x x))
  (precedes ((0 0) (1 0)) ((0 3) (2 3)) ((1 1) (0 1)) ((2 4) (0 4)))
  (non-orig (privk b) (privk ca) (privk ca-0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (added-strand init 5)
    (enc "check" n (exp (gen) (mul y y))) (0 4))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca-0))))
      (recv
        (cat (exp (gen) (mul y y (rec x)))
          (enc (exp (gen) (mul y y (rec x))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y))))))
  (label 46)
  (parent 44)
  (unrealized (2 1) (2 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 4)))
  (non-orig (privk b) (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (operation encryption-test (added-listener (exp (gen) (mul y y)))
    (enc "check" n (exp (gen) (mul y y))) (0 4))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y)))))
  (label 47)
  (parent 44)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 2)))
  (non-orig (privk b) (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (operation encryption-test (displaced 3 0 resp 1)
    (enc "reg" (exp (gen) y-0) a (privk a)) (2 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca)))))
  (label 48)
  (parent 45)
  (unrealized (0 4))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y y-0 expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y-0)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (defstrand resp 1 (b a) (y y-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (0 2)) ((3 0) (2 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen y y-0)
  (uniq-orig n)
  (operation encryption-test (added-strand resp 1)
    (enc "reg" (exp (gen) y-0) a (privk a)) (2 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (recv (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((send (enc "reg" (exp (gen) y-0) a (privk a)))))
  (label 49)
  (parent 45)
  (unrealized (0 4))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0)
    (h (exp (gen) (mul y y (rec x)))) (x x))
  (defstrand ca 2 (subject a) (ca ca-0) (h (exp (gen) x)))
  (precedes ((0 0) (1 0)) ((0 3) (2 3)) ((1 1) (0 1)) ((2 0) (3 0))
    ((2 4) (0 4)) ((3 1) (2 1)))
  (non-orig (privk b) (privk ca) (privk a) (privk ca-0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) x) a (privk ca-0)) (2 1))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca-0))))
      (recv
        (cat (exp (gen) (mul y y (rec x)))
          (enc (exp (gen) (mul y y (rec x))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca-0)))))
  (label 50)
  (parent 46)
  (unrealized (2 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y expn) (w expr))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (exp (gen) (mul y y (rec w))) w))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 4))
    ((3 1) (2 0)))
  (non-orig (privk b) (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (precur (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y y (rec w))) w))
    (exp (gen) (mul y y)) (2 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (exp (gen) (mul y y (rec w))) w))
      (send (cat (exp (gen) (mul y y (rec w))) w))))
  (label 51)
  (parent 47)
  (unrealized (3 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0)
    (h (exp (gen) (mul y y (rec x)))) (x x))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 3) (3 3)) ((1 1) (0 1))
    ((2 1) (0 2)) ((3 4) (0 4)))
  (non-orig (privk b) (privk ca) (privk ca-0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (added-strand init 5)
    (enc "check" n (exp (gen) (mul y y))) (0 4))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca-0))))
      (recv
        (cat (exp (gen) (mul y y (rec x)))
          (enc (exp (gen) (mul y y (rec x))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y))))))
  (label 52)
  (parent 48)
  (unrealized (3 1) (3 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1))
    ((2 1) (0 2)) ((3 1) (0 4)))
  (non-orig (privk b) (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (operation encryption-test (added-listener (exp (gen) (mul y y)))
    (enc "check" n (exp (gen) (mul y y))) (0 4))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y)))))
  (label 53)
  (parent 48)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0) (h (exp (gen) y))
    (x x))
  (precedes ((0 0) (1 0)) ((0 3) (3 3)) ((1 1) (0 1)) ((2 1) (0 2))
    ((3 0) (2 0)) ((3 4) (0 4)))
  (non-orig (privk b) (privk ca) (privk a) (privk ca-0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (displaced 3 4 init 5)
    (enc "check" n (exp (gen) (mul y y-0))) (0 4))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (recv (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca-0))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y x)))))
      (send (enc "check" n (exp (gen) (mul y x))))))
  (label 54)
  (parent 49)
  (unrealized (3 1) (3 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca a-0 b-0 ca-0 name) (y y-0 x expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y-0)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (defstrand resp 1 (b a) (y y-0))
  (defstrand init 5 (n n) (a a-0) (b b-0) (ca ca-0)
    (h (exp (gen) (mul y y-0 (rec x)))) (x x))
  (precedes ((0 0) (1 0)) ((0 3) (4 3)) ((1 1) (0 1)) ((2 1) (0 2))
    ((3 0) (2 0)) ((4 4) (0 4)))
  (non-orig (privk a) (privk b) (privk ca) (privk ca-0))
  (uniq-gen y y-0 x)
  (uniq-orig n)
  (operation encryption-test (added-strand init 5)
    (enc "check" n (exp (gen) (mul y y-0))) (0 4))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (recv (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((send (enc "reg" (exp (gen) y-0) a (privk a))))
    ((send (enc "reg" (exp (gen) x) a-0 (privk a-0)))
      (recv (enc (exp (gen) x) a-0 (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a-0 (privk ca-0))))
      (recv
        (cat (exp (gen) (mul y y-0 (rec x)))
          (enc (exp (gen) (mul y y-0 (rec x))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y y-0)))))
      (send (enc "check" n (exp (gen) (mul y y-0))))))
  (label 55)
  (parent 49)
  (unrealized (4 1) (4 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y y-0 expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y-0)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (defstrand resp 1 (b a) (y y-0))
  (deflistener (exp (gen) (mul y y-0)))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (0 2))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (0 4)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen y y-0)
  (uniq-orig n)
  (operation encryption-test (added-listener (exp (gen) (mul y y-0)))
    (enc "check" n (exp (gen) (mul y y-0))) (0 4))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (recv (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((send (enc "reg" (exp (gen) y-0) a (privk a))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0)))))
  (label 56)
  (parent 49)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0)
    (h (exp (gen) (mul y y (rec x)))) (x x))
  (defstrand ca 2 (subject a) (ca ca-0) (h (exp (gen) x)))
  (defstrand ca 2 (subject b-0) (ca ca-0)
    (h (exp (gen) (mul y y (rec x)))))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((0 3) (2 3)) ((1 1) (0 1))
    ((2 0) (3 0)) ((2 0) (4 0)) ((2 4) (0 4)) ((3 1) (2 1))
    ((4 1) (2 3)))
  (non-orig (privk b) (privk ca) (privk a) (privk b-0) (privk ca-0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) (mul y y (rec x))) b-0 (privk ca-0)) (2 3))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca-0))))
      (recv
        (cat (exp (gen) (mul y y (rec x)))
          (enc (exp (gen) (mul y y (rec x))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca-0))))
    ((recv (enc "reg" (exp (gen) (mul y y (rec x))) b-0 (privk b-0)))
      (send (enc (exp (gen) (mul y y (rec x))) b-0 (privk ca-0)))))
  (label 57)
  (parent 50)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (b ca name) (y expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (gen) (mul y y)))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 4))
    ((3 1) (2 0)))
  (non-orig (privk b) (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (precur (3 0))
  (operation nonce-test (contracted (y-0 y) (w (mul y y))) (gen) (3 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (gen) (mul y y))) (send (cat (gen) (mul y y)))))
  (label 58)
  (parent 51)
  (unrealized (2 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (exp (gen) y) y))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 4))
    ((3 1) (2 0)))
  (non-orig (privk b) (privk ca))
  (precur (3 0))
  (uniq-gen y)
  (uniq-orig n)
  (operation nonce-test (displaced 4 0 resp 1) (exp (gen) y-0) (3 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (exp (gen) y) y)) (send (cat (exp (gen) y) y))))
  (label 59)
  (parent 51)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (b ca b-0 name) (y y-0 expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (exp (gen) y-0) (mul y y (rec y-0))))
  (defstrand resp 1 (b b-0) (y y-0))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 4))
    ((3 1) (2 0)) ((4 0) (3 0)))
  (non-orig (privk b) (privk ca))
  (precur (3 0))
  (uniq-gen y y-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 1) (exp (gen) y-0) (3 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (exp (gen) y-0) (mul y y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y y (rec y-0)))))
    ((send (enc "reg" (exp (gen) y-0) b-0 (privk b-0)))))
  (label 60)
  (parent 51)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0)
    (h (exp (gen) (mul y y (rec x)))) (x x))
  (defstrand ca 2 (subject a) (ca ca-0) (h (exp (gen) x)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 3) (3 3)) ((1 1) (0 1))
    ((2 1) (0 2)) ((3 0) (4 0)) ((3 4) (0 4)) ((4 1) (3 1)))
  (non-orig (privk b) (privk ca) (privk a) (privk ca-0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) x) a (privk ca-0)) (3 1))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca-0))))
      (recv
        (cat (exp (gen) (mul y y (rec x)))
          (enc (exp (gen) (mul y y (rec x))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca-0)))))
  (label 61)
  (parent 52)
  (unrealized (3 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y expn) (w expr))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (exp (gen) (mul y y (rec w))) w))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 2)) ((3 1) (0 4)) ((4 1) (3 0)))
  (non-orig (privk b) (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (precur (4 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y y (rec w))) w))
    (exp (gen) (mul y y)) (3 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (exp (gen) (mul y y (rec w))) w))
      (send (cat (exp (gen) (mul y y (rec w))) w))))
  (label 62)
  (parent 53)
  (unrealized (4 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a b-0 name) (y x expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca) (h (exp (gen) y)) (x x))
  (precedes ((0 0) (1 0)) ((0 3) (3 3)) ((1 1) (0 1)) ((2 1) (0 2))
    ((2 1) (3 1)) ((3 0) (2 0)) ((3 4) (0 4)))
  (non-orig (privk b) (privk ca) (privk a))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (displaced 4 2 ca 2)
    (enc (exp (gen) x) a (privk ca-0)) (3 1))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (recv (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b-0 (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (send (enc "check" n (exp (gen) (mul y x))))))
  (label 63)
  (parent 54)
  (unrealized (3 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0) (h (exp (gen) y))
    (x x))
  (defstrand ca 2 (subject a) (ca ca-0) (h (exp (gen) x)))
  (precedes ((0 0) (1 0)) ((0 3) (3 3)) ((1 1) (0 1)) ((2 1) (0 2))
    ((3 0) (2 0)) ((3 0) (4 0)) ((3 4) (0 4)) ((4 1) (3 1)))
  (non-orig (privk b) (privk ca) (privk a) (privk ca-0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) x) a (privk ca-0)) (3 1))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (recv (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca-0))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y x)))))
      (send (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca-0)))))
  (label 64)
  (parent 54)
  (unrealized (3 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca a-0 b-0 ca-0 name) (y y-0 x expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y-0)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (defstrand resp 1 (b a) (y y-0))
  (defstrand init 5 (n n) (a a-0) (b b-0) (ca ca-0)
    (h (exp (gen) (mul y y-0 (rec x)))) (x x))
  (defstrand ca 2 (subject a-0) (ca ca-0) (h (exp (gen) x)))
  (precedes ((0 0) (1 0)) ((0 3) (4 3)) ((1 1) (0 1)) ((2 1) (0 2))
    ((3 0) (2 0)) ((4 0) (5 0)) ((4 4) (0 4)) ((5 1) (4 1)))
  (non-orig (privk a) (privk b) (privk ca) (privk a-0) (privk ca-0))
  (uniq-gen y y-0 x)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) x) a-0 (privk ca-0)) (4 1))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (recv (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((send (enc "reg" (exp (gen) y-0) a (privk a))))
    ((send (enc "reg" (exp (gen) x) a-0 (privk a-0)))
      (recv (enc (exp (gen) x) a-0 (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a-0 (privk ca-0))))
      (recv
        (cat (exp (gen) (mul y y-0 (rec x)))
          (enc (exp (gen) (mul y y-0 (rec x))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y y-0)))))
      (send (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) x) a-0 (privk a-0)))
      (send (enc (exp (gen) x) a-0 (privk ca-0)))))
  (label 65)
  (parent 55)
  (unrealized (4 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y y-0 expn) (w expr))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y-0)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (defstrand resp 1 (b a) (y y-0))
  (deflistener (exp (gen) (mul y y-0)))
  (deflistener (cat (exp (gen) (mul y y-0 (rec w))) w))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (0 2))
    ((3 0) (2 0)) ((3 0) (5 0)) ((4 1) (0 4)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen y y-0)
  (uniq-orig n)
  (precur (5 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y y-0 (rec w))) w))
    (exp (gen) (mul y y-0)) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (recv (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((send (enc "reg" (exp (gen) y-0) a (privk a))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0))))
    ((recv (cat (exp (gen) (mul y y-0 (rec w))) w))
      (send (cat (exp (gen) (mul y y-0 (rec w))) w))))
  (label 66)
  (parent 56)
  (unrealized (5 0))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (gen) (mul y y)))
  (deflistener y)
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (0 4))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (non-orig (privk b) (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (precur (3 0))
  (operation nonce-test (added-listener y) (mul y y) (3 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (gen) (mul y y))) (send (cat (gen) (mul y y))))
    ((recv y) (send y)))
  (label 67)
  (parent 58)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0)
    (h (exp (gen) (mul y y (rec x)))) (x x))
  (defstrand ca 2 (subject a) (ca ca-0) (h (exp (gen) x)))
  (defstrand ca 2 (subject b-0) (ca ca-0)
    (h (exp (gen) (mul y y (rec x)))))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (5 0)) ((0 3) (3 3))
    ((1 1) (0 1)) ((2 1) (0 2)) ((3 0) (4 0)) ((3 0) (5 0))
    ((3 4) (0 4)) ((4 1) (3 1)) ((5 1) (3 3)))
  (non-orig (privk b) (privk ca) (privk a) (privk b-0) (privk ca-0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) (mul y y (rec x))) b-0 (privk ca-0)) (3 3))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca-0))))
      (recv
        (cat (exp (gen) (mul y y (rec x)))
          (enc (exp (gen) (mul y y (rec x))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y y)))))
      (send (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca-0))))
    ((recv (enc "reg" (exp (gen) (mul y y (rec x))) b-0 (privk b-0)))
      (send (enc (exp (gen) (mul y y (rec x))) b-0 (privk ca-0)))))
  (label 68)
  (parent 61)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (b ca name) (y expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (gen) (mul y y)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 2)) ((3 1) (0 4)) ((4 1) (3 0)))
  (non-orig (privk b) (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (precur (4 0))
  (operation nonce-test (contracted (y-0 y) (w (mul y y))) (gen) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (gen) (mul y y))) (send (cat (gen) (mul y y)))))
  (label 69)
  (parent 62)
  (unrealized (3 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (exp (gen) y) y))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 2)) ((3 1) (0 4)) ((4 1) (3 0)))
  (non-orig (privk b) (privk ca))
  (precur (4 0))
  (uniq-gen y)
  (uniq-orig n)
  (operation nonce-test (displaced 5 0 resp 1) (exp (gen) y-0) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (exp (gen) y) y)) (send (cat (exp (gen) y) y))))
  (label 70)
  (parent 62)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (b ca b-0 name) (y y-0 expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (exp (gen) y-0) (mul y y (rec y-0))))
  (defstrand resp 1 (b b-0) (y y-0))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 2)) ((3 1) (0 4)) ((4 1) (3 0)) ((5 0) (4 0)))
  (non-orig (privk b) (privk ca))
  (precur (4 0))
  (uniq-gen y y-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 1) (exp (gen) y-0) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (exp (gen) y-0) (mul y y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y y (rec y-0)))))
    ((send (enc "reg" (exp (gen) y-0) b-0 (privk b-0)))))
  (label 71)
  (parent 62)
  (unrealized (3 0) (4 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (b ca a name) (y x expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (precedes ((0 0) (1 0)) ((0 3) (3 3)) ((1 1) (0 1)) ((2 1) (0 2))
    ((2 1) (3 1)) ((3 0) (2 0)) ((3 4) (0 4)))
  (non-orig (privk b) (privk ca) (privk a))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (displaced 4 1 ca 2)
    (enc (exp (gen) y) b-0 (privk ca)) (3 3))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (recv (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (send (enc "check" n (exp (gen) (mul y x))))))
  (label 72)
  (parent 63)
  (unrealized)
  (shape)
  (maps ((0) ((n n) (y y) (a a) (b b) (ca ca) (h (exp (gen) x)))))
  (origs (n (0 3))))

(defskeleton dhca
  (vars (n text) (b ca a b-0 name) (y x expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject b-0) (ca ca) (h (exp (gen) y)))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((0 3) (3 3)) ((1 1) (0 1))
    ((2 1) (0 2)) ((2 1) (3 1)) ((3 0) (2 0)) ((3 4) (0 4))
    ((4 1) (3 3)))
  (non-orig (privk b) (privk ca) (privk a) (privk b-0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) y) b-0 (privk ca)) (3 3))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (recv (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b-0 (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (send (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) y) b-0 (privk b-0)))
      (send (enc (exp (gen) y) b-0 (privk ca)))))
  (label 73)
  (parent 63)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a name) (y x expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (precedes ((0 0) (1 0)) ((0 3) (3 3)) ((1 1) (0 1)) ((2 1) (0 2))
    ((3 0) (2 0)) ((3 0) (4 0)) ((3 4) (0 4)) ((4 1) (3 1)))
  (non-orig (privk b) (privk ca) (privk a))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (displaced 5 1 ca 2)
    (enc (exp (gen) y) b-0 (privk ca-0)) (3 3))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (recv (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (send (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca)))))
  (label 74)
  (parent 64)
  (unrealized)
  (shape)
  (maps ((0) ((n n) (y y) (a a) (b b) (ca ca) (h (exp (gen) x)))))
  (origs (n (0 3))))

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0) (h (exp (gen) y))
    (x x))
  (defstrand ca 2 (subject a) (ca ca-0) (h (exp (gen) x)))
  (defstrand ca 2 (subject b-0) (ca ca-0) (h (exp (gen) y)))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((0 3) (3 3)) ((1 1) (0 1))
    ((2 1) (0 2)) ((3 0) (2 0)) ((3 0) (4 0)) ((3 4) (0 4))
    ((4 1) (3 1)) ((5 1) (3 3)))
  (non-orig (privk b) (privk ca) (privk a) (privk b-0) (privk ca-0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) y) b-0 (privk ca-0)) (3 3))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (recv (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca-0))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y x)))))
      (send (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca-0))))
    ((recv (enc "reg" (exp (gen) y) b-0 (privk b-0)))
      (send (enc (exp (gen) y) b-0 (privk ca-0)))))
  (label 75)
  (parent 64)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca a-0 b-0 ca-0 name) (y y-0 x expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y-0)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (defstrand resp 1 (b a) (y y-0))
  (defstrand init 5 (n n) (a a-0) (b b-0) (ca ca-0)
    (h (exp (gen) (mul y y-0 (rec x)))) (x x))
  (defstrand ca 2 (subject a-0) (ca ca-0) (h (exp (gen) x)))
  (defstrand ca 2 (subject b-0) (ca ca-0)
    (h (exp (gen) (mul y y-0 (rec x)))))
  (precedes ((0 0) (1 0)) ((0 0) (6 0)) ((0 3) (4 3)) ((1 1) (0 1))
    ((2 1) (0 2)) ((3 0) (2 0)) ((3 0) (6 0)) ((4 0) (5 0))
    ((4 0) (6 0)) ((4 4) (0 4)) ((5 1) (4 1)) ((6 1) (4 3)))
  (non-orig (privk a) (privk b) (privk ca) (privk a-0) (privk b-0)
    (privk ca-0))
  (uniq-gen y y-0 x)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) (mul y y-0 (rec x))) b-0 (privk ca-0)) (4 3))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (recv (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((send (enc "reg" (exp (gen) y-0) a (privk a))))
    ((send (enc "reg" (exp (gen) x) a-0 (privk a-0)))
      (recv (enc (exp (gen) x) a-0 (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a-0 (privk ca-0))))
      (recv
        (cat (exp (gen) (mul y y-0 (rec x)))
          (enc (exp (gen) (mul y y-0 (rec x))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y y-0)))))
      (send (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) x) a-0 (privk a-0)))
      (send (enc (exp (gen) x) a-0 (privk ca-0))))
    ((recv (enc "reg" (exp (gen) (mul y y-0 (rec x))) b-0 (privk b-0)))
      (send (enc (exp (gen) (mul y y-0 (rec x))) b-0 (privk ca-0)))))
  (label 76)
  (parent 65)
  (unrealized (6 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y y-0 expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y-0)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (defstrand resp 1 (b a) (y y-0))
  (deflistener (exp (gen) (mul y y-0)))
  (deflistener (cat (gen) (mul y y-0)))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (0 2))
    ((3 0) (2 0)) ((3 0) (5 0)) ((4 1) (0 4)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen y y-0)
  (uniq-orig n)
  (precur (5 0))
  (operation nonce-test (contracted (y-1 y) (y-2 y-0) (w (mul y y-0)))
    (gen) (5 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (recv (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((send (enc "reg" (exp (gen) y-0) a (privk a))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0))))
    ((recv (cat (gen) (mul y y-0))) (send (cat (gen) (mul y y-0)))))
  (label 77)
  (parent 66)
  (unrealized (4 0) (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y y-0 expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (y y-0))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y-0)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y)))
  (defstrand resp 1 (b a) (y y))
  (deflistener (exp (gen) (mul y y-0)))
  (deflistener (cat (exp (gen) y-0) y))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (0 2))
    ((3 0) (2 0)) ((3 0) (5 0)) ((4 1) (0 4)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (precur (5 0))
  (uniq-gen y y-0)
  (uniq-orig n)
  (operation nonce-test (displaced 6 0 resp 1) (exp (gen) y-1) (5 0))
  (traces
    ((send (enc "reg" (exp (gen) y-0) b (privk b)))
      (recv (enc (exp (gen) y-0) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) a (privk ca))))
      (send
        (cat (exp (gen) y-0) (enc (exp (gen) y-0) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (recv (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y-0) b (privk b)))
      (send (enc (exp (gen) y-0) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y) a (privk a)))
      (send (enc (exp (gen) y) a (privk ca))))
    ((send (enc "reg" (exp (gen) y) a (privk a))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0))))
    ((recv (cat (exp (gen) y-0) y)) (send (cat (exp (gen) y-0) y))))
  (label 78)
  (parent 66)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y y-0 expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y-0)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (defstrand resp 1 (b a) (y y-0))
  (deflistener (exp (gen) (mul y y-0)))
  (deflistener (cat (exp (gen) y-0) y))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (0 2))
    ((3 0) (2 0)) ((3 0) (5 0)) ((4 1) (0 4)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (precur (5 0))
  (uniq-gen y y-0)
  (uniq-orig n)
  (operation nonce-test (displaced 6 3 resp 1) (exp (gen) y-1) (5 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (recv (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((send (enc "reg" (exp (gen) y-0) a (privk a))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0))))
    ((recv (cat (exp (gen) y-0) y)) (send (cat (exp (gen) y-0) y))))
  (label 79)
  (parent 66)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca b-0 name) (y y-0 y-1 expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y-0)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (defstrand resp 1 (b a) (y y-0))
  (deflistener (exp (gen) (mul y y-0)))
  (deflistener (cat (exp (gen) y-1) (mul y y-0 (rec y-1))))
  (defstrand resp 1 (b b-0) (y y-1))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (0 2))
    ((3 0) (2 0)) ((3 0) (5 0)) ((4 1) (0 4)) ((5 1) (4 0))
    ((6 0) (5 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (precur (5 0))
  (uniq-gen y y-0 y-1)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 1) (exp (gen) y-1) (5 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (recv (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((send (enc "reg" (exp (gen) y-0) a (privk a))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0))))
    ((recv (cat (exp (gen) y-1) (mul y y-0 (rec y-1))))
      (send (cat (exp (gen) y-1) (mul y y-0 (rec y-1)))))
    ((send (enc "reg" (exp (gen) y-1) b-0 (privk b-0)))))
  (label 80)
  (parent 66)
  (unrealized (4 0) (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (b ca name) (y expn))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (h (exp (gen) y)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (deflistener (exp (gen) (mul y y)))
  (deflistener (cat (gen) (mul y y)))
  (deflistener y)
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (0 2)) ((3 1) (0 4)) ((4 1) (3 0)) ((5 1) (4 0)))
  (non-orig (privk b) (privk ca))
  (uniq-gen y)
  (uniq-orig n)
  (precur (4 0))
  (operation nonce-test (added-listener y) (mul y y) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y)))))
      (recv (enc "check" n (exp (gen) (mul y y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (exp (gen) (mul y y))) (send (exp (gen) (mul y y))))
    ((recv (cat (gen) (mul y y))) (send (cat (gen) (mul y y))))
    ((recv y) (send y)))
  (label 81)
  (parent 69)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (b ca a name) (x y expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((0 3) (3 3)) ((1 1) (0 1))
    ((2 1) (0 2)) ((2 1) (3 1)) ((3 0) (2 0)) ((3 4) (0 4))
    ((4 1) (3 3)))
  (non-orig (privk b) (privk ca) (privk a))
  (uniq-gen x y)
  (uniq-orig n)
  (operation encryption-test (displaced 5 0 resp 1)
    (enc "reg" (exp (gen) y) b-0 (privk b-0)) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca)))))
  (label 82)
  (parent 73)
  (seen 72)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a ca-0 name) (x y expn))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand init 5 (n n) (a a) (b b) (ca ca-0) (h (exp (gen) y)) (x x))
  (defstrand ca 2 (subject a) (ca ca-0) (h (exp (gen) x)))
  (defstrand ca 2 (subject b) (ca ca-0) (h (exp (gen) y)))
  (precedes ((0 0) (1 0)) ((0 0) (5 0)) ((0 3) (3 3)) ((1 1) (0 1))
    ((2 1) (0 2)) ((3 0) (2 0)) ((3 0) (4 0)) ((3 4) (0 4))
    ((4 1) (3 1)) ((5 1) (3 3)))
  (non-orig (privk b) (privk ca) (privk a) (privk ca-0))
  (uniq-gen x y)
  (uniq-orig n)
  (operation encryption-test (displaced 6 0 resp 1)
    (enc "reg" (exp (gen) y) b-0 (privk b-0)) (5 0))
  (traces
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca-0)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca-0))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca-0))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca-0))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca-0)))))
  (label 83)
  (parent 75)
  (unrealized)
  (shape)
  (maps ((0) ((n n) (y y) (a a) (b b) (ca ca) (h (exp (gen) x)))))
  (origs (n (0 3))))

(comment "Nothing left to do")

(defprotocol dhca diffie-hellman
  (defrole init
    (vars (x expn) (a b ca name) (h base) (n text))
    (trace (send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv (cat h (enc h b (privk ca)) (enc n (exp h x))))
      (send (enc "check" n (exp h x))))
    (non-orig (privk ca))
    (uniq-gen x))
  (defrole resp
    (vars (y expn) (a b ca name) (h base) (n text))
    (trace (send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat h (enc h a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp h y)))) (recv (enc "check" n (exp h y))))
    (non-orig (privk ca))
    (uniq-gen y))
  (defrole ca
    (vars (subject ca name) (h base))
    (trace (recv (enc "reg" h subject (privk subject)))
      (send (enc h subject (privk ca))))
    (non-orig (privk subject)))
  (comment A diffie-hellman exchange which uses a certificate authority
    to certify long-term DH values))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (non-orig (privk ca))
  (uniq-gen x y)
  (uniq-orig n)
  (comment point of view in which init and resp each complete and they
    agree on the relevant parameters)
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y))))))
  (label 84)
  (unrealized (0 1) (0 3) (1 1) (1 2) (1 4))
  (preskeleton)
  (comment "Not a skeleton"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (precedes ((0 0) (1 2)) ((1 3) (0 3)))
  (non-orig (privk ca))
  (uniq-gen x y)
  (uniq-orig n)
  (comment point of view in which init and resp each complete and they
    agree on the relevant parameters)
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y))))))
  (label 85)
  (parent 84)
  (unrealized (0 1) (1 1) (1 2) (1 4))
  (origs (n (1 3)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (precedes ((0 0) (1 2)) ((1 0) (2 0)) ((1 3) (0 3)) ((2 1) (1 1)))
  (non-orig (privk b) (privk ca))
  (uniq-gen x y)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) y) b (privk ca)) (1 1))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca)))))
  (label 86)
  (parent 85)
  (unrealized (0 1) (1 2) (1 4))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((1 3) (0 3)) ((2 1) (1 1))
    ((3 1) (1 2)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen x y)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) x) a (privk ca)) (1 2))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca)))))
  (label 87)
  (parent 86)
  (unrealized (0 1) (1 4))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y x expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (precedes ((0 0) (3 0)) ((0 4) (1 4)) ((1 0) (2 0)) ((1 3) (0 3))
    ((2 1) (1 1)) ((3 1) (1 2)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (displaced 4 0 init 5)
    (enc "check" n (exp (gen) (mul x-0 y))) (1 4))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (send (enc "check" n (exp (gen) (mul y x)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (recv (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca)))))
  (label 88)
  (parent 87)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca a-0 b-0 ca-0 name) (x y x-0 expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand init 5 (n n) (a a-0) (b b-0) (ca ca-0)
    (h (exp (gen) (mul x y (rec x-0)))) (x x-0))
  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((1 3) (0 3)) ((1 3) (4 3))
    ((2 1) (1 1)) ((3 1) (1 2)) ((4 4) (1 4)))
  (non-orig (privk a) (privk b) (privk ca) (privk ca-0))
  (uniq-gen x y x-0)
  (uniq-orig n)
  (operation encryption-test (added-strand init 5)
    (enc "check" n (exp (gen) (mul x y))) (1 4))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) x-0) a-0 (privk a-0)))
      (recv (enc (exp (gen) x-0) a-0 (privk ca-0)))
      (send
        (cat (exp (gen) x-0) (enc (exp (gen) x-0) a-0 (privk ca-0))))
      (recv
        (cat (exp (gen) (mul x y (rec x-0)))
          (enc (exp (gen) (mul x y (rec x-0))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y))))))
  (label 89)
  (parent 87)
  (unrealized (0 1) (4 1) (4 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (deflistener (exp (gen) (mul x y)))
  (precedes ((0 0) (3 0)) ((0 0) (4 0)) ((1 0) (2 0)) ((1 0) (4 0))
    ((1 3) (0 3)) ((2 1) (1 1)) ((3 1) (1 2)) ((4 1) (1 4)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen x y)
  (uniq-orig n)
  (operation encryption-test (added-listener (exp (gen) (mul x y)))
    (enc "check" n (exp (gen) (mul x y))) (1 4))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y)))))
  (label 90)
  (parent 87)
  (unrealized (0 1) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y x expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (precedes ((0 0) (3 0)) ((0 4) (1 4)) ((1 0) (2 0)) ((1 3) (0 3))
    ((2 1) (1 1)) ((3 1) (0 1)) ((3 1) (1 2)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (displaced 4 3 ca 2)
    (enc (exp (gen) x) a (privk ca)) (0 1))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (send (enc "check" n (exp (gen) (mul y x)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (recv (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca)))))
  (label 91)
  (parent 88)
  (unrealized)
  (shape)
  (maps ((0 1) ((a a) (b b) (ca ca) (x x) (y y) (n n))))
  (origs (n (1 3))))

(defskeleton dhca
  (vars (n text) (a b ca name) (y x expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (precedes ((0 0) (3 0)) ((0 0) (4 0)) ((0 4) (1 4)) ((1 0) (2 0))
    ((1 3) (0 3)) ((2 1) (1 1)) ((3 1) (1 2)) ((4 1) (0 1)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen y x)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) x) a (privk ca)) (0 1))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (send (enc "check" n (exp (gen) (mul y x)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y x)))))
      (recv (enc "check" n (exp (gen) (mul y x)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca)))))
  (label 92)
  (parent 88)
  (unrealized)
  (shape)
  (maps ((0 1) ((a a) (b b) (ca ca) (x x) (y y) (n n))))
  (origs (n (1 3))))

(defskeleton dhca
  (vars (n text) (a b ca a-0 b-0 ca-0 name) (x y x-0 expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand init 5 (n n) (a a-0) (b b-0) (ca ca-0)
    (h (exp (gen) (mul x y (rec x-0)))) (x x-0))
  (defstrand ca 2 (subject a-0) (ca ca-0) (h (exp (gen) x-0)))
  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((1 3) (0 3)) ((1 3) (4 3))
    ((2 1) (1 1)) ((3 1) (1 2)) ((4 0) (5 0)) ((4 4) (1 4))
    ((5 1) (4 1)))
  (non-orig (privk a) (privk b) (privk ca) (privk a-0) (privk ca-0))
  (uniq-gen x y x-0)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) x-0) a-0 (privk ca-0)) (4 1))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) x-0) a-0 (privk a-0)))
      (recv (enc (exp (gen) x-0) a-0 (privk ca-0)))
      (send
        (cat (exp (gen) x-0) (enc (exp (gen) x-0) a-0 (privk ca-0))))
      (recv
        (cat (exp (gen) (mul x y (rec x-0)))
          (enc (exp (gen) (mul x y (rec x-0))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x-0) a-0 (privk a-0)))
      (send (enc (exp (gen) x-0) a-0 (privk ca-0)))))
  (label 93)
  (parent 89)
  (unrealized (0 1) (4 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn) (w expr))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) (mul x y (rec w))) w))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 0) (2 0)) ((1 0) (5 0))
    ((1 3) (0 3)) ((2 1) (1 1)) ((3 1) (1 2)) ((4 1) (1 4))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen x y)
  (uniq-orig n)
  (precur (5 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x y (rec w))) w))
    (exp (gen) (mul x y)) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) (mul x y (rec w))) w))
      (send (cat (exp (gen) (mul x y (rec w))) w))))
  (label 94)
  (parent 90)
  (unrealized (0 1) (5 0))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca a-0 b-0 ca-0 name) (x y x-0 expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (defstrand init 5 (n n) (a a-0) (b b-0) (ca ca-0)
    (h (exp (gen) (mul x y (rec x-0)))) (x x-0))
  (defstrand ca 2 (subject a-0) (ca ca-0) (h (exp (gen) x-0)))
  (defstrand ca 2 (subject b-0) (ca ca-0)
    (h (exp (gen) (mul x y (rec x-0)))))
  (precedes ((0 0) (3 0)) ((0 0) (6 0)) ((1 0) (2 0)) ((1 0) (6 0))
    ((1 3) (0 3)) ((1 3) (4 3)) ((2 1) (1 1)) ((3 1) (1 2))
    ((4 0) (5 0)) ((4 0) (6 0)) ((4 4) (1 4)) ((5 1) (4 1))
    ((6 1) (4 3)))
  (non-orig (privk a) (privk b) (privk ca) (privk a-0) (privk b-0)
    (privk ca-0))
  (uniq-gen x y x-0)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) (mul x y (rec x-0))) b-0 (privk ca-0)) (4 3))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((send (enc "reg" (exp (gen) x-0) a-0 (privk a-0)))
      (recv (enc (exp (gen) x-0) a-0 (privk ca-0)))
      (send
        (cat (exp (gen) x-0) (enc (exp (gen) x-0) a-0 (privk ca-0))))
      (recv
        (cat (exp (gen) (mul x y (rec x-0)))
          (enc (exp (gen) (mul x y (rec x-0))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) x-0) a-0 (privk a-0)))
      (send (enc (exp (gen) x-0) a-0 (privk ca-0))))
    ((recv (enc "reg" (exp (gen) (mul x y (rec x-0))) b-0 (privk b-0)))
      (send (enc (exp (gen) (mul x y (rec x-0))) b-0 (privk ca-0)))))
  (label 95)
  (parent 93)
  (unrealized (0 1) (6 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (gen) (mul x y)))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 0) (2 0)) ((1 0) (5 0))
    ((1 3) (0 3)) ((2 1) (1 1)) ((3 1) (1 2)) ((4 1) (1 4))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen x y)
  (uniq-orig n)
  (precur (5 0))
  (operation nonce-test (contracted (x-0 x) (y-0 y) (w (mul x y))) (gen)
    (5 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (gen) (mul x y))) (send (cat (gen) (mul x y)))))
  (label 96)
  (parent 94)
  (unrealized (0 1) (4 0) (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y y-0 expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x y-0))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y-0)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) y-0)))
  (deflistener (exp (gen) (mul y y-0)))
  (deflistener (cat (exp (gen) y-0) y))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 0) (2 0)) ((1 0) (5 0))
    ((1 3) (0 3)) ((2 1) (1 1)) ((3 1) (1 2)) ((4 1) (1 4))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (precur (5 0))
  (uniq-gen y y-0)
  (uniq-orig n)
  (operation nonce-test (displaced 6 0 resp 1) (exp (gen) y-1) (5 0))
  (traces
    ((send (enc "reg" (exp (gen) y-0) a (privk a)))
      (recv (enc (exp (gen) y-0) a (privk ca)))
      (send (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (send (enc "check" n (exp (gen) (mul y y-0)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) y-0) (enc (exp (gen) y-0) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul y y-0)))))
      (recv (enc "check" n (exp (gen) (mul y y-0)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) y-0) a (privk a)))
      (send (enc (exp (gen) y-0) a (privk ca))))
    ((recv (exp (gen) (mul y y-0))) (send (exp (gen) (mul y y-0))))
    ((recv (cat (exp (gen) y-0) y)) (send (cat (exp (gen) y-0) y))))
  (label 97)
  (parent 94)
  (unrealized (0 1) (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 0) (2 0)) ((1 0) (5 0))
    ((1 3) (0 3)) ((2 1) (1 1)) ((3 1) (1 2)) ((4 1) (1 4))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (precur (5 0))
  (uniq-gen x y)
  (uniq-orig n)
  (operation nonce-test (displaced 6 1 resp 1) (exp (gen) y-0) (5 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x))))
  (label 98)
  (parent 94)
  (unrealized (0 1) (5 0))
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca b-0 name) (x y y-0 expn))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) y)) (x x))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (h (exp (gen) x)) (y y))
  (defstrand ca 2 (subject b) (ca ca) (h (exp (gen) y)))
  (defstrand ca 2 (subject a) (ca ca) (h (exp (gen) x)))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y-0) (mul x y (rec y-0))))
  (defstrand resp 1 (b b-0) (y y-0))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 0) (2 0)) ((1 0) (5 0))
    ((1 3) (0 3)) ((2 1) (1 1)) ((3 1) (1 2)) ((4 1) (1 4))
    ((5 1) (4 0)) ((6 0) (5 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (precur (5 0))
  (uniq-gen x y y-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 1) (exp (gen) y-0) (5 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y)))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca))))
    ((recv (enc "reg" (exp (gen) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) y-0) (mul x y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul x y (rec y-0)))))
    ((send (enc "reg" (exp (gen) y-0) b-0 (privk b-0)))))
  (label 99)
  (parent 94)
  (unrealized (0 1) (4 0) (5 0))
  (comment "empty cohort"))

(comment "Nothing left to do")