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

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

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

(defskeleton dhnsl
  (vars (a b name) (y expt) (y-0 x rndx))
  (defstrand init 3 (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 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 (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))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (y expt) (x rndx) (w expt))
  (defstrand init 3 (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 (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 rndx))
  (defstrand init 3 (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)
  (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 (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) (y y) (x x))))
  (origs))

(defskeleton dhnsl
  (vars (a b name) (y expt) (y-0 x rndx) (w expt))
  (defstrand init 3 (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 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 (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 (a b name) (y expt) (x rndx))
  (defstrand init 3 (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 (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) (y x expt) (x-0 y-0 rndx))
  (defstrand init 3 (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)
  (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 (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) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (y expt) (x rndx))
  (defstrand init 3 (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 (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) (y expt) (x x-0 rndx))
  (defstrand init 3 (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)
  (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 (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) (y expt) (y-0 x rndx))
  (defstrand init 3 (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 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 (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 9)
  (parent 4)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b name) (y expt) (x y-0 rndx))
  (defstrand init 3 (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)
  (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 (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 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) (y expt) (y-0 rndx) (x expt) (x-0 y-1 rndx))
  (defstrand init 3 (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 x-0)
  (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 (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 11)
  (parent 4)
  (unrealized (0 1) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (y expt) (y-0 x rndx))
  (defstrand init 3 (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 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 (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 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) (y expt) (y-0 x x-0 rndx))
  (defstrand init 3 (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 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) (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-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 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) (y x expt) (x-0 y-0 rndx))
  (defstrand init 3 (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))
  (deflistener x-0)
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (1 0)))
  (absent (y-0 (exp (gen) x)))
  (non-orig (privk a) (privk b))
  (precur (1 0))
  (uniq-gen x-0)
  (operation nonce-test (added-listener x-0) (mul x-0 (rec 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 (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))))
    ((recv x-0) (send x-0)))
  (label 14)
  (parent 6)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b name) (y expt) (y-0 x rndx))
  (defstrand init 3 (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 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 (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 15)
  (parent 7)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b a-0 b-0 name) (y expt) (x x-0 rndx))
  (defstrand init 3 (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))
  (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) (exp (gen) y) b (pubk a)))
      (send (enc (exp (gen) y) (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) (y expt) (x y-0 rndx))
  (defstrand init 3 (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))))
  (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-0 (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) (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-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)))))
    ((recv x) (send x)))
  (label 17)
  (parent 10)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b b-0 a-0 name) (y expt) (y-0 rndx) (x expt) (x-0 y-1 rndx))
  (defstrand init 3 (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))
  (deflistener x-0)
  (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-1 (exp (gen) x)) (y-0 (exp (gen) x-0)))
  (non-orig (privk a) (privk b))
  (precur (2 0))
  (uniq-gen x-0)
  (operation nonce-test (added-listener x-0) (mul x-0 (rec 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 (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))))
    ((recv x-0) (send x-0)))
  (label 18)
  (parent 11)
  (unrealized (4 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b name) (y expt) (y-0 y-1 x rndx))
  (defstrand init 3 (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 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 (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 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) (y expt) (y-0 x x-0 rndx))
  (defstrand init 3 (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))
  (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-0 (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) (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-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)))) ((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) (x expt) (y rndx))
    (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))))
    (absent (y (exp (gen) x)))
    (comment "Y and Z should be assumed to be freshly chosen per role"))
  (defrole init
    (vars (a b name) (y expt) (x rndx))
    (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))))
    (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) (x expt) (y rndx))
  (defstrand resp 3 (b b) (a a) (x x) (y y))
  (absent (y (exp (gen) x)))
  (non-orig (privk a))
  (uniq-gen y)
  (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)))))
  (label 21)
  (unrealized (0 2))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (y x rndx))
  (defstrand resp 3 (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 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) (x x) (y y))))
  (origs))

(defskeleton dhnsl
  (vars (a b name) (x expt) (y rndx) (w expt))
  (defstrand resp 3 (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))
  (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 (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) (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) (x expt) (y rndx))
  (defstrand resp 3 (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))
  (uniq-gen y)
  (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))))
    ((recv (cat (gen) y)) (send (cat (gen) y))))
  (label 24)
  (parent 23)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b name) (x expt) (y rndx))
  (defstrand resp 3 (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))
  (precur (1 0))
  (uniq-gen y)
  (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))))
    ((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) (x x-0 expt) (y y-0 rndx))
  (defstrand resp 3 (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))
  (precur (1 0))
  (uniq-gen y)
  (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))))
    ((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 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) (x expt) (y x-0 rndx))
  (defstrand resp 3 (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))
  (precur (1 0))
  (uniq-gen y)
  (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))))
    ((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 27)
  (parent 23)
  (unrealized (0 2) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (a b name) (y x rndx))
  (defstrand resp 3 (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 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) (x x-0 expt) (y y-0 rndx))
  (defstrand resp 3 (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))
  (deflistener y)
  (precedes ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0)) ((3 1) (1 0)))
  (absent (y-0 (exp (gen) x-0)) (y (exp (gen) x)))
  (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 (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-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))))
    ((recv y) (send y)))
  (label 29)
  (parent 26)
  (unrealized (3 0))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (a b a-0 b-0 name) (x expt) (y x-0 rndx))
  (defstrand resp 3 (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))
  (deflistener y)
  (precedes ((0 1) (3 0)) ((1 1) (0 2)) ((2 0) (1 0)) ((3 1) (1 0)))
  (absent (y (exp (gen) x)))
  (non-orig (privk a))
  (precur (1 0))
  (uniq-gen y)
  (operation nonce-test (added-listener y) (mul y (rec 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))))
    ((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)))) ((recv y) (send y)))
  (label 30)
  (parent 27)
  (unrealized (3 0))
  (comment "empty cohort"))

(comment "Nothing left to do")