(herald dhca (algebra diffie-hellman))

(comment "CPSA 3.6.8")
(comment "All input read from tst/dh-ca.scm")

(defprotocol dhca diffie-hellman
  (defrole init
    (vars (x rndx) (a b ca name) (y expt) (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 (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)))))
    (non-orig (privk ca))
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (a b ca name) (x expt) (n text))
    (trace (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)))))
    (non-orig (privk ca))
    (uniq-gen y))
  (defrole ca
    (vars (subject ca name) (x expt))
    (trace (recv (enc "reg" (exp (gen) x) subject (privk subject)))
      (send (enc (exp (gen) x) 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 rndx) (y expt))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (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 (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))))))
  (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) (y expt) (x rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand ca 2 (subject a) (ca ca) (x 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 (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 1)
  (parent 0)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defskeleton dhca
  (vars (n text) (a ca a-0 b ca-0 name) (y y-0 rndx))
  (defstrand init 5 (n n) (a a) (b a) (ca ca) (x y) (y y))
  (defstrand ca 2 (subject a) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x y))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca-0) (y y-0)
    (x (mul y y (rec y-0))))
  (defstrand ca 2 (subject b) (ca ca-0) (x y-0))
  (defstrand ca 2 (subject a-0) (ca ca-0) (x (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 27)
  (parent 19)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

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

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

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

(defskeleton dhca
  (vars (n text) (a ca b name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand resp 4 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (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 y x)
  (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 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))))
    ((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 y x)))))))
  (label 31)
  (parent 21)
  (unrealized)
  (shape)
  (maps ((0) ((x x) (a a) (b b) (ca ca) (y y) (n n))))
  (origs))

(defskeleton dhca
  (vars (n text) (a ca a-0 b name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject a-0) (ca ca) (x 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 y x)
  (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 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))))
    ((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 y x))))))
    ((recv (enc "reg" (exp (gen) x) a-0 (privk a-0)))
      (send (enc (exp (gen) x) a-0 (privk ca)))))
  (label 32)
  (parent 21)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca b name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand resp 4 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x 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 y x)
  (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 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))))
    ((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 y x))))))
    ((recv (enc "reg" (exp (gen) y) b (privk b)))
      (send (enc (exp (gen) y) b (privk ca)))))
  (label 33)
  (parent 22)
  (seen 31)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dhca
  (vars (n text) (a ca a-0 b ca-0 name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand resp 4 (n n) (a a-0) (b b) (ca ca-0) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca-0) (x y))
  (defstrand ca 2 (subject a-0) (ca ca-0) (x 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 y x)
  (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 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))))
    ((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 y x))))))
    ((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 34)
  (parent 22)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca a-0 b-0 ca-0 name) (x y y-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand resp 1 (b b) (y y))
  (defstrand resp 4 (n n) (a a-0) (b b-0) (ca ca-0) (y y-0)
    (x (mul x y (rec y-0))))
  (defstrand ca 2 (subject b-0) (ca ca-0) (x y-0))
  (defstrand ca 2 (subject a-0) (ca ca-0) (x (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 35)
  (parent 23)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

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

(defskeleton dhca
  (vars (n text) (a ca b name) (y y-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x y-0) (y y))
  (defstrand ca 2 (subject a) (ca ca) (x y-0))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand resp 4 (n n) (a a) (b b) (ca ca) (y y) (x y-0))
  (defstrand ca 2 (subject a) (ca ca) (x 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 37)
  (parent 32)
  (unrealized)
  (shape)
  (maps ((0) ((x y-0) (a a) (b b) (ca ca) (y y) (n n))))
  (origs))

(defskeleton dhca
  (vars (n text) (a ca b ca-0 name) (y y-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x y-0) (y y))
  (defstrand ca 2 (subject a) (ca ca) (x y-0))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand resp 4 (n n) (a a) (b b) (ca ca-0) (y y) (x y-0))
  (defstrand ca 2 (subject b) (ca ca-0) (x y))
  (defstrand ca 2 (subject a) (ca ca-0) (x 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 38)
  (parent 34)
  (unrealized)
  (shape)
  (maps ((0) ((x y-0) (a a) (b b) (ca ca) (y y) (n n))))
  (origs))

(comment "Nothing left to do")

(defprotocol dhca diffie-hellman
  (defrole init
    (vars (x rndx) (a b ca name) (y expt) (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 (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)))))
    (non-orig (privk ca))
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (a b ca name) (x expt) (n text))
    (trace (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)))))
    (non-orig (privk ca))
    (uniq-gen y))
  (defrole ca
    (vars (subject ca name) (x expt))
    (trace (recv (enc "reg" (exp (gen) x) subject (privk subject)))
      (send (enc (exp (gen) x) 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) (y rndx) (x expt))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (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 (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))))))
  (label 39)
  (unrealized (0 1) (0 2))
  (origs (n (0 3)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x expt) (y rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x 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 (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 40)
  (parent 39)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y rndx))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (y y) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x 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 (exp (gen) x) 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 41)
  (parent 40)
  (unrealized (0 4))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y rndx) (x expt))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (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 (exp (gen) x) 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) 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 42)
  (parent 40)
  (unrealized (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 rndx))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (y y) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0) (x x)
    (y (mul y y (rec 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 43)
  (parent 41)
  (unrealized (2 1) (2 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y rndx))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (y y) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x 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 44)
  (parent 41)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y rndx))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (y y) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x 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 45)
  (parent 42)
  (unrealized (0 4))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y y-0 rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x y-0))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x 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 46)
  (parent 42)
  (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 rndx))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (y y) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0) (x x)
    (y (mul y y (rec x))))
  (defstrand ca 2 (subject a) (ca ca-0) (x 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 47)
  (parent 43)
  (unrealized (2 3))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x rndx))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (y y) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0) (x x)
    (y (mul y y (rec 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 49)
  (parent 45)
  (unrealized (3 1) (3 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca name) (y rndx))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (y y) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x 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 50)
  (parent 45)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0) (x x) (y y))
  (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 51)
  (parent 46)
  (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 rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x y-0))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x y-0))
  (defstrand resp 1 (b a) (y y-0))
  (defstrand init 5 (n n) (a a-0) (b b-0) (ca ca-0) (x x)
    (y (mul y y-0 (rec 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 52)
  (parent 46)
  (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 rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x y-0))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x 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 53)
  (parent 46)
  (unrealized (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x rndx))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (y y) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0) (x x)
    (y (mul y y (rec x))))
  (defstrand ca 2 (subject a) (ca ca-0) (x x))
  (defstrand ca 2 (subject b-0) (ca ca-0) (x (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 54)
  (parent 47)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

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

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

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

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x rndx))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (y y) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0) (x x)
    (y (mul y y (rec x))))
  (defstrand ca 2 (subject a) (ca ca-0) (x 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 58)
  (parent 49)
  (unrealized (3 3))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton dhca
  (vars (n text) (b ca a b-0 name) (y x rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca) (x x) (y y))
  (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 60)
  (parent 51)
  (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 rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0) (x x) (y y))
  (defstrand ca 2 (subject a) (ca ca-0) (x 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 61)
  (parent 51)
  (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 rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x y-0))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x y-0))
  (defstrand resp 1 (b a) (y y-0))
  (defstrand init 5 (n n) (a a-0) (b b-0) (ca ca-0) (x x)
    (y (mul y y-0 (rec x))))
  (defstrand ca 2 (subject a-0) (ca ca-0) (x 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 62)
  (parent 52)
  (unrealized (4 3))
  (comment "1 in cohort - 1 not yet seen"))

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

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

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

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (y x rndx))
  (defstrand resp 5 (n n) (a b) (b b) (ca ca) (y y) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0) (x x)
    (y (mul y y (rec x))))
  (defstrand ca 2 (subject a) (ca ca-0) (x x))
  (defstrand ca 2 (subject b-0) (ca ca-0) (x (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 66)
  (parent 58)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

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

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

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

(defskeleton dhca
  (vars (n text) (b ca a name) (x y rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (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 x y)
  (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 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))))))
  (label 70)
  (parent 60)
  (unrealized)
  (shape)
  (maps ((0) ((n n) (y y) (a a) (b b) (ca ca) (x x))))
  (origs (n (0 3))))

(defskeleton dhca
  (vars (n text) (b ca a b-0 name) (x y rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca) (x x) (y y))
  (defstrand ca 2 (subject b-0) (ca ca) (x 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 x y)
  (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 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-0 (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-0 (privk b-0)))
      (send (enc (exp (gen) y) b-0 (privk ca)))))
  (label 71)
  (parent 60)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a name) (x y rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand ca 2 (subject a) (ca ca) (x 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 x y)
  (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 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) x) a (privk a)))
      (send (enc (exp (gen) x) a (privk ca)))))
  (label 72)
  (parent 61)
  (unrealized)
  (shape)
  (maps ((0) ((n n) (y y) (a a) (b b) (ca ca) (x x))))
  (origs (n (0 3))))

(defskeleton dhca
  (vars (n text) (b ca a b-0 ca-0 name) (x y rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand init 5 (n n) (a a) (b b-0) (ca ca-0) (x x) (y y))
  (defstrand ca 2 (subject a) (ca ca-0) (x x))
  (defstrand ca 2 (subject b-0) (ca ca-0) (x 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 x y)
  (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 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-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) 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 73)
  (parent 61)
  (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 rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x y-0))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x y-0))
  (defstrand resp 1 (b a) (y y-0))
  (defstrand init 5 (n n) (a a-0) (b b-0) (ca ca-0) (x x)
    (y (mul y y-0 (rec x))))
  (defstrand ca 2 (subject a-0) (ca ca-0) (x x))
  (defstrand ca 2 (subject b-0) (ca ca-0) (x (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 74)
  (parent 62)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

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

(defskeleton dhca
  (vars (n text) (b ca a name) (x y rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand ca 2 (subject b) (ca ca) (x 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 76)
  (parent 71)
  (seen 70)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dhca
  (vars (n text) (b ca a ca-0 name) (x y rndx))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand init 5 (n n) (a a) (b b) (ca ca-0) (x x) (y y))
  (defstrand ca 2 (subject a) (ca ca-0) (x x))
  (defstrand ca 2 (subject b) (ca ca-0) (x 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 77)
  (parent 73)
  (unrealized)
  (shape)
  (maps ((0) ((n n) (y y) (a a) (b b) (ca ca) (x x))))
  (origs (n (0 3))))

(comment "Nothing left to do")

(defprotocol dhca diffie-hellman
  (defrole init
    (vars (x rndx) (a b ca name) (y expt) (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 (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)))))
    (non-orig (privk ca))
    (uniq-gen x))
  (defrole resp
    (vars (y rndx) (a b ca name) (x expt) (n text))
    (trace (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)))))
    (non-orig (privk ca))
    (uniq-gen y))
  (defrole ca
    (vars (subject ca name) (x expt))
    (trace (recv (enc "reg" (exp (gen) x) subject (privk subject)))
      (send (enc (exp (gen) x) 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 rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (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 78)
  (unrealized (0 1) (0 3) (1 1) (1 2) (1 4))
  (preskeleton)
  (origs (n (1 3)))
  (comment "Not a skeleton"))

(defskeleton dhca
  (vars (n text) (a b ca name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (precedes ((0 0) (1 2)) ((1 3) (0 3)))
  (non-orig (privk ca))
  (uniq-gen x y)
  (uniq-orig n)
  (comment point of view in which init and resp each complete and they
    agree on the relevant parameters)
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (send (enc "check" n (exp (gen) (mul x y)))))
    ((send (enc "reg" (exp (gen) y) b (privk b)))
      (recv (enc (exp (gen) y) b (privk ca)))
      (recv (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (send
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul x y)))))
      (recv (enc "check" n (exp (gen) (mul x y))))))
  (label 79)
  (parent 78)
  (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 rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x 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 80)
  (parent 79)
  (unrealized (0 1) (1 2) (1 4))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x 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 y x)
  (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 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 81)
  (parent 80)
  (unrealized (0 1) (1 4))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x 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 y x-0))) (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 82)
  (parent 81)
  (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) (y x x-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-0) (ca ca-0) (x x-0)
    (y (mul y x (rec 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 y x x-0)
  (uniq-orig n)
  (operation encryption-test (added-strand init 5)
    (enc "check" n (exp (gen) (mul y x))) (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))))
    ((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 y x (rec x-0)))
          (enc (exp (gen) (mul y x (rec x-0))) b-0 (privk ca-0))
          (enc n (exp (gen) (mul y x)))))
      (send (enc "check" n (exp (gen) (mul y x))))))
  (label 83)
  (parent 81)
  (unrealized (0 1) (4 1) (4 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (deflistener (exp (gen) (mul y x)))
  (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 y x)
  (uniq-orig n)
  (operation encryption-test (added-listener (exp (gen) (mul y x)))
    (enc "check" n (exp (gen) (mul y x))) (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))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x)))))
  (label 84)
  (parent 81)
  (unrealized (0 1) (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x 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 85)
  (parent 82)
  (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 rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand ca 2 (subject a) (ca ca) (x 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 86)
  (parent 82)
  (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) (y x x-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-0) (ca ca-0) (x x-0)
    (y (mul y x (rec x-0))))
  (defstrand ca 2 (subject a-0) (ca ca-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 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 y x 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 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))))
    ((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 y x (rec x-0)))
          (enc (exp (gen) (mul y x (rec x-0))) 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-0) a-0 (privk a-0)))
      (send (enc (exp (gen) x-0) a-0 (privk ca-0)))))
  (label 87)
  (parent 83)
  (unrealized (0 1) (4 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 0) (2 0)) ((1 0) (5 0))
    ((1 3) (0 3)) ((2 1) (1 1)) ((3 1) (1 2)) ((4 1) (1 4))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (exp (gen) (mul y x)) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul 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 (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) y) x)) (send (cat (exp (gen) y) x))))
  (label 88)
  (parent 84)
  (unrealized (0 1) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 0) (2 0)) ((1 0) (5 0))
    ((1 3) (0 3)) ((2 1) (1 1)) ((3 1) (1 2)) ((4 1) (1 4))
    ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk ca))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (exp (gen) (mul y x)) (4 0))
  (traces
    ((send (enc "reg" (exp (gen) x) a (privk a)))
      (recv (enc (exp (gen) x) a (privk ca)))
      (send (cat (exp (gen) x) (enc (exp (gen) x) a (privk ca))))
      (recv
        (cat (exp (gen) y) (enc (exp (gen) y) b (privk ca))
          (enc n (exp (gen) (mul 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 (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) x) y)) (send (cat (exp (gen) x) y))))
  (label 89)
  (parent 84)
  (unrealized (0 1) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhca
  (vars (n text) (a b ca a-0 b-0 ca-0 name) (y x x-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (ca ca) (x x) (y y))
  (defstrand resp 5 (n n) (a a) (b b) (ca ca) (y y) (x x))
  (defstrand ca 2 (subject b) (ca ca) (x y))
  (defstrand ca 2 (subject a) (ca ca) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-0) (ca ca-0) (x x-0)
    (y (mul y x (rec x-0))))
  (defstrand ca 2 (subject a-0) (ca ca-0) (x x-0))
  (defstrand ca 2 (subject b-0) (ca ca-0) (x (mul y x (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 y x x-0)
  (uniq-orig n)
  (operation encryption-test (added-strand ca 2)
    (enc (exp (gen) (mul y x (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 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))))
    ((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 y x (rec x-0)))
          (enc (exp (gen) (mul y x (rec x-0))) 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-0) a-0 (privk a-0)))
      (send (enc (exp (gen) x-0) a-0 (privk ca-0))))
    ((recv (enc "reg" (exp (gen) (mul y x (rec x-0))) b-0 (privk b-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) b-0 (privk ca-0)))))
  (label 90)
  (parent 87)
  (unrealized (0 1) (6 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")