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

(comment "CPSA 4.4.7")
(comment "All input read from tst/dhnsl_hack.scm")

(defprotocol dhnsl basic
  (defrole init
    (vars (a b name) (h2 h3 gx akey) (dhkey skey))
    (trace (send (enc gx a (pubk b)))
      (recv (enc h2 (enc "dh" h2 gx dhkey) h3 b (pubk a)))
      (send (enc (enc "dh" h3 gx dhkey) (pubk b))))
    (non-orig dhkey (invk gx))
    (uniq-orig gx)
    (comment "X should be assumed to be freshly chosen per role"))
  (defrole resp
    (vars (b a name) (h1 gy gz akey) (dhkey skey))
    (trace (recv (enc h1 a (pubk b)))
      (send (enc gy (enc "dh" gy h1 dhkey) gz b (pubk a)))
      (recv (enc (enc "dh" gz h1 dhkey) (pubk b))))
    (non-orig dhkey (invk gy) (invk gz))
    (uniq-orig gy gz)
    (comment "Y and Z should be assumed to be freshly chosen per role"))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (comment
    "Needham-Schroeder-Lowe DH challenge/responses in place of nonces"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz akey) (a b name))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gz) (gx gx) (a a) (b b))
  (non-orig dhkey (invk gx) (privk a) (privk b))
  (uniq-orig gx)
  (comment "Initiator point-of-view")
  (traces
    ((send (enc gx a (pubk b)))
      (recv (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b)))))
  (label 0)
  (unrealized (0 1))
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (origs (gx (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz gz-0 akey) (a b b-0 a-0 name))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gz) (gx gx) (a a) (b b))
  (defstrand resp 2 (dhkey dhkey) (h1 gx) (gy gy) (gz gz-0) (b b-0)
    (a a-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig dhkey (invk gx) (invk gy) (invk gz-0) (privk a) (privk b))
  (uniq-orig gx gy gz-0)
  (comment "Initiator point-of-view")
  (operation encryption-test (added-strand resp 2)
    (enc "dh" gy gx dhkey) (0 1))
  (strand-map 0)
  (traces
    ((send (enc gx a (pubk b)))
      (recv (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b))))
    ((recv (enc gx a-0 (pubk b-0)))
      (send (enc gy (enc "dh" gy gx dhkey) gz-0 b-0 (pubk a-0)))))
  (label 1)
  (parent 0)
  (unrealized (1 0))
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz gz-0 akey) (a b name))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gz) (gx gx) (a a) (b b))
  (defstrand resp 2 (dhkey dhkey) (h1 gx) (gy gy) (gz gz-0) (b b) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig dhkey (invk gx) (invk gy) (invk gz-0) (privk a) (privk b))
  (uniq-orig gx gy gz-0)
  (comment "Initiator point-of-view")
  (operation nonce-test (contracted (b-0 b) (a-0 a)) gx (1 0)
    (enc gx a (pubk b)))
  (strand-map 0 1)
  (traces
    ((send (enc gx a (pubk b)))
      (recv (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b))))
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gz-0 b (pubk a)))))
  (label 2)
  (parent 1)
  (unrealized (0 1))
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey dhkey-0 skey) (gx gy gz gz-0 gy-0 gz-1 akey)
    (a b b-0 a-0 name))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gz) (gx gx) (a a) (b b))
  (defstrand resp 2 (dhkey dhkey) (h1 gx) (gy gy) (gz gz-0) (b b-0)
    (a a-0))
  (defstrand resp 2 (dhkey dhkey-0) (h1 gx) (gy gy-0) (gz gz-1) (b b)
    (a a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig dhkey dhkey-0 (invk gx) (invk gy) (invk gz-0) (invk gy-0)
    (invk gz-1) (privk a) (privk b))
  (uniq-orig gx gy gz-0 gy-0 gz-1)
  (comment "Initiator point-of-view")
  (operation nonce-test (added-strand resp 2) gx (1 0)
    (enc gx a (pubk b)))
  (strand-map 0 1)
  (traces
    ((send (enc gx a (pubk b)))
      (recv (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b))))
    ((recv (enc gx a-0 (pubk b-0)))
      (send (enc gy (enc "dh" gy gx dhkey) gz-0 b-0 (pubk a-0))))
    ((recv (enc gx a (pubk b)))
      (send (enc gy-0 (enc "dh" gy-0 gx dhkey-0) gz-1 b (pubk a)))))
  (label 3)
  (parent 1)
  (unrealized (1 0))
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz akey) (a b name))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gz) (gx gx) (a a) (b b))
  (defstrand resp 2 (dhkey dhkey) (h1 gx) (gy gy) (gz gz) (b b) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig dhkey (invk gx) (invk gy) (invk gz) (privk a) (privk b))
  (uniq-orig gx gy gz)
  (comment "Initiator point-of-view")
  (operation encryption-test (contracted (gz-0 gz))
    (enc "dh" gy gx dhkey) (0 1)
    (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
  (strand-map 0 1)
  (traces
    ((send (enc gx a (pubk b)))
      (recv (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b))))
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))))
  (label 4)
  (parent 2)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (origs (gy (1 1)) (gz (1 1)) (gx (0 0))))

(defskeleton dhnsl
  (vars (dhkey dhkey-0 skey) (gx gy gz gz-0 gy-0 gz-1 akey) (a b name))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gz) (gx gx) (a a) (b b))
  (defstrand resp 2 (dhkey dhkey) (h1 gx) (gy gy) (gz gz-0) (b b) (a a))
  (defstrand resp 2 (dhkey dhkey-0) (h1 gx) (gy gy-0) (gz gz-1) (b b)
    (a a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig dhkey dhkey-0 (invk gx) (invk gy) (invk gz-0) (invk gy-0)
    (invk gz-1) (privk a) (privk b))
  (uniq-orig gx gy gz-0 gy-0 gz-1)
  (comment "Initiator point-of-view")
  (operation nonce-test (contracted (b-0 b) (a-0 a)) gx (1 0)
    (enc gx a (pubk b))
    (enc gy-0 (enc "dh" gy-0 gx dhkey-0) gz-1 b (pubk a)))
  (strand-map 0 1 2)
  (traces
    ((send (enc gx a (pubk b)))
      (recv (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b))))
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gz-0 b (pubk a))))
    ((recv (enc gx a (pubk b)))
      (send (enc gy-0 (enc "dh" gy-0 gx dhkey-0) gz-1 b (pubk a)))))
  (label 5)
  (parent 3)
  (unrealized (0 1))
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey dhkey-0 skey) (gx gy gz gy-0 gz-0 akey) (a b name))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gz) (gx gx) (a a) (b b))
  (defstrand resp 2 (dhkey dhkey) (h1 gx) (gy gy) (gz gz) (b b) (a a))
  (defstrand resp 2 (dhkey dhkey-0) (h1 gx) (gy gy-0) (gz gz-0) (b b)
    (a a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig dhkey dhkey-0 (invk gx) (invk gy) (invk gz) (invk gy-0)
    (invk gz-0) (privk a) (privk b))
  (uniq-orig gx gy gz gy-0 gz-0)
  (comment "Initiator point-of-view")
  (operation encryption-test (contracted (gz-1 gz))
    (enc "dh" gy gx dhkey) (0 1)
    (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
  (strand-map 0 1 2)
  (traces
    ((send (enc gx a (pubk b)))
      (recv (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b))))
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gz b (pubk a))))
    ((recv (enc gx a (pubk b)))
      (send (enc gy-0 (enc "dh" gy-0 gx dhkey-0) gz-0 b (pubk a)))))
  (label 6)
  (parent 5)
  (seen 4)
  (seen-ops
    (4 (operation generalization deleted (2 0)) (strand-map 0 1)))
  (realized)
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")

(defprotocol dhnsl basic
  (defrole init
    (vars (a b name) (h2 h3 gx akey) (dhkey skey))
    (trace (send (enc gx a (pubk b)))
      (recv (enc h2 (enc "dh" h2 gx dhkey) h3 b (pubk a)))
      (send (enc (enc "dh" h3 gx dhkey) (pubk b))))
    (non-orig dhkey (invk gx))
    (uniq-orig gx)
    (comment "X should be assumed to be freshly chosen per role"))
  (defrole resp
    (vars (b a name) (h1 gy gz akey) (dhkey skey))
    (trace (recv (enc h1 a (pubk b)))
      (send (enc gy (enc "dh" gy h1 dhkey) gz b (pubk a)))
      (recv (enc (enc "dh" gz h1 dhkey) (pubk b))))
    (non-orig dhkey (invk gy) (invk gz))
    (uniq-orig gy gz)
    (comment "Y and Z should be assumed to be freshly chosen per role"))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (comment
    "Needham-Schroeder-Lowe DH challenge/responses in place of nonces"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz akey) (a b name))
  (defstrand resp 3 (dhkey dhkey) (h1 gx) (gy gy) (gz gz) (b b) (a a))
  (non-orig dhkey (invk gy) (invk gz) (privk a))
  (uniq-orig gy gz)
  (comment "Responder point-of-view")
  (traces
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (recv (enc (enc "dh" gz gx dhkey) (pubk b)))))
  (label 7)
  (unrealized (0 2))
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (origs (gz (0 1)) (gy (0 1)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz h2 akey) (a b a-0 b-0 name))
  (defstrand resp 3 (dhkey dhkey) (h1 gx) (gy gy) (gz gz) (b b) (a a))
  (defstrand init 3 (dhkey dhkey) (h2 h2) (h3 gz) (gx gx) (a a-0)
    (b b-0))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig dhkey (invk gx) (invk gy) (invk gz) (privk a))
  (uniq-orig gx gy gz)
  (comment "Responder point-of-view")
  (operation encryption-test (added-strand init 3)
    (enc "dh" gz gx dhkey) (0 2))
  (strand-map 0)
  (traces
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (recv (enc (enc "dh" gz gx dhkey) (pubk b))))
    ((send (enc gx a-0 (pubk b-0)))
      (recv (enc h2 (enc "dh" h2 gx dhkey) gz b-0 (pubk a-0)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b-0)))))
  (label 8)
  (parent 7)
  (unrealized (1 1))
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy akey) (a b name))
  (defstrand resp 3 (dhkey dhkey) (h1 gx) (gy gy) (gz gy) (b b) (a a))
  (non-orig dhkey (invk gy) (privk a))
  (uniq-orig gy)
  (comment "Responder point-of-view")
  (operation encryption-test (displaced 1 0 resp 2)
    (enc "dh" gz gx dhkey) (0 2))
  (strand-map 0)
  (traces
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gy b (pubk a)))
      (recv (enc (enc "dh" gy gx dhkey) (pubk b)))))
  (label 9)
  (parent 7)
  (unrealized (0 2))
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gy) (dhkey dhkey))))
  (origs (gy (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz akey) (a b a-0 b-0 name))
  (defstrand resp 3 (dhkey dhkey) (h1 gx) (gy gy) (gz gz) (b b) (a a))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gz) (gx gx) (a a-0)
    (b b-0))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig dhkey (invk gx) (invk gy) (invk gz) (privk a))
  (uniq-orig gx gy gz)
  (comment "Responder point-of-view")
  (operation encryption-test (displaced 2 0 resp 2)
    (enc "dh" h2 gx dhkey) (1 1))
  (strand-map 0 1)
  (traces
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (recv (enc (enc "dh" gz gx dhkey) (pubk b))))
    ((send (enc gx a-0 (pubk b-0)))
      (recv (enc gy (enc "dh" gy gx dhkey) gz b-0 (pubk a-0)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b-0)))))
  (label 10)
  (parent 8)
  (unrealized (1 1))
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz h2 gz-0 akey) (a b a-0 b-0 b-1 a-1 name))
  (defstrand resp 3 (dhkey dhkey) (h1 gx) (gy gy) (gz gz) (b b) (a a))
  (defstrand init 3 (dhkey dhkey) (h2 h2) (h3 gz) (gx gx) (a a-0)
    (b b-0))
  (defstrand resp 2 (dhkey dhkey) (h1 gx) (gy h2) (gz gz-0) (b b-1)
    (a a-1))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((1 2) (0 2))
    ((2 1) (1 1)))
  (non-orig dhkey (invk gx) (invk gy) (invk gz) (invk h2) (invk gz-0)
    (privk a))
  (uniq-orig gx gy gz h2 gz-0)
  (comment "Responder point-of-view")
  (operation encryption-test (added-strand resp 2)
    (enc "dh" h2 gx dhkey) (1 1))
  (strand-map 0 1)
  (traces
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (recv (enc (enc "dh" gz gx dhkey) (pubk b))))
    ((send (enc gx a-0 (pubk b-0)))
      (recv (enc h2 (enc "dh" h2 gx dhkey) gz b-0 (pubk a-0)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b-0))))
    ((recv (enc gx a-1 (pubk b-1)))
      (send (enc h2 (enc "dh" h2 gx dhkey) gz-0 b-1 (pubk a-1)))))
  (label 11)
  (parent 8)
  (unrealized (1 1))
  (dead)
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy h2 akey) (a b a-0 b-0 name))
  (defstrand resp 3 (dhkey dhkey) (h1 gx) (gy gy) (gz gy) (b b) (a a))
  (defstrand init 3 (dhkey dhkey) (h2 h2) (h3 gy) (gx gx) (a a-0)
    (b b-0))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig dhkey (invk gx) (invk gy) (privk a))
  (uniq-orig gx gy)
  (comment "Responder point-of-view")
  (operation encryption-test (added-strand init 3)
    (enc "dh" gy gx dhkey) (0 2)
    (enc gy (enc "dh" gy gx dhkey) gy b (pubk a)))
  (strand-map 0)
  (traces
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gy b (pubk a)))
      (recv (enc (enc "dh" gy gx dhkey) (pubk b))))
    ((send (enc gx a-0 (pubk b-0)))
      (recv (enc h2 (enc "dh" h2 gx dhkey) gy b-0 (pubk a-0)))
      (send (enc (enc "dh" gy gx dhkey) (pubk b-0)))))
  (label 12)
  (parent 9)
  (unrealized (1 1))
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gy) (dhkey dhkey))))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz akey) (a b name))
  (defstrand resp 3 (dhkey dhkey) (h1 gx) (gy gy) (gz gz) (b b) (a a))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gz) (gx gx) (a a) (b b))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig dhkey (invk gx) (invk gy) (invk gz) (privk a))
  (uniq-orig gx gy gz)
  (comment "Responder point-of-view")
  (operation encryption-test (contracted (a-0 a) (b-0 b))
    (enc "dh" gy gx dhkey) (1 1)
    (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
  (strand-map 0 1)
  (traces
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (recv (enc (enc "dh" gz gx dhkey) (pubk b))))
    ((send (enc gx a (pubk b)))
      (recv (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b)))))
  (label 13)
  (parent 10)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (origs (gy (0 1)) (gz (0 1)) (gx (1 0))))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy akey) (a b a-0 b-0 name))
  (defstrand resp 3 (dhkey dhkey) (h1 gx) (gy gy) (gz gy) (b b) (a a))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gy) (gx gx) (a a-0)
    (b b-0))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig dhkey (invk gx) (invk gy) (privk a))
  (uniq-orig gx gy)
  (comment "Responder point-of-view")
  (operation encryption-test (displaced 2 0 resp 2)
    (enc "dh" h2 gx dhkey) (1 1))
  (strand-map 0 1)
  (traces
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gy b (pubk a)))
      (recv (enc (enc "dh" gy gx dhkey) (pubk b))))
    ((send (enc gx a-0 (pubk b-0)))
      (recv (enc gy (enc "dh" gy gx dhkey) gy b-0 (pubk a-0)))
      (send (enc (enc "dh" gy gx dhkey) (pubk b-0)))))
  (label 14)
  (parent 12)
  (unrealized (1 1))
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gy) (dhkey dhkey))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy h2 gz akey) (a b a-0 b-0 b-1 a-1 name))
  (defstrand resp 3 (dhkey dhkey) (h1 gx) (gy gy) (gz gy) (b b) (a a))
  (defstrand init 3 (dhkey dhkey) (h2 h2) (h3 gy) (gx gx) (a a-0)
    (b b-0))
  (defstrand resp 2 (dhkey dhkey) (h1 gx) (gy h2) (gz gz) (b b-1)
    (a a-1))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((1 2) (0 2))
    ((2 1) (1 1)))
  (non-orig dhkey (invk gx) (invk gy) (invk h2) (invk gz) (privk a))
  (uniq-orig gx gy h2 gz)
  (comment "Responder point-of-view")
  (operation encryption-test (added-strand resp 2)
    (enc "dh" h2 gx dhkey) (1 1))
  (strand-map 0 1)
  (traces
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gy b (pubk a)))
      (recv (enc (enc "dh" gy gx dhkey) (pubk b))))
    ((send (enc gx a-0 (pubk b-0)))
      (recv (enc h2 (enc "dh" h2 gx dhkey) gy b-0 (pubk a-0)))
      (send (enc (enc "dh" gy gx dhkey) (pubk b-0))))
    ((recv (enc gx a-1 (pubk b-1)))
      (send (enc h2 (enc "dh" h2 gx dhkey) gz b-1 (pubk a-1)))))
  (label 15)
  (parent 12)
  (unrealized (1 1))
  (dead)
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gy) (dhkey dhkey))))
  (comment "empty cohort"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy akey) (a b name))
  (defstrand resp 3 (dhkey dhkey) (h1 gx) (gy gy) (gz gy) (b b) (a a))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gy) (gx gx) (a a) (b b))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig dhkey (invk gx) (invk gy) (privk a))
  (uniq-orig gx gy)
  (comment "Responder point-of-view")
  (operation encryption-test (contracted (a-0 a) (b-0 b))
    (enc "dh" gy gx dhkey) (1 1)
    (enc gy (enc "dh" gy gx dhkey) gy b (pubk a)))
  (strand-map 0 1)
  (traces
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gy b (pubk a)))
      (recv (enc (enc "dh" gy gx dhkey) (pubk b))))
    ((send (enc gx a (pubk b)))
      (recv (enc gy (enc "dh" gy gx dhkey) gy b (pubk a)))
      (send (enc (enc "dh" gy gx dhkey) (pubk b)))))
  (label 16)
  (parent 14)
  (seen 13)
  (seen-ops
    (13 (operation generalization separated gy-0) (strand-map 0 1)))
  (realized)
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gy) (dhkey dhkey))))
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")