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

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

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

(defskeleton dhnsl
  (vars (n text) (a b name) (h2 base) (x y expn))
  (defstrand init 5 (n n) (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)))
  (ind-zero-in (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (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 n (exp h2 x))) (send n))
    ((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) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b name) (x y expn))
  (defstrand init 5 (n n) (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)))
  (ind-zero-in (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (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 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 2)
  (parent 1)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (b a name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (h2 (exp (gen) y)) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (h1 (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 3) (0 3)))
  (ind-zero-in (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 3)
  (parent 2)
  (unrealized (1 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (h2 (exp (gen) y)) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) 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)))
  (ind-zero-in (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 4)
  (parent 2)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (b a name) (y x expn))
  (defstrand init 5 (n n) (a a) (b b) (h2 (exp (gen) y)) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (h1 (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3)))
  (ind-zero-in (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 5)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (h2 (exp (gen) y)) (x x) (n n))))
  (origs (n (1 3))))

(comment "Nothing left to do")

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

(defskeleton dhnsl
  (vars (n text) (a b name) (y x expn))
  (defstrand resp 5 (n n) (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 0) (0 0)) ((1 2) (0 2)))
  (ind-zero-in (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 7)
  (parent 6)
  (unrealized (0 4))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y x expn))
  (defstrand resp 5 (n n) (b b) (a a) (h1 (exp (gen) x)) (y y))
  (defstrand init 5 (n n) (a a) (b b) (h2 (exp (gen) y)) (x x))
  (precedes ((0 1) (1 1)) ((0 3) (1 3)) ((1 0) (0 0)) ((1 2) (0 2))
    ((1 4) (0 4)))
  (ind-zero-in (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 8)
  (parent 7)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (h1 (exp (gen) 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 expn))
  (defstrand resp 5 (n n) (b b) (a a) (h1 (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b) (h2 (exp (gen) y)) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-0)
    (h2 (exp (gen) (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)))
  (ind-zero-in (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 9)
  (parent 7)
  (unrealized (2 1))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (n text) (a b name) (y x expn))
  (defstrand resp 5 (n n) (b b) (a a) (h1 (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b) (h2 (exp (gen) 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)))
  (ind-zero-in (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 10)
  (parent 7)
  (unrealized (2 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

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

(defskeleton dhns
  (vars (n text) (a b name) (h2 base) (x y expn))
  (defstrand init 5 (n n) (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)))
  (ind-zero-in (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (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 (pubk a))) (send (enc h2 (pubk b)))
      (recv (enc n (exp h2 x))) (send n))
    ((recv (enc (exp (gen) x) a (pubk b)))
      (send (enc (exp (gen) x) (exp (gen) y) (pubk a)))))
  (label 12)
  (parent 11)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b name) (x y expn))
  (defstrand init 5 (n n) (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)))
  (ind-zero-in (y (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (uniq-gen x y)
  (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) (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 13)
  (parent 12)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhns
  (vars (n text) (b a name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (h2 (exp (gen) y)) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (h1 (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((1 3) (0 3)))
  (ind-zero-in (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 14)
  (parent 13)
  (unrealized (1 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhns
  (vars (n text) (a b name) (x y expn))
  (defstrand init 5 (n n) (a a) (b b) (h2 (exp (gen) y)) (x x))
  (defstrand resp 2 (b b) (a a) (h1 (exp (gen) 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)))
  (ind-zero-in (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 15)
  (parent 13)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (b a name) (y x expn))
  (defstrand init 5 (n n) (a a) (b b) (h2 (exp (gen) y)) (x x))
  (defstrand resp 4 (n n) (b b) (a a) (h1 (exp (gen) x)) (y y))
  (precedes ((0 0) (1 0)) ((0 2) (1 2)) ((1 1) (0 1)) ((1 3) (0 3)))
  (ind-zero-in (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 16)
  (parent 14)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (h2 (exp (gen) y)) (x x) (n n))))
  (origs (n (1 3))))

(comment "Nothing left to do")

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

(defskeleton dhns
  (vars (n text) (a b b-0 name) (y x expn))
  (defstrand resp 5 (n n) (b b) (a a) (h1 (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h2 (exp (gen) y)) (x x))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (ind-zero-in (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 18)
  (parent 17)
  (unrealized (0 4))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dhns
  (vars (n text) (b a b-0 name) (y x expn))
  (defstrand resp 5 (n n) (b b) (a a) (h1 (exp (gen) x)) (y y))
  (defstrand init 5 (n n) (a a) (b b-0) (h2 (exp (gen) y)) (x x))
  (precedes ((0 1) (1 1)) ((0 3) (1 3)) ((1 0) (0 0)) ((1 2) (0 2))
    ((1 4) (0 4)))
  (ind-zero-in (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 19)
  (parent 18)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (h1 (exp (gen) 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 expn))
  (defstrand resp 5 (n n) (b b) (a a) (h1 (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h2 (exp (gen) y)) (x x))
  (defstrand init 5 (n n) (a a-0) (b b-1)
    (h2 (exp (gen) (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)))
  (ind-zero-in (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 20)
  (parent 18)
  (unrealized (2 1))
  (comment "empty cohort"))

(defskeleton dhns
  (vars (n text) (a b b-0 name) (y x expn))
  (defstrand resp 5 (n n) (b b) (a a) (h1 (exp (gen) x)) (y y))
  (defstrand init 3 (a a) (b b-0) (h2 (exp (gen) 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)))
  (ind-zero-in (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 21)
  (parent 18)
  (unrealized (2 0))
  (comment "empty cohort"))

(comment "Nothing left to do")