(herald dhca (algebra diffie-hellman))

(comment "CPSA 3.2.2")
(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 "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)))
  (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 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 9)
  (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 10)
  (parent 6)
  (unrealized (3 0))
  (comment "empty cohort"))

(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 11)
  (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 12)
  (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 13)
  (parent 7)
  (unrealized (4 0))
  (comment "empty cohort"))

(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 14)
  (parent 8)
  (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)))
  (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 15)
  (parent 9)
  (unrealized (3 2))
  (comment "1 in cohort - 1 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 16)
  (parent 11)
  (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 17)
  (parent 11)
  (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 18)
  (parent 12)
  (unrealized (4 2))
  (comment "1 in cohort - 1 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))
  (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 19)
  (parent 15)
  (unrealized (5 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 20)
  (parent 16)
  (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 21)
  (parent 16)
  (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 22)
  (parent 17)
  (seen 20)
  (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 23)
  (parent 17)
  (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 24)
  (parent 18)
  (unrealized (6 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 25)
  (parent 21)
  (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 26)
  (parent 23)
  (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 27)
  (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 28)
  (parent 27)
  (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 29)
  (parent 28)
  (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 30)
  (parent 28)
  (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 31)
  (parent 29)
  (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 32)
  (parent 29)
  (unrealized (2 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)))
  (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 33)
  (parent 30)
  (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 34)
  (parent 30)
  (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 35)
  (parent 31)
  (unrealized (2 3))
  (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 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 36)
  (parent 33)
  (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 37)
  (parent 33)
  (unrealized (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 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 38)
  (parent 34)
  (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 39)
  (parent 34)
  (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 40)
  (parent 34)
  (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 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 41)
  (parent 35)
  (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)))
  (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 42)
  (parent 36)
  (unrealized (3 3))
  (comment "1 in cohort - 1 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 43)
  (parent 38)
  (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 44)
  (parent 38)
  (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 45)
  (parent 39)
  (unrealized (4 3))
  (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 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 46)
  (parent 42)
  (unrealized (5 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 47)
  (parent 43)
  (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 48)
  (parent 43)
  (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 49)
  (parent 44)
  (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 50)
  (parent 44)
  (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 51)
  (parent 45)
  (unrealized (6 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 52)
  (parent 48)
  (seen 47)
  (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 53)
  (parent 50)
  (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 54)
  (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)
  (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 55)
  (parent 54)
  (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 56)
  (parent 55)
  (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 57)
  (parent 56)
  (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 58)
  (parent 57)
  (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 59)
  (parent 57)
  (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 60)
  (parent 57)
  (unrealized (0 1) (4 0))
  (comment "empty cohort"))

(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 61)
  (parent 58)
  (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 62)
  (parent 58)
  (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 63)
  (parent 59)
  (unrealized (0 1) (4 3))
  (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 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 64)
  (parent 63)
  (unrealized (0 1) (6 0))
  (comment "empty cohort"))

(comment "Nothing left to do")