(herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol"
  (algebra diffie-hellman))

(comment "CPSA 3.6.0")
(comment "All input read from dhnsl_use.scm")

(defprotocol dhnsl diffie-hellman
  (defrole resp
    (vars (b a name) (x expt) (y rndx) (n text))
    (trace (recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    (uniq-orig n)
    (uniq-gen y)
    (absent (y (exp (gen) x)))
    (comment "Y should be assumed to be freshly chosen per role"))
  (defrole init
    (vars (a b name) (y expt) (x rndx) (n text))
    (trace (send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    (uniq-gen x)
    (comment "X should be assumed to be freshly chosen per role"))
  (comment
    "Needham-Schroeder-Lowe DH challenge/responses in place of nonces"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y expt) (x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (comment "Initiator point-of-view")
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n)))
  (label 0)
  (unrealized (0 1) (0 3))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y expt) (y-0 x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y-0 x)
  (operation nonce-test (added-strand resp 2) (exp (gen) x) (0 1)
    (enc (exp (gen) x) a (pubk b)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) b (pubk a)))))
  (label 1)
  (parent 0)
  (unrealized (0 1) (0 3))
  (comment "2 in cohort - 2 not yet seen"))

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

(defskeleton dhnsl
  (vars (n text) (a b name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation nonce-test (contracted (y-0 y) (y-1 y)) (exp (gen) x) (0 1)
    (enc (exp (gen) x) a (pubk b))
    (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))))
  (label 3)
  (parent 1)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

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

(defskeleton dhnsl
  (vars (n text) (a b name) (y expt) (x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (deflistener (cat (gen) x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (precur (1 0))
  (operation nonce-test (contracted (x-0 x) (w x)) (gen) (1 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (gen) x)) (send (cat (gen) x))))
  (label 5)
  (parent 2)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b b-0 a-0 name) (y x expt) (x-0 y-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x-0))
  (deflistener (cat (exp (gen) y-0) (mul x-0 (rec y-0))))
  (defstrand resp 2 (b b-0) (a a-0) (x x) (y y-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen x-0 y-0)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (1 0))
  (traces
    ((send (enc (exp (gen) x-0) a (pubk b)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) y-0) (mul x-0 (rec y-0))))
      (send (cat (exp (gen) y-0) (mul x-0 (rec y-0)))))
    ((recv (enc (exp (gen) x) a-0 (pubk b-0)))
      (send (enc (exp (gen) x) (exp (gen) y-0) b-0 (pubk a-0)))))
  (label 6)
  (parent 2)
  (unrealized (0 1) (0 3) (1 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y expt) (x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (deflistener (cat (exp (gen) x) (one)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen x)
  (operation nonce-test (displaced 2 0 init 1) (exp (gen) x-0) (1 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one)))))
  (label 7)
  (parent 2)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 name) (y expt) (x x-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0))))
  (defstrand init 1 (a a-0) (b b-0) (x x-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 0) (1 0)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (1 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0))))
      (send (cat (exp (gen) x-0) (mul x (rec x-0)))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))))
  (label 8)
  (parent 2)
  (unrealized (0 1) (0 3) (1 0))
  (comment "empty cohort"))

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

(defskeleton dhnsl
  (vars (n text) (a b name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y))
  (deflistener (exp (gen) (mul x y)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (2 0)) ((2 1) (0 3)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (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 (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y)))))
  (label 10)
  (parent 3)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y expt) (y-0 x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (deflistener (cat (gen) x))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y-0 x)
  (precur (2 0))
  (operation nonce-test (contracted (x-0 x) (w x)) (gen) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) b (pubk a))))
    ((recv (cat (gen) x)) (send (cat (gen) x))))
  (label 11)
  (parent 4)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y expt) (x y-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (deflistener (cat (exp (gen) y-0) (mul x (rec y-0))))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x y-0)
  (operation nonce-test (displaced 3 1 resp 2) (exp (gen) y-1) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) b (pubk a))))
    ((recv (cat (exp (gen) y-0) (mul x (rec y-0))))
      (send (cat (exp (gen) y-0) (mul x (rec y-0))))))
  (label 12)
  (parent 4)
  (unrealized (0 1) (0 3) (2 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b b-0 a-0 name) (y expt) (y-0 rndx) (x expt)
    (x-0 y-1 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x-0))
  (defstrand resp 2 (b b) (a a) (x x-0) (y y-0))
  (deflistener (cat (exp (gen) y-1) (mul x-0 (rec y-1))))
  (defstrand resp 2 (b b-0) (a a-0) (x x) (y y-1))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (absent (y-1 (exp (gen) x)) (y-0 (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y-0 x-0 y-1)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-1) (2 0))
  (traces
    ((send (enc (exp (gen) x-0) a (pubk b)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y-0) b (pubk a))))
    ((recv (cat (exp (gen) y-1) (mul x-0 (rec y-1))))
      (send (cat (exp (gen) y-1) (mul x-0 (rec y-1)))))
    ((recv (enc (exp (gen) x) a-0 (pubk b-0)))
      (send (enc (exp (gen) x) (exp (gen) y-1) b-0 (pubk a-0)))))
  (label 13)
  (parent 4)
  (unrealized (0 1) (0 3) (2 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y expt) (y-0 x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (deflistener (cat (exp (gen) x) (one)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y-0 x)
  (operation nonce-test (displaced 3 0 init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) b (pubk a))))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one)))))
  (label 14)
  (parent 4)
  (seen 16)
  (unrealized (2 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 name) (y expt) (y-0 x x-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0))))
  (defstrand init 1 (a a-0) (b b-0) (x x-0))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 0) (2 0)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y-0 x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) b (pubk a))))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0))))
      (send (cat (exp (gen) x-0) (mul x (rec x-0)))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))))
  (label 15)
  (parent 4)
  (unrealized (0 1) (0 3) (2 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y expt) (y-0 x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (deflistener (cat (exp (gen) x) (one)))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y-0 x)
  (operation nonce-test (added-strand resp 2) (exp (gen) x) (1 0)
    (enc (exp (gen) x) a (pubk b)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) b (pubk a)))))
  (label 16)
  (parent 7)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (b a name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (displaced 2 0 init 3) (exp (gen) y) (1 2)
    (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x))))))
  (label 17)
  (parent 9)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (y y) (x x) (n n))))
  (origs (n (1 3))))

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

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

(defskeleton dhnsl
  (vars (n text) (a b name) (y expt) (y-0 y-1 x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (deflistener (cat (exp (gen) x) (one)))
  (defstrand resp 2 (b b) (a a) (x x) (y y-1))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (absent (y-1 (exp (gen) x)) (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y-0 y-1 x)
  (operation nonce-test (added-strand resp 2) (exp (gen) x) (2 0)
    (enc (exp (gen) x) a (pubk b)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) b (pubk a))))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-1) b (pubk a)))))
  (label 20)
  (parent 14)
  (seen 16)
  (unrealized (2 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (b a name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (gen) y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (2 0)) ((1 3) (0 3))
    ((2 1) (1 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (uniq-gen x y)
  (uniq-orig n)
  (precur (2 0))
  (operation nonce-test (contracted (y-0 y) (w y)) (gen) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))))
    ((recv (cat (gen) y)) (send (cat (gen) y))))
  (label 21)
  (parent 18)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (b a name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (2 0)) ((1 3) (0 3))
    ((2 1) (1 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (precur (2 0))
  (uniq-gen x y)
  (uniq-orig n)
  (operation nonce-test (displaced 3 1 resp 2) (exp (gen) y-0) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one)))))
  (label 22)
  (parent 18)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton dhnsl
  (vars (n text) (b a name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) x) (mul y (rec x))))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (2 0)) ((1 3) (0 3))
    ((2 1) (1 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (precur (2 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (displaced 3 0 init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))))
    ((recv (cat (exp (gen) x) (mul y (rec x))))
      (send (cat (exp (gen) x) (mul y (rec x))))))
  (label 24)
  (parent 18)
  (unrealized (1 2) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton dhnsl
  (vars (n text) (a b name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (gen) (mul x y)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((2 1) (0 3))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (precur (3 0))
  (operation nonce-test (contracted (x-0 x) (y-0 y) (w (mul x y))) (gen)
    (3 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (gen) (mul x y))) (send (cat (gen) (mul x y)))))
  (label 26)
  (parent 19)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((2 1) (0 3))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x y)
  (operation nonce-test (displaced 4 1 resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a))))
    ((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 27)
  (parent 19)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b b-0 a-0 name) (x expt) (x-0 y y-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x-0))
  (defstrand resp 2 (b b) (a a) (x x-0) (y y))
  (deflistener (exp (gen) (mul x-0 y)))
  (deflistener (cat (exp (gen) y-0) (mul x-0 y (rec y-0))))
  (defstrand resp 2 (b b-0) (a a-0) (x x) (y y-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((2 1) (0 3))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (absent (y-0 (exp (gen) x)) (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x-0 y y-0)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((send (enc (exp (gen) x-0) a (pubk b)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x-0 y)))) (send n))
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) b (pubk a))))
    ((recv (exp (gen) (mul x-0 y))) (send (exp (gen) (mul x-0 y))))
    ((recv (cat (exp (gen) y-0) (mul x-0 y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul x-0 y (rec y-0)))))
    ((recv (enc (exp (gen) x) a-0 (pubk b-0)))
      (send (enc (exp (gen) x) (exp (gen) y-0) b-0 (pubk a-0)))))
  (label 28)
  (parent 19)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((2 1) (0 3))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x)
  (operation nonce-test (displaced 4 0 init 1) (exp (gen) x-0) (3 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a))))
    ((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 29)
  (parent 19)
  (unrealized (3 0))
  (comment "empty cohort"))

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

(defskeleton dhnsl
  (vars (n text) (b a name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((1 3) (0 3))
    ((2 1) (1 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (precur (2 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (displaced 3 0 init 3) (exp (gen) y) (2 0)
    (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one)))))
  (label 31)
  (parent 22)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (b a name) (y y-0 x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) x) (mul y (rec x))))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((1 1) (2 0))
    ((1 3) (0 3)) ((2 1) (1 2)) ((3 1) (2 0)))
  (absent (y-0 (exp (gen) x)) (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (precur (2 0))
  (uniq-gen y y-0 x)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) (exp (gen) x) (2 0)
    (enc (exp (gen) x) a (pubk b))
    (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))))
    ((recv (cat (exp (gen) x) (mul y (rec x))))
      (send (cat (exp (gen) x) (mul y (rec x)))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) b (pubk a)))))
  (label 32)
  (parent 24)
  (unrealized (1 2) (2 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhnsl diffie-hellman
  (defrole resp
    (vars (b a name) (x expt) (y rndx) (n text))
    (trace (recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    (uniq-orig n)
    (uniq-gen y)
    (absent (y (exp (gen) x)))
    (comment "Y should be assumed to be freshly chosen per role"))
  (defrole init
    (vars (a b name) (y expt) (x rndx) (n text))
    (trace (send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    (uniq-gen x)
    (comment "X should be assumed to be freshly chosen per role"))
  (comment
    "Needham-Schroeder-Lowe DH challenge/responses in place of nonces"))

(defskeleton dhnsl
  (vars (n text) (a b name) (x expt) (y rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (uniq-orig n)
  (comment "Responder point-of-view")
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n)))
  (label 33)
  (unrealized (0 2) (0 4))
  (origs (n (0 3)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-strand init 3) (exp (gen) y) (0 2)
    (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))))
  (label 34)
  (parent 33)
  (unrealized (0 4))
  (comment "3 in cohort - 3 not yet seen"))

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

(defskeleton dhnsl
  (vars (n text) (a b name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (precedes ((0 1) (1 1)) ((0 3) (1 3)) ((1 0) (0 0)) ((1 2) (0 2))
    ((1 4) (0 4)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (displaced 1 2 init 5) n (0 4)
    (enc n (exp (gen) (mul y x-0))))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n)))
  (label 36)
  (parent 34)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (x x) (y y) (n n))))
  (origs (n (0 3))))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-0) (y (mul y x (rec x-0)))
    (x x-0))
  (precedes ((0 1) (1 1)) ((0 1) (2 1)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 4) (0 4)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (added-strand init 5) n (0 4)
    (enc n (exp (gen) (mul y x))))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0))) b-0
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-0)))
      (recv (enc n (exp (gen) (mul y x)))) (send n)))
  (label 37)
  (parent 34)
  (unrealized (2 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (precedes ((0 1) (1 1)) ((0 1) (2 0)) ((1 0) (0 0)) ((1 2) (0 2))
    ((2 1) (0 4)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-listener (exp (gen) (mul y x))) n (0 4)
    (enc n (exp (gen) (mul y x))))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x)))))
  (label 38)
  (parent 34)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b name) (x expt) (y rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (gen) y))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (uniq-orig n)
  (precur (1 0))
  (operation nonce-test (contracted (y-0 y) (w y)) (gen) (1 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (cat (gen) y)) (send (cat (gen) y))))
  (label 39)
  (parent 35)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b name) (x expt) (y rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y)
  (uniq-orig n)
  (operation nonce-test (displaced 2 0 resp 2) (exp (gen) y-0) (1 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one)))))
  (label 40)
  (parent 35)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b b-0 a-0 name) (x x-0 expt) (y y-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y-0) (mul y (rec y-0))))
  (defstrand resp 2 (b b-0) (a a-0) (x x-0) (y y-0))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (absent (y-0 (exp (gen) x-0)) (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y y-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (1 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (cat (exp (gen) y-0) (mul y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y (rec y-0)))))
    ((recv (enc (exp (gen) x-0) a-0 (pubk b-0)))
      (send (enc (exp (gen) x-0) (exp (gen) y-0) b-0 (pubk a-0)))))
  (label 41)
  (parent 35)
  (unrealized (0 2) (0 4) (1 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 name) (x expt) (y x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) x-0) (mul y (rec x-0))))
  (defstrand init 1 (a a-0) (b b-0) (x x-0))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y x-0)
  (uniq-orig n)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (1 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (cat (exp (gen) x-0) (mul y (rec x-0))))
      (send (cat (exp (gen) x-0) (mul y (rec x-0)))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))))
  (label 42)
  (parent 35)
  (unrealized (0 2) (0 4) (1 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 name) (y x x-0 rndx) (w expt))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-0) (y (mul y x (rec x-0)))
    (x x-0))
  (deflistener (cat (exp (gen) (mul y x (rec x-0) (rec w))) w))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (precur (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x (rec x-0) (rec w))) w))
    (exp (gen) (mul y x (rec x-0))) (2 1))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0))) b-0
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-0)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) (mul y x (rec x-0) (rec w))) w))
      (send (cat (exp (gen) (mul y x (rec x-0) (rec w))) w))))
  (label 43)
  (parent 37)
  (unrealized (3 0))
  (comment "6 in cohort - 6 not yet seen"))

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

(defskeleton dhnsl
  (vars (n text) (a b name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b) (y y) (x x))
  (precedes ((0 1) (2 1)) ((1 1) (0 2)) ((2 0) (0 0)) ((2 2) (1 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-strand init 3) (exp (gen) y) (1 0)
    (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))))
  (label 45)
  (parent 40)
  (unrealized (0 4) (1 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-0) (y (mul y x (rec x-0)))
    (x x-0))
  (deflistener (cat (gen) (mul y x (rec x-0))))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (precur (3 0))
  (operation nonce-test
    (contracted (y-0 y) (x-1 x) (x-2 x-0) (w (mul y x (rec x-0)))) (gen)
    (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0))) b-0
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-0)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (gen) (mul y x (rec x-0))))
      (send (cat (gen) (mul y x (rec x-0))))))
  (label 46)
  (parent 43)
  (unrealized (2 1) (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 name) (x x-0 y rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-0) (y (mul (rec x) x-0 y)) (x x))
  (deflistener (cat (exp (gen) y) (mul (rec x) x-0)))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1)))
  (absent (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x x-0 y)
  (uniq-orig n)
  (operation nonce-test (displaced 4 0 resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x-0 y)))) (recv n))
    ((send (enc (exp (gen) x-0) a (pubk b)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((send (enc (exp (gen) x) a-0 (pubk b-0)))
      (recv
        (enc (exp (gen) x) (exp (gen) (mul (rec x) x-0 y)) b-0
          (pubk a-0)))
      (send (enc (exp (gen) (mul (rec x) x-0 y)) (pubk b-0)))
      (recv (enc n (exp (gen) (mul x-0 y)))) (send n))
    ((recv (cat (exp (gen) y) (mul (rec x) x-0)))
      (send (cat (exp (gen) y) (mul (rec x) x-0)))))
  (label 47)
  (parent 43)
  (unrealized (2 1) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 b-1 a-1 name) (x expt)
    (y x-0 x-1 y-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-0) (y (mul y x-0 (rec x-1)))
    (x x-1))
  (deflistener (cat (exp (gen) y-0) (mul y x-0 (rec x-1) (rec y-0))))
  (defstrand resp 2 (b b-1) (a a-1) (x x) (y y-0))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1))
    ((4 1) (3 0)))
  (absent (y-0 (exp (gen) x)) (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x-0 x-1 y-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((send (enc (exp (gen) x-0) a (pubk b)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((send (enc (exp (gen) x-1) a-0 (pubk b-0)))
      (recv
        (enc (exp (gen) x-1) (exp (gen) (mul y x-0 (rec x-1))) b-0
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x-0 (rec x-1))) (pubk b-0)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) y-0) (mul y x-0 (rec x-1) (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y x-0 (rec x-1) (rec y-0)))))
    ((recv (enc (exp (gen) x) a-1 (pubk b-1)))
      (send (enc (exp (gen) x) (exp (gen) y-0) b-1 (pubk a-1)))))
  (label 48)
  (parent 43)
  (unrealized (2 1) (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-0) (y (mul y (rec x) x-0)) (x x))
  (deflistener (cat (exp (gen) x-0) (mul y (rec x))))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1)))
  (absent (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (displaced 4 1 init 1) (exp (gen) x-1) (3 0))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((send (enc (exp (gen) x-0) a (pubk b)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((send (enc (exp (gen) x) a-0 (pubk b-0)))
      (recv
        (enc (exp (gen) x) (exp (gen) (mul y (rec x) x-0)) b-0
          (pubk a-0)))
      (send (enc (exp (gen) (mul y (rec x) x-0)) (pubk b-0)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) x-0) (mul y (rec x))))
      (send (cat (exp (gen) x-0) (mul y (rec x))))))
  (label 49)
  (parent 43)
  (unrealized (2 1) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-0) (y (mul y x (rec x-0)))
    (x x-0))
  (deflistener (cat (exp (gen) x-0) (mul y x (rec x-0) (rec x-0))))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (displaced 4 2 init 1) (exp (gen) x-1) (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0))) b-0
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-0)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) x-0) (mul y x (rec x-0) (rec x-0))))
      (send (cat (exp (gen) x-0) (mul y x (rec x-0) (rec x-0))))))
  (label 50)
  (parent 43)
  (unrealized (2 1) (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 a-1 b-1 name) (y x x-0 x-1 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-0) (y (mul y x (rec x-0)))
    (x x-0))
  (deflistener (cat (exp (gen) x-1) (mul y x (rec x-0) (rec x-1))))
  (defstrand init 1 (a a-1) (b b-1) (x x-1))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1))
    ((4 0) (3 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x x-0 x-1)
  (uniq-orig n)
  (operation nonce-test (added-strand init 1) (exp (gen) x-1) (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0))) b-0
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-0)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) x-1) (mul y x (rec x-0) (rec x-1))))
      (send (cat (exp (gen) x-1) (mul y x (rec x-0) (rec x-1)))))
    ((send (enc (exp (gen) x-1) a-1 (pubk b-1)))))
  (label 51)
  (parent 43)
  (unrealized (2 1) (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (gen) (mul y x)))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2))
    ((2 1) (0 4)) ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (uniq-orig n)
  (precur (3 0))
  (operation nonce-test (contracted (y-0 y) (x-0 x) (w (mul y x))) (gen)
    (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (gen) (mul y x))) (send (cat (gen) (mul y x)))))
  (label 52)
  (parent 44)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b name) (x y rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2))
    ((2 1) (0 4)) ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x y)
  (uniq-orig n)
  (operation nonce-test (displaced 4 0 resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk 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 53)
  (parent 44)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b b-0 a-0 name) (x expt) (y x-0 y-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x-0))
  (deflistener (exp (gen) (mul y x-0)))
  (deflistener (cat (exp (gen) y-0) (mul y x-0 (rec y-0))))
  (defstrand resp 2 (b b-0) (a a-0) (x x) (y y-0))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2))
    ((2 1) (0 4)) ((3 1) (2 0)) ((4 1) (3 0)))
  (absent (y-0 (exp (gen) x)) (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x-0 y-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((send (enc (exp (gen) x-0) a (pubk b)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((recv (exp (gen) (mul y x-0))) (send (exp (gen) (mul y x-0))))
    ((recv (cat (exp (gen) y-0) (mul y x-0 (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y x-0 (rec y-0)))))
    ((recv (enc (exp (gen) x) a-0 (pubk b-0)))
      (send (enc (exp (gen) x) (exp (gen) y-0) b-0 (pubk a-0)))))
  (label 54)
  (parent 44)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2))
    ((2 1) (0 4)) ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (displaced 4 1 init 1) (exp (gen) x-0) (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((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 55)
  (parent 44)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x-0) (mul y x (rec x-0))))
  (defstrand init 1 (a a-0) (b b-0) (x x-0))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2))
    ((2 1) (0 4)) ((3 1) (2 0)) ((4 0) (3 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) x-0) (mul y x (rec x-0))))
      (send (cat (exp (gen) x-0) (mul y x (rec x-0)))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))))
  (label 56)
  (parent 44)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 name) (x y x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-0) (y (mul (rec x) y x-0)) (x x))
  (deflistener (cat (exp (gen) y) (mul (rec x) x-0)))
  (precedes ((0 1) (1 1)) ((0 3) (2 3)) ((1 0) (0 0)) ((1 2) (0 2))
    ((1 2) (3 0)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1)))
  (absent (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x y x-0)
  (uniq-orig n)
  (operation nonce-test (displaced 4 1 init 3) (exp (gen) y) (3 0)
    (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((send (enc (exp (gen) x-0) a (pubk b)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((send (enc (exp (gen) x) a-0 (pubk b-0)))
      (recv
        (enc (exp (gen) x) (exp (gen) (mul (rec x) y x-0)) b-0
          (pubk a-0)))
      (send (enc (exp (gen) (mul (rec x) y x-0)) (pubk b-0)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) y) (mul (rec x) x-0)))
      (send (cat (exp (gen) y) (mul (rec x) x-0)))))
  (label 57)
  (parent 47)
  (unrealized (2 1) (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b a-0 b-0 name) (y x y-0 x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (defstrand init 3 (a a) (b b) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-0) (y (mul y (rec x) x-0)) (x x))
  (deflistener (cat (exp (gen) x-0) (mul y (rec x))))
  (defstrand resp 2 (b b) (a a) (x x-0) (y y-0))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 0) (4 0)) ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4))
    ((3 1) (2 1)) ((4 1) (3 0)))
  (absent (y-0 (exp (gen) x-0)) (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x y-0 x-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) (exp (gen) x-0) (3 0)
    (enc (exp (gen) x-0) a (pubk b))
    (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((send (enc (exp (gen) x-0) a (pubk b)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (pubk b))))
    ((send (enc (exp (gen) x) a-0 (pubk b-0)))
      (recv
        (enc (exp (gen) x) (exp (gen) (mul y (rec x) x-0)) b-0
          (pubk a-0)))
      (send (enc (exp (gen) (mul y (rec x) x-0)) (pubk b-0)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) x-0) (mul y (rec x))))
      (send (cat (exp (gen) x-0) (mul y (rec x)))))
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y-0) b (pubk a)))))
  (label 58)
  (parent 49)
  (unrealized (2 1) (3 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhns diffie-hellman
  (defrole resp
    (vars (b a name) (x expt) (y rndx) (n text))
    (trace (recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    (uniq-orig n)
    (uniq-gen y)
    (absent (y (exp (gen) x)))
    (comment "Y should be assumed to be freshly chosen per role"))
  (defrole init
    (vars (a b name) (y expt) (x rndx) (n text))
    (trace (send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    (uniq-gen x)
    (comment "X should be assumed to be freshly chosen per role"))
  (comment
    "Needham-Schroeder-Lowe DH challenge/responses in place of nonces"))

(defskeleton dhns
  (vars (n text) (a b name) (y expt) (x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (comment "Initiator point-of-view")
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n)))
  (label 59)
  (unrealized (0 1) (0 3))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b name) (y expt) (y-0 x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y-0 x)
  (operation nonce-test (added-strand resp 2) (exp (gen) x) (0 1)
    (enc (exp (gen) x) a (pubk b)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a)))))
  (label 60)
  (parent 59)
  (unrealized (0 1) (0 3))
  (comment "2 in cohort - 2 not yet seen"))

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

(defskeleton dhns
  (vars (n text) (a b name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (operation nonce-test (contracted (y-0 y) (y-1 y)) (exp (gen) x) (0 1)
    (enc (exp (gen) x) a (pubk b))
    (enc (exp (gen) x) (exp (gen) y) (pubk a)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))))
  (label 62)
  (parent 60)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

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

(defskeleton dhns
  (vars (n text) (a b name) (y expt) (x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (deflistener (cat (gen) x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (precur (1 0))
  (operation nonce-test (contracted (x-0 x) (w x)) (gen) (1 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (gen) x)) (send (cat (gen) x))))
  (label 64)
  (parent 61)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 name) (y x expt) (x-0 y-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x-0))
  (deflistener (cat (exp (gen) y-0) (mul x-0 (rec y-0))))
  (defstrand resp 2 (b b-0) (a a-0) (x x) (y y-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen x-0 y-0)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (1 0))
  (traces
    ((send (enc (exp (gen) x-0) a (pubk b)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) y-0) (mul x-0 (rec y-0))))
      (send (cat (exp (gen) y-0) (mul x-0 (rec y-0)))))
    ((recv (enc (exp (gen) x) a-0 (pubk b-0)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a-0)))))
  (label 65)
  (parent 61)
  (unrealized (0 1) (0 3) (1 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b name) (y expt) (x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (deflistener (cat (exp (gen) x) (one)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen x)
  (operation nonce-test (displaced 2 0 init 1) (exp (gen) x-0) (1 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one)))))
  (label 66)
  (parent 61)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b a-0 b-0 name) (y expt) (x x-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0))))
  (defstrand init 1 (a a-0) (b b-0) (x x-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 0) (1 0)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (1 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0))))
      (send (cat (exp (gen) x-0) (mul x (rec x-0)))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))))
  (label 67)
  (parent 61)
  (unrealized (0 1) (0 3) (1 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (b a name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 3) (0 3)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (uniq-gen x y)
  (uniq-orig n)
  (operation encryption-test (displaced 1 2 resp 4)
    (enc n (exp (gen) (mul x y-0))) (0 3))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y))))))
  (label 68)
  (parent 62)
  (unrealized (1 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y))
  (deflistener (exp (gen) (mul x y)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (2 0)) ((2 1) (0 3)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (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 (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y)))))
  (label 69)
  (parent 62)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b name) (y expt) (y-0 x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (deflistener (cat (gen) x))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y-0 x)
  (precur (2 0))
  (operation nonce-test (contracted (x-0 x) (w x)) (gen) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a))))
    ((recv (cat (gen) x)) (send (cat (gen) x))))
  (label 70)
  (parent 63)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b name) (y expt) (x y-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (deflistener (cat (exp (gen) y-0) (mul x (rec y-0))))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x y-0)
  (operation nonce-test (displaced 3 1 resp 2) (exp (gen) y-1) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a))))
    ((recv (cat (exp (gen) y-0) (mul x (rec y-0))))
      (send (cat (exp (gen) y-0) (mul x (rec y-0))))))
  (label 71)
  (parent 63)
  (unrealized (0 1) (0 3) (2 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 name) (y expt) (y-0 rndx) (x expt)
    (x-0 y-1 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x-0))
  (defstrand resp 2 (b b) (a a) (x x-0) (y y-0))
  (deflistener (cat (exp (gen) y-1) (mul x-0 (rec y-1))))
  (defstrand resp 2 (b b-0) (a a-0) (x x) (y y-1))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (absent (y-1 (exp (gen) x)) (y-0 (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y-0 x-0 y-1)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-1) (2 0))
  (traces
    ((send (enc (exp (gen) x-0) a (pubk b)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y-0) (pubk a))))
    ((recv (cat (exp (gen) y-1) (mul x-0 (rec y-1))))
      (send (cat (exp (gen) y-1) (mul x-0 (rec y-1)))))
    ((recv (enc (exp (gen) x) a-0 (pubk b-0)))
      (send (enc (exp (gen) x) (exp (gen) y-1) (pubk a-0)))))
  (label 72)
  (parent 63)
  (unrealized (0 1) (0 3) (2 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b name) (y expt) (y-0 x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (deflistener (cat (exp (gen) x) (one)))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y-0 x)
  (operation nonce-test (displaced 3 0 init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a))))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one)))))
  (label 73)
  (parent 63)
  (seen 75)
  (unrealized (2 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b a-0 b-0 name) (y expt) (y-0 x x-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0))))
  (defstrand init 1 (a a-0) (b b-0) (x x-0))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 0) (2 0)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y-0 x x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a))))
    ((recv (cat (exp (gen) x-0) (mul x (rec x-0))))
      (send (cat (exp (gen) x-0) (mul x (rec x-0)))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))))
  (label 74)
  (parent 63)
  (unrealized (0 1) (0 3) (2 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b name) (y expt) (y-0 x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (deflistener (cat (exp (gen) x) (one)))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y-0 x)
  (operation nonce-test (added-strand resp 2) (exp (gen) x) (1 0)
    (enc (exp (gen) x) a (pubk b)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a)))))
  (label 75)
  (parent 66)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (b a name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (displaced 2 0 init 3) (exp (gen) y) (1 2)
    (enc (exp (gen) x) (exp (gen) y) (pubk a)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x))))))
  (label 76)
  (parent 68)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (y y) (x x) (n n))))
  (origs (n (1 3))))

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

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

(defskeleton dhns
  (vars (n text) (a b name) (y expt) (y-0 y-1 x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (deflistener (cat (exp (gen) x) (one)))
  (defstrand resp 2 (b b) (a a) (x x) (y y-1))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (absent (y-1 (exp (gen) x)) (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen y-0 y-1 x)
  (operation nonce-test (added-strand resp 2) (exp (gen) x) (2 0)
    (enc (exp (gen) x) a (pubk b)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a))))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-1) (pubk a)))))
  (label 79)
  (parent 73)
  (seen 75)
  (unrealized (2 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dhns
  (vars (n text) (b a name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (gen) y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (2 0)) ((1 3) (0 3))
    ((2 1) (1 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (uniq-gen x y)
  (uniq-orig n)
  (precur (2 0))
  (operation nonce-test (contracted (y-0 y) (w y)) (gen) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))))
    ((recv (cat (gen) y)) (send (cat (gen) y))))
  (label 80)
  (parent 77)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (b a name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (2 0)) ((1 3) (0 3))
    ((2 1) (1 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (precur (2 0))
  (uniq-gen x y)
  (uniq-orig n)
  (operation nonce-test (displaced 3 1 resp 2) (exp (gen) y-0) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one)))))
  (label 81)
  (parent 77)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (b a b-0 a-0 name) (x rndx) (x-0 expt) (y y-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y-0) (mul y (rec y-0))))
  (defstrand resp 2 (b b-0) (a a-0) (x x-0) (y y-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (2 0)) ((1 3) (0 3))
    ((2 1) (1 2)) ((3 1) (2 0)))
  (absent (y-0 (exp (gen) x-0)) (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (precur (2 0))
  (uniq-gen x y y-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))))
    ((recv (cat (exp (gen) y-0) (mul y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y (rec y-0)))))
    ((recv (enc (exp (gen) x-0) a-0 (pubk b-0)))
      (send (enc (exp (gen) x-0) (exp (gen) y-0) (pubk a-0)))))
  (label 82)
  (parent 77)
  (unrealized (1 2) (2 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (b a name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) x) (mul y (rec x))))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (2 0)) ((1 3) (0 3))
    ((2 1) (1 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (precur (2 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (displaced 3 0 init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))))
    ((recv (cat (exp (gen) x) (mul y (rec x))))
      (send (cat (exp (gen) x) (mul y (rec x))))))
  (label 83)
  (parent 77)
  (unrealized (1 2) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (b a a-0 b-0 name) (x y x-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) x-0) (mul y (rec x-0))))
  (defstrand init 1 (a a-0) (b b-0) (x x-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (2 0)) ((1 3) (0 3))
    ((2 1) (1 2)) ((3 0) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (precur (2 0))
  (uniq-gen x y x-0)
  (uniq-orig n)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))))
    ((recv (cat (exp (gen) x-0) (mul y (rec x-0))))
      (send (cat (exp (gen) x-0) (mul y (rec x-0)))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))))
  (label 84)
  (parent 77)
  (unrealized (1 2) (2 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (gen) (mul x y)))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((2 1) (0 3))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (precur (3 0))
  (operation nonce-test (contracted (x-0 x) (y-0 y) (w (mul x y))) (gen)
    (3 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (gen) (mul x y))) (send (cat (gen) (mul x y)))))
  (label 85)
  (parent 78)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b name) (x y rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((2 1) (0 3))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x y)
  (operation nonce-test (displaced 4 1 resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a))))
    ((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 86)
  (parent 78)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 name) (x expt) (x-0 y y-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x-0))
  (defstrand resp 2 (b b) (a a) (x x-0) (y y))
  (deflistener (exp (gen) (mul x-0 y)))
  (deflistener (cat (exp (gen) y-0) (mul x-0 y (rec y-0))))
  (defstrand resp 2 (b b-0) (a a-0) (x x) (y y-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((2 1) (0 3))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (absent (y-0 (exp (gen) x)) (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x-0 y y-0)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((send (enc (exp (gen) x-0) a (pubk b)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x-0 y)))) (send n))
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) (pubk a))))
    ((recv (exp (gen) (mul x-0 y))) (send (exp (gen) (mul x-0 y))))
    ((recv (cat (exp (gen) y-0) (mul x-0 y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul x-0 y (rec y-0)))))
    ((recv (enc (exp (gen) x) a-0 (pubk b-0)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a-0)))))
  (label 87)
  (parent 78)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((2 1) (0 3))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x)
  (operation nonce-test (displaced 4 0 init 1) (exp (gen) x-0) (3 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a))))
    ((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 88)
  (parent 78)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b a-0 b-0 name) (x y x-0 rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 2 (b b) (a a) (x x) (y y))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) x-0) (mul x y (rec x-0))))
  (defstrand init 1 (a a-0) (b b-0) (x x-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 1) (3 0)) ((2 1) (0 3))
    ((3 1) (2 0)) ((4 0) (3 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x y x-0)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (3 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul x y)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a))))
    ((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y))))
    ((recv (cat (exp (gen) x-0) (mul x y (rec x-0))))
      (send (cat (exp (gen) x-0) (mul x y (rec x-0)))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))))
  (label 89)
  (parent 78)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (b a name) (y x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((1 3) (0 3))
    ((2 1) (1 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (precur (2 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (displaced 3 0 init 3) (exp (gen) y) (2 0)
    (enc (exp (gen) x) (exp (gen) y) (pubk a)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one)))))
  (label 90)
  (parent 81)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (b a name) (y y-0 x rndx))
  (defstrand init 5 (n n) (a a) (b b) (y y) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) x) (mul y (rec x))))
  (defstrand resp 2 (b b) (a a) (x x) (y y-0))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((1 1) (2 0))
    ((1 3) (0 3)) ((2 1) (1 2)) ((3 1) (2 0)))
  (absent (y-0 (exp (gen) x)) (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (precur (2 0))
  (uniq-gen y y-0 x)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) (exp (gen) x) (2 0)
    (enc (exp (gen) x) a (pubk b))
    (enc (exp (gen) x) (exp (gen) y) (pubk a)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))))
    ((recv (cat (exp (gen) x) (mul y (rec x))))
      (send (cat (exp (gen) x) (mul y (rec x)))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a)))))
  (label 91)
  (parent 83)
  (unrealized (1 2) (2 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhns diffie-hellman
  (defrole resp
    (vars (b a name) (x expt) (y rndx) (n text))
    (trace (recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    (uniq-orig n)
    (uniq-gen y)
    (absent (y (exp (gen) x)))
    (comment "Y should be assumed to be freshly chosen per role"))
  (defrole init
    (vars (a b name) (y expt) (x rndx) (n text))
    (trace (send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    (uniq-gen x)
    (comment "X should be assumed to be freshly chosen per role"))
  (comment
    "Needham-Schroeder-Lowe DH challenge/responses in place of nonces"))

(defskeleton dhns
  (vars (n text) (a b name) (x expt) (y rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (uniq-orig n)
  (comment "Responder point-of-view")
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n)))
  (label 92)
  (unrealized (0 2) (0 4))
  (origs (n (0 3)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b b-0 name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-strand init 3) (exp (gen) y) (0 2)
    (enc (exp (gen) x) (exp (gen) y) (pubk a)))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0)))))
  (label 93)
  (parent 92)
  (unrealized (0 4))
  (comment "3 in cohort - 3 not yet seen"))

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

(defskeleton dhns
  (vars (n text) (b a b-0 name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 5 (n n) (a a) (b b-0) (y y) (x x))
  (precedes ((0 1) (1 1)) ((0 3) (1 3)) ((1 0) (0 0)) ((1 2) (0 2))
    ((1 4) (0 4)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (displaced 1 2 init 5) n (0 4)
    (enc n (exp (gen) (mul y x-0))))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0)))
      (recv (enc n (exp (gen) (mul y x)))) (send n)))
  (label 95)
  (parent 93)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (x x) (y y) (n n))))
  (origs (n (0 3))))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y x (rec x-0)))
    (x x-0))
  (precedes ((0 1) (1 1)) ((0 1) (2 1)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 4) (0 4)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (added-strand init 5) n (0 4)
    (enc n (exp (gen) (mul y x))))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0)))
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x)))) (send n)))
  (label 96)
  (parent 93)
  (unrealized (2 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b b-0 name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (precedes ((0 1) (1 1)) ((0 1) (2 0)) ((1 0) (0 0)) ((1 2) (0 2))
    ((2 1) (0 4)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-listener (exp (gen) (mul y x))) n (0 4)
    (enc n (exp (gen) (mul y x))))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x)))))
  (label 97)
  (parent 93)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b name) (x expt) (y rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (gen) y))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (uniq-orig n)
  (precur (1 0))
  (operation nonce-test (contracted (y-0 y) (w y)) (gen) (1 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (cat (gen) y)) (send (cat (gen) y))))
  (label 98)
  (parent 94)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b name) (x expt) (y rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y)
  (uniq-orig n)
  (operation nonce-test (displaced 2 0 resp 2) (exp (gen) y-0) (1 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one)))))
  (label 99)
  (parent 94)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 name) (x x-0 expt) (y y-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y-0) (mul y (rec y-0))))
  (defstrand resp 2 (b b-0) (a a-0) (x x-0) (y y-0))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (absent (y-0 (exp (gen) x-0)) (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y y-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (1 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (cat (exp (gen) y-0) (mul y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y (rec y-0)))))
    ((recv (enc (exp (gen) x-0) a-0 (pubk b-0)))
      (send (enc (exp (gen) x-0) (exp (gen) y-0) (pubk a-0)))))
  (label 100)
  (parent 94)
  (unrealized (0 2) (0 4) (1 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b a-0 b-0 name) (x expt) (y x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) x-0) (mul y (rec x-0))))
  (defstrand init 1 (a a-0) (b b-0) (x x-0))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y x-0)
  (uniq-orig n)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (1 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (cat (exp (gen) x-0) (mul y (rec x-0))))
      (send (cat (exp (gen) x-0) (mul y (rec x-0)))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-0)))))
  (label 101)
  (parent 94)
  (unrealized (0 2) (0 4) (1 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (y x x-0 rndx) (w expt))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y x (rec x-0)))
    (x x-0))
  (deflistener (cat (exp (gen) (mul y x (rec x-0) (rec w))) w))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (precur (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x (rec x-0) (rec w))) w))
    (exp (gen) (mul y x (rec x-0))) (2 1))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0)))
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) (mul y x (rec x-0) (rec w))) w))
      (send (cat (exp (gen) (mul y x (rec x-0) (rec w))) w))))
  (label 102)
  (parent 96)
  (unrealized (3 0))
  (comment "6 in cohort - 6 not yet seen"))

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

(defskeleton dhns
  (vars (n text) (a b b-0 name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (precedes ((0 1) (2 1)) ((1 1) (0 2)) ((2 0) (0 0)) ((2 2) (1 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-strand init 3) (exp (gen) y) (1 0)
    (enc (exp (gen) x) (exp (gen) y) (pubk a)))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0)))))
  (label 104)
  (parent 99)
  (unrealized (0 4))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y x (rec x-0)))
    (x x-0))
  (deflistener (cat (gen) (mul y x (rec x-0))))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (precur (3 0))
  (operation nonce-test
    (contracted (y-0 y) (x-1 x) (x-2 x-0) (w (mul y x (rec x-0)))) (gen)
    (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0)))
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (gen) (mul y x (rec x-0))))
      (send (cat (gen) (mul y x (rec x-0))))))
  (label 105)
  (parent 102)
  (unrealized (2 1) (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (x x-0 y rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul (rec x) x-0 y)) (x x))
  (deflistener (cat (exp (gen) y) (mul (rec x) x-0)))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1)))
  (absent (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x x-0 y)
  (uniq-orig n)
  (operation nonce-test (displaced 4 0 resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x-0 y)))) (recv n))
    ((send (enc (exp (gen) x-0) a (pubk b-0)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x) (exp (gen) (mul (rec x) x-0 y)) (pubk a-0)))
      (send (enc (exp (gen) (mul (rec x) x-0 y)) (pubk b-1)))
      (recv (enc n (exp (gen) (mul x-0 y)))) (send n))
    ((recv (cat (exp (gen) y) (mul (rec x) x-0)))
      (send (cat (exp (gen) y) (mul (rec x) x-0)))))
  (label 106)
  (parent 102)
  (unrealized (2 1) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 b-2 a-1 name) (x expt)
    (y x-0 x-1 y-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y x-0 (rec x-1)))
    (x x-1))
  (deflistener (cat (exp (gen) y-0) (mul y x-0 (rec x-1) (rec y-0))))
  (defstrand resp 2 (b b-2) (a a-1) (x x) (y y-0))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1))
    ((4 1) (3 0)))
  (absent (y-0 (exp (gen) x)) (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x-0 x-1 y-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((send (enc (exp (gen) x-0) a (pubk b-0)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x-1) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x-1) (exp (gen) (mul y x-0 (rec x-1)))
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x-0 (rec x-1))) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) y-0) (mul y x-0 (rec x-1) (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y x-0 (rec x-1) (rec y-0)))))
    ((recv (enc (exp (gen) x) a-1 (pubk b-2)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a-1)))))
  (label 107)
  (parent 102)
  (unrealized (2 1) (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y (rec x) x-0)) (x x))
  (deflistener (cat (exp (gen) x-0) (mul y (rec x))))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1)))
  (absent (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (displaced 4 1 init 1) (exp (gen) x-1) (3 0))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((send (enc (exp (gen) x-0) a (pubk b-0)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x) (exp (gen) (mul y (rec x) x-0)) (pubk a-0)))
      (send (enc (exp (gen) (mul y (rec x) x-0)) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) x-0) (mul y (rec x))))
      (send (cat (exp (gen) x-0) (mul y (rec x))))))
  (label 108)
  (parent 102)
  (unrealized (2 1) (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y x (rec x-0)))
    (x x-0))
  (deflistener (cat (exp (gen) x-0) (mul y x (rec x-0) (rec x-0))))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (displaced 4 2 init 1) (exp (gen) x-1) (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0)))
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) x-0) (mul y x (rec x-0) (rec x-0))))
      (send (cat (exp (gen) x-0) (mul y x (rec x-0) (rec x-0))))))
  (label 109)
  (parent 102)
  (unrealized (2 1) (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 a-1 b-2 name) (y x x-0 x-1 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y x (rec x-0)))
    (x x-0))
  (deflistener (cat (exp (gen) x-1) (mul y x (rec x-0) (rec x-1))))
  (defstrand init 1 (a a-1) (b b-2) (x x-1))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((0 3) (2 3)) ((1 0) (0 0))
    ((1 2) (0 2)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1))
    ((4 0) (3 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x x-0 x-1)
  (uniq-orig n)
  (operation nonce-test (added-strand init 1) (exp (gen) x-1) (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0)))
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) x-1) (mul y x (rec x-0) (rec x-1))))
      (send (cat (exp (gen) x-1) (mul y x (rec x-0) (rec x-1)))))
    ((send (enc (exp (gen) x-1) a-1 (pubk b-2)))))
  (label 110)
  (parent 102)
  (unrealized (2 1) (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (gen) (mul y x)))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2))
    ((2 1) (0 4)) ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x)
  (uniq-orig n)
  (precur (3 0))
  (operation nonce-test (contracted (y-0 y) (x-0 x) (w (mul y x))) (gen)
    (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (gen) (mul y x))) (send (cat (gen) (mul y x)))))
  (label 111)
  (parent 103)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 name) (x y rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2))
    ((2 1) (0 4)) ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x y)
  (uniq-orig n)
  (operation nonce-test (displaced 4 0 resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((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 112)
  (parent 103)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 b-1 a-0 name) (x expt) (y x-0 y-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x-0))
  (deflistener (exp (gen) (mul y x-0)))
  (deflistener (cat (exp (gen) y-0) (mul y x-0 (rec y-0))))
  (defstrand resp 2 (b b-1) (a a-0) (x x) (y y-0))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2))
    ((2 1) (0 4)) ((3 1) (2 0)) ((4 1) (3 0)))
  (absent (y-0 (exp (gen) x)) (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x-0 y-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (3 0))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((send (enc (exp (gen) x-0) a (pubk b-0)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((recv (exp (gen) (mul y x-0))) (send (exp (gen) (mul y x-0))))
    ((recv (cat (exp (gen) y-0) (mul y x-0 (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y x-0 (rec y-0)))))
    ((recv (enc (exp (gen) x) a-0 (pubk b-1)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a-0)))))
  (label 113)
  (parent 103)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2))
    ((2 1) (0 4)) ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (displaced 4 1 init 1) (exp (gen) x-0) (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((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 114)
  (parent 103)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x-0) (mul y x (rec x-0))))
  (defstrand init 1 (a a-0) (b b-1) (x x-0))
  (precedes ((0 1) (1 1)) ((0 1) (3 0)) ((1 0) (0 0)) ((1 2) (0 2))
    ((2 1) (0 4)) ((3 1) (2 0)) ((4 0) (3 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) x-0) (mul y x (rec x-0))))
      (send (cat (exp (gen) x-0) (mul y x (rec x-0)))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-1)))))
  (label 115)
  (parent 103)
  (unrealized (2 0) (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (b a b-0 name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 5 (n n) (a a) (b b-0) (y y) (x x))
  (precedes ((0 1) (2 1)) ((0 3) (2 3)) ((1 1) (0 2)) ((2 0) (0 0))
    ((2 2) (1 0)) ((2 4) (0 4)))
  (absent (y (exp (gen) x)))
  (non-orig (privk b) (privk a))
  (precur (1 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (displaced 2 3 init 5) n (0 4)
    (enc n (exp (gen) (mul y x-0))))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0)))
      (recv (enc n (exp (gen) (mul y x)))) (send n)))
  (label 116)
  (parent 104)
  (seen 95)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y x (rec x-0)))
    (x x-0))
  (precedes ((0 1) (2 1)) ((0 1) (3 1)) ((0 3) (3 3)) ((1 1) (0 2))
    ((2 0) (0 0)) ((2 2) (1 0)) ((3 4) (0 4)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (added-strand init 5) n (0 4)
    (enc n (exp (gen) (mul y x))))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0)))
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x)))) (send n)))
  (label 117)
  (parent 104)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b b-0 name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (precedes ((0 1) (2 1)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 0) (0 0))
    ((2 2) (1 0)) ((3 1) (0 4)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-listener (exp (gen) (mul y x))) n (0 4)
    (enc n (exp (gen) (mul y x))))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x)))))
  (label 118)
  (parent 104)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (x y x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (defstrand init 3 (a a) (b b-0) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul (rec x) y x-0)) (x x))
  (deflistener (cat (exp (gen) y) (mul (rec x) x-0)))
  (precedes ((0 1) (1 1)) ((0 3) (2 3)) ((1 0) (0 0)) ((1 2) (0 2))
    ((1 2) (3 0)) ((2 0) (3 0)) ((2 4) (0 4)) ((3 1) (2 1)))
  (absent (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (3 0))
  (uniq-gen x y x-0)
  (uniq-orig n)
  (operation nonce-test (displaced 4 1 init 3) (exp (gen) y) (3 0)
    (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((send (enc (exp (gen) x-0) a (pubk b-0)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x) (exp (gen) (mul (rec x) y x-0)) (pubk a-0)))
      (send (enc (exp (gen) (mul (rec x) y x-0)) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) y) (mul (rec x) x-0)))
      (send (cat (exp (gen) y) (mul (rec x) x-0)))))
  (label 119)
  (parent 106)
  (unrealized (2 1) (3 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (y x x-0 rndx) (w expt))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y x (rec x-0)))
    (x x-0))
  (deflistener (cat (exp (gen) (mul y x (rec x-0) (rec w))) w))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((0 3) (3 3)) ((1 1) (0 2))
    ((2 0) (0 0)) ((2 2) (1 0)) ((3 0) (4 0)) ((3 4) (0 4))
    ((4 1) (3 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x (rec x-0) (rec w))) w))
    (exp (gen) (mul y x (rec x-0))) (3 1))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0)))
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) (mul y x (rec x-0) (rec w))) w))
      (send (cat (exp (gen) (mul y x (rec x-0) (rec w))) w))))
  (label 120)
  (parent 117)
  (unrealized (4 0))
  (comment "6 in cohort - 6 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b b-0 name) (y x rndx) (w expt))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) (mul y x (rec w))) w))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 0) (0 0))
    ((2 2) (1 0)) ((3 1) (0 4)) ((4 1) (3 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x (rec w))) w))
    (exp (gen) (mul y x)) (3 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) (mul y x (rec w))) w))
      (send (cat (exp (gen) (mul y x (rec w))) w))))
  (label 121)
  (parent 118)
  (unrealized (4 0))
  (comment "5 in cohort - 5 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y x (rec x-0)))
    (x x-0))
  (deflistener (cat (gen) (mul y x (rec x-0))))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((0 3) (3 3)) ((1 1) (0 2))
    ((2 0) (0 0)) ((2 2) (1 0)) ((3 0) (4 0)) ((3 4) (0 4))
    ((4 1) (3 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test
    (contracted (y-0 y) (x-1 x) (x-2 x-0) (w (mul y x (rec x-0)))) (gen)
    (4 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0)))
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (gen) (mul y x (rec x-0))))
      (send (cat (gen) (mul y x (rec x-0))))))
  (label 122)
  (parent 120)
  (unrealized (3 1) (4 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (x x-0 y rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul (rec x) x-0 y)) (x x))
  (deflistener (cat (exp (gen) y) (mul (rec x) x-0)))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((0 3) (3 3)) ((1 1) (0 2))
    ((2 0) (0 0)) ((2 2) (1 0)) ((3 0) (4 0)) ((3 4) (0 4))
    ((4 1) (3 1)))
  (absent (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen x x-0 y)
  (uniq-orig n)
  (operation nonce-test (displaced 5 0 resp 2) (exp (gen) y-0) (4 0))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x-0 y)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x-0) a (pubk b-0)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x) (exp (gen) (mul (rec x) x-0 y)) (pubk a-0)))
      (send (enc (exp (gen) (mul (rec x) x-0 y)) (pubk b-1)))
      (recv (enc n (exp (gen) (mul x-0 y)))) (send n))
    ((recv (cat (exp (gen) y) (mul (rec x) x-0)))
      (send (cat (exp (gen) y) (mul (rec x) x-0)))))
  (label 123)
  (parent 120)
  (unrealized (3 1) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 b-2 a-1 name) (x expt)
    (y x-0 x-1 y-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y x-0 (rec x-1)))
    (x x-1))
  (deflistener (cat (exp (gen) y-0) (mul y x-0 (rec x-1) (rec y-0))))
  (defstrand resp 2 (b b-2) (a a-1) (x x) (y y-0))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((0 3) (3 3)) ((1 1) (0 2))
    ((2 0) (0 0)) ((2 2) (1 0)) ((3 0) (4 0)) ((3 4) (0 4))
    ((4 1) (3 1)) ((5 1) (4 0)))
  (absent (y-0 (exp (gen) x)) (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen y x-0 x-1 y-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (4 0))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x-0) a (pubk b-0)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x-1) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x-1) (exp (gen) (mul y x-0 (rec x-1)))
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x-0 (rec x-1))) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) y-0) (mul y x-0 (rec x-1) (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y x-0 (rec x-1) (rec y-0)))))
    ((recv (enc (exp (gen) x) a-1 (pubk b-2)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a-1)))))
  (label 124)
  (parent 120)
  (unrealized (3 1) (4 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y (rec x) x-0)) (x x))
  (deflistener (cat (exp (gen) x-0) (mul y (rec x))))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((0 3) (3 3)) ((1 1) (0 2))
    ((2 0) (0 0)) ((2 2) (1 0)) ((3 0) (4 0)) ((3 4) (0 4))
    ((4 1) (3 1)))
  (absent (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (displaced 5 2 init 1) (exp (gen) x-1) (4 0))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x-0) a (pubk b-0)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x) (exp (gen) (mul y (rec x) x-0)) (pubk a-0)))
      (send (enc (exp (gen) (mul y (rec x) x-0)) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) x-0) (mul y (rec x))))
      (send (cat (exp (gen) x-0) (mul y (rec x))))))
  (label 125)
  (parent 120)
  (unrealized (3 1) (4 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y x (rec x-0)))
    (x x-0))
  (deflistener (cat (exp (gen) x-0) (mul y x (rec x-0) (rec x-0))))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((0 3) (3 3)) ((1 1) (0 2))
    ((2 0) (0 0)) ((2 2) (1 0)) ((3 0) (4 0)) ((3 4) (0 4))
    ((4 1) (3 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (displaced 5 3 init 1) (exp (gen) x-1) (4 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0)))
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) x-0) (mul y x (rec x-0) (rec x-0))))
      (send (cat (exp (gen) x-0) (mul y x (rec x-0) (rec x-0))))))
  (label 126)
  (parent 120)
  (unrealized (3 1) (4 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 a-1 b-2 name) (y x x-0 x-1 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul y x (rec x-0)))
    (x x-0))
  (deflistener (cat (exp (gen) x-1) (mul y x (rec x-0) (rec x-1))))
  (defstrand init 1 (a a-1) (b b-2) (x x-1))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((0 3) (3 3)) ((1 1) (0 2))
    ((2 0) (0 0)) ((2 2) (1 0)) ((3 0) (4 0)) ((3 4) (0 4))
    ((4 1) (3 1)) ((5 0) (4 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen y x x-0 x-1)
  (uniq-orig n)
  (operation nonce-test (added-strand init 1) (exp (gen) x-1) (4 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x-0) (exp (gen) (mul y x (rec x-0)))
          (pubk a-0)))
      (send (enc (exp (gen) (mul y x (rec x-0))) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x)))) (send n))
    ((recv (cat (exp (gen) x-1) (mul y x (rec x-0) (rec x-1))))
      (send (cat (exp (gen) x-1) (mul y x (rec x-0) (rec x-1)))))
    ((send (enc (exp (gen) x-1) a-1 (pubk b-2)))))
  (label 127)
  (parent 120)
  (unrealized (3 1) (4 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (gen) (mul y x)))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 0) (0 0))
    ((2 2) (1 0)) ((3 1) (0 4)) ((4 1) (3 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (contracted (y-0 y) (x-0 x) (w (mul y x))) (gen)
    (4 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (gen) (mul y x))) (send (cat (gen) (mul y x)))))
  (label 128)
  (parent 121)
  (unrealized (3 0) (4 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 name) (x y rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (deflistener (exp (gen) (mul x y)))
  (deflistener (cat (exp (gen) y) x))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 0) (0 0))
    ((2 2) (1 0)) ((3 1) (0 4)) ((4 1) (3 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen x y)
  (uniq-orig n)
  (operation nonce-test (displaced 5 0 resp 2) (exp (gen) y-0) (4 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul x y)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((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 129)
  (parent 121)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 b-1 a-0 name) (x expt) (y x-0 y-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x-0))
  (deflistener (exp (gen) (mul y x-0)))
  (deflistener (cat (exp (gen) y-0) (mul y x-0 (rec y-0))))
  (defstrand resp 2 (b b-1) (a a-0) (x x) (y y-0))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 0) (0 0))
    ((2 2) (1 0)) ((3 1) (0 4)) ((4 1) (3 0)) ((5 1) (4 0)))
  (absent (y-0 (exp (gen) x)) (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen y x-0 y-0)
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (4 0))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x-0) a (pubk b-0)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((recv (exp (gen) (mul y x-0))) (send (exp (gen) (mul y x-0))))
    ((recv (cat (exp (gen) y-0) (mul y x-0 (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y x-0 (rec y-0)))))
    ((recv (enc (exp (gen) x) a-0 (pubk b-1)))
      (send (enc (exp (gen) x) (exp (gen) y-0) (pubk a-0)))))
  (label 130)
  (parent 121)
  (unrealized (3 0) (4 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 name) (y x rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x) y))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 0) (0 0))
    ((2 2) (1 0)) ((3 1) (0 4)) ((4 1) (3 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (displaced 5 2 init 1) (exp (gen) x-0) (4 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((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 131)
  (parent 121)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (y x x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x))
  (deflistener (exp (gen) (mul y x)))
  (deflistener (cat (exp (gen) x-0) (mul y x (rec x-0))))
  (defstrand init 1 (a a-0) (b b-1) (x x-0))
  (precedes ((0 1) (2 1)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 0) (0 0))
    ((2 2) (1 0)) ((3 1) (0 4)) ((4 1) (3 0)) ((5 0) (4 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (added-strand init 1) (exp (gen) x-0) (4 0))
  (traces
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x) a (pubk b-0)))
      (recv (enc (exp (gen) x) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((recv (exp (gen) (mul y x))) (send (exp (gen) (mul y x))))
    ((recv (cat (exp (gen) x-0) (mul y x (rec x-0))))
      (send (cat (exp (gen) x-0) (mul y x (rec x-0)))))
    ((send (enc (exp (gen) x-0) a-0 (pubk b-1)))))
  (label 132)
  (parent 121)
  (unrealized (3 0) (4 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 a-0 b-1 name) (x y x-0 rndx))
  (defstrand resp 5 (n n) (b b) (a a) (x x-0) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b-0) (y y) (x x-0))
  (defstrand init 5 (n n) (a a-0) (b b-1) (y (mul (rec x) y x-0)) (x x))
  (deflistener (cat (exp (gen) y) (mul (rec x) x-0)))
  (precedes ((0 1) (2 1)) ((0 3) (3 3)) ((1 1) (0 2)) ((2 0) (0 0))
    ((2 2) (1 0)) ((2 2) (4 0)) ((3 0) (4 0)) ((3 4) (0 4))
    ((4 1) (3 1)))
  (absent (y (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (4 0) (1 0))
  (uniq-gen x y x-0)
  (uniq-orig n)
  (operation nonce-test (displaced 5 2 init 3) (exp (gen) y) (4 0)
    (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
  (traces
    ((recv (enc (exp (gen) x-0) a (pubk b)))
      (send (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))
      (send (enc n (exp (gen) (mul y x-0)))) (recv n))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one))))
    ((send (enc (exp (gen) x-0) a (pubk b-0)))
      (recv (enc (exp (gen) x-0) (exp (gen) y) (pubk a)))
      (send (enc (exp (gen) y) (pubk b-0))))
    ((send (enc (exp (gen) x) a-0 (pubk b-1)))
      (recv
        (enc (exp (gen) x) (exp (gen) (mul (rec x) y x-0)) (pubk a-0)))
      (send (enc (exp (gen) (mul (rec x) y x-0)) (pubk b-1)))
      (recv (enc n (exp (gen) (mul y x-0)))) (send n))
    ((recv (cat (exp (gen) y) (mul (rec x) x-0)))
      (send (cat (exp (gen) y) (mul (rec x) x-0)))))
  (label 133)
  (parent 123)
  (unrealized (3 1) (4 0))
  (comment "empty cohort"))

(comment "Nothing left to do")