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

(comment "CPSA 3.6.8")
(comment "All input read from tst/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))
  (dead)
  (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))
  (dead)
  (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))
  (dead)
  (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 "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))
  (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))
  (dead)
  (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))
  (dead)
  (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))
  (dead)
  (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))
  (dead)
  (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))
  (dead)
  (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))
  (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) 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)
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (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) x) y)) (send (cat (exp (gen) x) y))))
  (label 19)
  (parent 10)
  (unrealized (3 0))
  (dead)
  (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))
  (uniq-gen x y)
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (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) y) x)) (send (cat (exp (gen) y) x))))
  (label 20)
  (parent 10)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(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 21)
  (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 22)
  (parent 18)
  (unrealized (2 0))
  (dead)
  (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 23)
  (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 24)
  (parent 18)
  (unrealized (1 2) (2 0))
  (dead)
  (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 25)
  (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 26)
  (parent 18)
  (unrealized (1 2) (2 0))
  (dead)
  (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 27)
  (parent 23)
  (unrealized (2 0))
  (dead)
  (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 28)
  (parent 25)
  (unrealized (1 2) (2 0))
  (dead)
  (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 29)
  (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 30)
  (parent 29)
  (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 31)
  (parent 29)
  (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 32)
  (parent 30)
  (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 33)
  (parent 30)
  (unrealized (2 1))
  (comment "3 in cohort - 3 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 34)
  (parent 30)
  (unrealized (2 0))
  (comment "2 in cohort - 2 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 35)
  (parent 31)
  (unrealized (1 0))
  (dead)
  (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 36)
  (parent 31)
  (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 37)
  (parent 31)
  (unrealized (0 2) (0 4) (1 0))
  (dead)
  (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 38)
  (parent 31)
  (unrealized (0 2) (0 4) (1 0))
  (dead)
  (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 (exp (gen) (mul y 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)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (added-listener (cat (exp (gen) (mul y x)) x-0))
    (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)) x-0))
      (send (cat (exp (gen) (mul y x)) x-0))))
  (label 39)
  (parent 33)
  (unrealized (3 0))
  (dead)
  (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 (exp (gen) (mul y (rec x-0))) 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)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y (rec x-0))) x))
    (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 (rec x-0))) x))
      (send (cat (exp (gen) (mul y (rec x-0))) x))))
  (label 40)
  (parent 33)
  (unrealized (3 0))
  (dead)
  (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 (exp (gen) (mul x (rec x-0))) y))
  (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)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x (rec x-0))) y))
    (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 x (rec x-0))) y))
      (send (cat (exp (gen) (mul x (rec x-0))) y))))
  (label 41)
  (parent 33)
  (unrealized (3 0))
  (dead)
  (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) 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)
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (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) y) x)) (send (cat (exp (gen) y) x))))
  (label 42)
  (parent 34)
  (unrealized (3 0))
  (dead)
  (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))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (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) x) y)) (send (cat (exp (gen) x) y))))
  (label 43)
  (parent 34)
  (unrealized (3 0))
  (dead)
  (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))
  (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 44)
  (parent 36)
  (unrealized (0 4) (1 0))
  (dead)
  (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 45)
  (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 46)
  (parent 45)
  (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 47)
  (parent 45)
  (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 48)
  (parent 46)
  (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 49)
  (parent 46)
  (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 50)
  (parent 47)
  (unrealized (1 0))
  (dead)
  (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 51)
  (parent 47)
  (unrealized (0 1) (0 3) (1 0))
  (dead)
  (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 52)
  (parent 47)
  (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 53)
  (parent 47)
  (unrealized (0 1) (0 3) (1 0))
  (dead)
  (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 54)
  (parent 48)
  (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 55)
  (parent 48)
  (unrealized (2 0))
  (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))
  (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 56)
  (parent 49)
  (unrealized (2 0))
  (dead)
  (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 57)
  (parent 49)
  (unrealized (0 1) (0 3) (2 0))
  (dead)
  (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 58)
  (parent 49)
  (unrealized (0 1) (0 3) (2 0))
  (dead)
  (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 59)
  (parent 49)
  (seen 61)
  (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 60)
  (parent 49)
  (unrealized (0 1) (0 3) (2 0))
  (dead)
  (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 61)
  (parent 52)
  (unrealized (1 0))
  (dead)
  (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 62)
  (parent 54)
  (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 63)
  (parent 54)
  (unrealized (2 0))
  (comment "5 in cohort - 5 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)))
  (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))
  (uniq-gen x y)
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (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) x) y)) (send (cat (exp (gen) x) y))))
  (label 64)
  (parent 55)
  (unrealized (3 0))
  (dead)
  (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))
  (uniq-gen x y)
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (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) y) x)) (send (cat (exp (gen) y) x))))
  (label 65)
  (parent 55)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(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 66)
  (parent 59)
  (seen 61)
  (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 67)
  (parent 63)
  (unrealized (2 0))
  (dead)
  (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 68)
  (parent 63)
  (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 69)
  (parent 63)
  (unrealized (1 2) (2 0))
  (dead)
  (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 70)
  (parent 63)
  (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 71)
  (parent 63)
  (unrealized (1 2) (2 0))
  (dead)
  (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 72)
  (parent 68)
  (unrealized (2 0))
  (dead)
  (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 73)
  (parent 70)
  (unrealized (1 2) (2 0))
  (dead)
  (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 74)
  (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 75)
  (parent 74)
  (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 76)
  (parent 74)
  (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 77)
  (parent 75)
  (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 78)
  (parent 75)
  (unrealized (2 1))
  (comment "3 in cohort - 3 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 79)
  (parent 75)
  (unrealized (2 0))
  (comment "2 in cohort - 2 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 80)
  (parent 76)
  (unrealized (1 0))
  (dead)
  (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 81)
  (parent 76)
  (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 82)
  (parent 76)
  (unrealized (0 2) (0 4) (1 0))
  (dead)
  (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 83)
  (parent 76)
  (unrealized (0 2) (0 4) (1 0))
  (dead)
  (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) (mul y 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)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (added-listener (cat (exp (gen) (mul y x)) x-0))
    (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)) x-0))
      (send (cat (exp (gen) (mul y x)) x-0))))
  (label 84)
  (parent 78)
  (unrealized (3 0))
  (dead)
  (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) (mul y (rec x-0))) 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)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y (rec x-0))) x))
    (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 (rec x-0))) x))
      (send (cat (exp (gen) (mul y (rec x-0))) x))))
  (label 85)
  (parent 78)
  (unrealized (3 0))
  (dead)
  (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) (mul x (rec x-0))) y))
  (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)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x (rec x-0))) y))
    (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 x (rec x-0))) y))
      (send (cat (exp (gen) (mul x (rec x-0))) y))))
  (label 86)
  (parent 78)
  (unrealized (3 0))
  (dead)
  (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) 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)
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (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) y) x)) (send (cat (exp (gen) y) x))))
  (label 87)
  (parent 79)
  (unrealized (3 0))
  (dead)
  (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))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (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) x) y)) (send (cat (exp (gen) x) y))))
  (label 88)
  (parent 79)
  (unrealized (3 0))
  (dead)
  (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))
  (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 89)
  (parent 81)
  (unrealized (0 4))
  (comment "3 in cohort - 3 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))
  (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 90)
  (parent 89)
  (seen 77)
  (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 91)
  (parent 89)
  (unrealized (3 1))
  (comment "3 in cohort - 3 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 92)
  (parent 89)
  (unrealized (3 0))
  (comment "2 in cohort - 2 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 (exp (gen) (mul y 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)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test (added-listener (cat (exp (gen) (mul y x)) x-0))
    (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)) x-0))
      (send (cat (exp (gen) (mul y x)) x-0))))
  (label 93)
  (parent 91)
  (unrealized (4 0))
  (dead)
  (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) (mul y (rec x-0))) 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)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y (rec x-0))) x))
    (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 (rec x-0))) x))
      (send (cat (exp (gen) (mul y (rec x-0))) x))))
  (label 94)
  (parent 91)
  (unrealized (4 0))
  (dead)
  (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) (mul x (rec x-0))) y))
  (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 (1 0))
  (uniq-gen y x x-0)
  (uniq-orig n)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x (rec x-0))) y))
    (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 x (rec x-0))) y))
      (send (cat (exp (gen) (mul x (rec x-0))) y))))
  (label 95)
  (parent 91)
  (unrealized (4 0))
  (dead)
  (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) 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 (1 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-listener (cat (exp (gen) y) x))
    (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) y) x)) (send (cat (exp (gen) y) x))))
  (label 96)
  (parent 92)
  (unrealized (4 0))
  (dead)
  (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 (1 0))
  (uniq-gen y x)
  (uniq-orig n)
  (operation nonce-test (added-listener (cat (exp (gen) x) y))
    (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) x) y)) (send (cat (exp (gen) x) y))))
  (label 97)
  (parent 92)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")