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

(comment "CPSA 3.4.0")
(comment "All input read from dhnsl_basic.scm")

(defprotocol dhnsl diffie-hellman
  (defrole resp
    (vars (b a name) (h1 base) (y expn))
    (trace (recv (enc h1 a (pubk b)))
      (send (enc h1 (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b))))
    (absent (y h1))
    (comment "Y and Z should be assumed to be freshly chosen per role"))
  (defrole init
    (vars (a b name) (h2 base) (x expn))
    (trace (send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) h2 b (pubk a))) (send (enc h2 (pubk b))))
    (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 (a b name) (h2 base) (x expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (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) h2 b (pubk a)))
      (send (enc h2 (pubk b)))))
  (label 0)
  (unrealized (0 1))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (h2 base) (x y expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) 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)
  (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) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))))
  (label 1)
  (parent 0)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (h2 base) (x expn) (w expr))
  (defstrand init 3 (a a) (b b) (h2 h2) (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) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((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 (a b name) (x y expn))
  (defstrand init 3 (a a) (b b) (h2 (exp (gen) y)) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) 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)
  (operation nonce-test (contracted (h2 (exp (gen) 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 (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))))
  (label 3)
  (parent 1)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (h2 (exp (gen) y)) (x x))))
  (origs))

(defskeleton dhnsl
  (vars (a b name) (h2 base) (x y expn) (w expr))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (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 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen 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) b (pubk a)))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) 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 (a b name) (h2 base) (x expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (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) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (cat (gen) x)) (send (cat (gen) x))))
  (label 5)
  (parent 2)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b b-0 a-0 name) (h2 h1 base) (x y expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (deflistener (cat (exp (gen) y) (mul x (rec y))))
  (defstrand resp 2 (b b-0) (a a-0) (h1 h1) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (absent (y h1))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen x)
  (operation nonce-test (added-strand resp 2) (exp (gen) y) (1 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (cat (exp (gen) y) (mul x (rec y))))
      (send (cat (exp (gen) y) (mul x (rec y)))))
    ((recv (enc h1 a-0 (pubk b-0)))
      (send (enc h1 (exp (gen) y) b-0 (pubk a-0)))))
  (label 6)
  (parent 2)
  (unrealized (0 1) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (h2 base) (x expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (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) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((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 (a b a-0 b-0 name) (h2 base) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (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)
  (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) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((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) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (h2 base) (y x expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (deflistener (cat (gen) x))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen 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) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a))))
    ((recv (cat (gen) x)) (send (cat (gen) x))))
  (label 9)
  (parent 4)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b name) (h2 base) (x y expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (deflistener (cat (exp (gen) y) (mul x (rec y))))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (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) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a))))
    ((recv (cat (exp (gen) y) (mul x (rec y))))
      (send (cat (exp (gen) y) (mul x (rec y))))))
  (label 10)
  (parent 4)
  (unrealized (0 1) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (a b b-0 a-0 name) (h2 h1 base) (y x y-0 expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (deflistener (cat (exp (gen) y-0) (mul x (rec y-0))))
  (defstrand resp 2 (b b-0) (a a-0) (h1 h1) (y y-0))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (absent (y-0 h1) (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (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) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) 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)))))
    ((recv (enc h1 a-0 (pubk b-0)))
      (send (enc h1 (exp (gen) y-0) b-0 (pubk a-0)))))
  (label 11)
  (parent 4)
  (unrealized (0 1) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (h2 base) (y x expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (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 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen 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) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a))))
    ((recv (cat (exp (gen) x) (one))) (send (cat (exp (gen) x) (one)))))
  (label 12)
  (parent 4)
  (seen 15)
  (unrealized (2 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (a b a-0 b-0 name) (h2 base) (y x x-0 expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (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 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (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) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) 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 13)
  (parent 4)
  (unrealized (0 1) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton dhnsl
  (vars (a b name) (h2 base) (x y expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (deflistener (cat (exp (gen) x) (one)))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen 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) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((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) b (pubk a)))))
  (label 15)
  (parent 7)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b a-0 b-0 name) (h2 base) (x x-0 expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (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))
  (deflistener x)
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 0) (1 0)) ((3 1) (1 0)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen x)
  (operation nonce-test (added-listener x) (mul x (rec x-0)) (1 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((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)))) ((recv x) (send x)))
  (label 16)
  (parent 8)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b name) (h2 base) (x y expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (deflistener (cat (exp (gen) y) (mul x (rec y))))
  (deflistener x)
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (2 0)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (added-listener x) (mul x (rec y)) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a))))
    ((recv (cat (exp (gen) y) (mul x (rec y))))
      (send (cat (exp (gen) y) (mul x (rec y))))) ((recv x) (send x)))
  (label 17)
  (parent 10)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b b-0 a-0 name) (h2 h1 base) (y x y-0 expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (deflistener (cat (exp (gen) y-0) (mul x (rec y-0))))
  (defstrand resp 2 (b b-0) (a a-0) (h1 h1) (y y-0))
  (deflistener x)
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)) ((4 1) (2 0)))
  (absent (y-0 h1) (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (added-listener x) (mul x (rec y-0)) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) 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)))))
    ((recv (enc h1 a-0 (pubk b-0)))
      (send (enc h1 (exp (gen) y-0) b-0 (pubk a-0))))
    ((recv x) (send x)))
  (label 18)
  (parent 11)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b name) (h2 base) (y x y-0 expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (deflistener (cat (exp (gen) x) (one)))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) x)) (y y-0))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (absent (y-0 (exp (gen) x)) (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen 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) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) 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-0) b (pubk a)))))
  (label 19)
  (parent 12)
  (seen 15)
  (unrealized (2 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dhnsl
  (vars (a b a-0 b-0 name) (h2 base) (y x x-0 expn))
  (defstrand init 3 (a a) (b b) (h2 h2) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (deflistener (cat (exp (gen) x-0) (mul x (rec x-0))))
  (defstrand init 1 (a a-0) (b b-0) (x x-0))
  (deflistener x)
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (2 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x)
  (operation nonce-test (added-listener x) (mul x (rec x-0)) (2 0))
  (traces
    ((send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) h2 b (pubk a))) (send (enc h2 (pubk b))))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) 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)))) ((recv x) (send x)))
  (label 20)
  (parent 13)
  (unrealized (4 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhnsl diffie-hellman
  (defrole resp
    (vars (b a name) (h1 base) (y expn))
    (trace (recv (enc h1 a (pubk b)))
      (send (enc h1 (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b))))
    (absent (y h1))
    (comment "Y and Z should be assumed to be freshly chosen per role"))
  (defrole init
    (vars (a b name) (h2 base) (x expn))
    (trace (send (enc (exp (gen) x) a (pubk b)))
      (recv (enc (exp (gen) x) h2 b (pubk a))) (send (enc h2 (pubk b))))
    (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 (a b name) (h1 base) (y expn))
  (defstrand resp 3 (b b) (a a) (h1 h1) (y y))
  (absent (y h1))
  (non-orig (privk a))
  (uniq-gen y)
  (comment "Responder point-of-view")
  (traces
    ((recv (enc h1 a (pubk b))) (send (enc h1 (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b)))))
  (label 21)
  (unrealized (0 2))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (y x expn))
  (defstrand resp 3 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b) (h2 (exp (gen) y)) (x x))
  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a))
  (uniq-gen y)
  (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 (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 22)
  (parent 21)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (h1 (exp (gen) x)) (y y))))
  (origs))

(defskeleton dhnsl
  (vars (a b name) (h1 base) (y expn) (w expr))
  (defstrand resp 3 (b b) (a a) (h1 h1) (y y))
  (deflistener (cat (exp (gen) (mul y (rec w))) w))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (absent (y h1))
  (non-orig (privk a))
  (uniq-gen y)
  (precur (1 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y (rec w))) w)) (exp (gen) y)
    (0 2) (enc h1 (exp (gen) y) b (pubk a)))
  (traces
    ((recv (enc h1 a (pubk b))) (send (enc h1 (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b))))
    ((recv (cat (exp (gen) (mul y (rec w))) w))
      (send (cat (exp (gen) (mul y (rec w))) w))))
  (label 23)
  (parent 21)
  (unrealized (1 0))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (h1 base) (y expn))
  (defstrand resp 3 (b b) (a a) (h1 h1) (y y))
  (deflistener (cat (gen) y))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (absent (y h1))
  (non-orig (privk a))
  (uniq-gen y)
  (precur (1 0))
  (operation nonce-test (contracted (y-0 y) (w y)) (gen) (1 0))
  (traces
    ((recv (enc h1 a (pubk b))) (send (enc h1 (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b))))
    ((recv (cat (gen) y)) (send (cat (gen) y))))
  (label 24)
  (parent 23)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b name) (h1 base) (y expn))
  (defstrand resp 3 (b b) (a a) (h1 h1) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (absent (y h1))
  (non-orig (privk a))
  (precur (1 0))
  (uniq-gen y)
  (operation nonce-test (displaced 2 0 resp 2) (exp (gen) y-0) (1 0))
  (traces
    ((recv (enc h1 a (pubk b))) (send (enc h1 (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b))))
    ((recv (cat (exp (gen) y) (one))) (send (cat (exp (gen) y) (one)))))
  (label 25)
  (parent 23)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (a b b-0 a-0 name) (h1 h1-0 base) (y y-0 expn))
  (defstrand resp 3 (b b) (a a) (h1 h1) (y y))
  (deflistener (cat (exp (gen) y-0) (mul y (rec y-0))))
  (defstrand resp 2 (b b-0) (a a-0) (h1 h1-0) (y y-0))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (absent (y-0 h1-0) (y h1))
  (non-orig (privk a))
  (precur (1 0))
  (uniq-gen y)
  (operation nonce-test (added-strand resp 2) (exp (gen) y-0) (1 0))
  (traces
    ((recv (enc h1 a (pubk b))) (send (enc h1 (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b))))
    ((recv (cat (exp (gen) y-0) (mul y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y (rec y-0)))))
    ((recv (enc h1-0 a-0 (pubk b-0)))
      (send (enc h1-0 (exp (gen) y-0) b-0 (pubk a-0)))))
  (label 26)
  (parent 23)
  (unrealized (0 2) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (a b a-0 b-0 name) (h1 base) (y x expn))
  (defstrand resp 3 (b b) (a a) (h1 h1) (y y))
  (deflistener (cat (exp (gen) x) (mul y (rec x))))
  (defstrand init 1 (a a-0) (b b-0) (x x))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  (absent (y h1))
  (non-orig (privk a))
  (precur (1 0))
  (uniq-gen y)
  (operation nonce-test (added-strand init 1) (exp (gen) x) (1 0))
  (traces
    ((recv (enc h1 a (pubk b))) (send (enc h1 (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b))))
    ((recv (cat (exp (gen) x) (mul y (rec x))))
      (send (cat (exp (gen) x) (mul y (rec x)))))
    ((send (enc (exp (gen) x) a-0 (pubk b-0)))))
  (label 27)
  (parent 23)
  (unrealized (0 2) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (y x expn))
  (defstrand resp 3 (b b) (a a) (h1 (exp (gen) x)) (y y))
  (deflistener (cat (exp (gen) y) (one)))
  (defstrand init 3 (a a) (b b) (h2 (exp (gen) y)) (x x))
  (precedes ((0 1) (2 1)) ((1 1) (0 2)) ((2 2) (1 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a))
  (precur (1 0))
  (uniq-gen y)
  (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))))
    ((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 28)
  (parent 25)
  (seen 22)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dhnsl
  (vars (a b b-0 a-0 name) (h1 h1-0 base) (y y-0 expn))
  (defstrand resp 3 (b b) (a a) (h1 h1) (y y))
  (deflistener (cat (exp (gen) y-0) (mul y (rec y-0))))
  (defstrand resp 2 (b b-0) (a a-0) (h1 h1-0) (y y-0))
  (deflistener y)
  (precedes ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0)) ((3 1) (1 0)))
  (absent (y-0 h1-0) (y h1))
  (non-orig (privk a))
  (precur (1 0))
  (uniq-gen y)
  (operation nonce-test (added-listener y) (mul y (rec y-0)) (1 0))
  (traces
    ((recv (enc h1 a (pubk b))) (send (enc h1 (exp (gen) y) b (pubk a)))
      (recv (enc (exp (gen) y) (pubk b))))
    ((recv (cat (exp (gen) y-0) (mul y (rec y-0))))
      (send (cat (exp (gen) y-0) (mul y (rec y-0)))))
    ((recv (enc h1-0 a-0 (pubk b-0)))
      (send (enc h1-0 (exp (gen) y-0) b-0 (pubk a-0))))
    ((recv y) (send y)))
  (label 29)
  (parent 26)
  (unrealized (3 0))
  (comment "empty cohort"))

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

(comment "Nothing left to do")