(herald "DHCR: unified model (UM) criss-cross" (bound 20) (limit 8000)
  (algebra diffie-hellman))

(comment "CPSA 3.6.8")
(comment "All input read from tst/dhcr_umx.scm")
(comment "Step count limited to 8000")
(comment "Strand count bounded at 20")

(defprotocol dhcr-umx diffie-hellman
  (defrole init
    (vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb))
    (uniq-orig na)
    (uniq-gen x)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) y) (gen)))
    (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb))))
  (defrole resp
    (vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb))
    (uniq-orig nb)
    (uniq-gen y)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) x) (gen)))
    (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb))
      (y (exp (gen) x))))
  (defrole ltx-gen
    (vars (self name) (l rndx))
    (trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
      (send l))
    (uniq-gen l)
    (fn-of ("ltx-of" (self l)) ("principal-of" (l self)))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (precedes ((1 0) (0 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq ((exp (gen) y) (gen)))
  (non-orig ltxb)
  (uniq-gen ltxb x)
  (uniq-orig na)
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat b (exp (gen) ltxb)))))
  (label 0)
  (unrealized (0 2))
  (origs (na (0 1)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxa ltxb rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (precedes ((0 1) (2 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x))
    (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) x) (gen)) ((exp (gen) y) (gen)))
  (non-orig ltxb)
  (uniq-gen y x ltxb)
  (uniq-orig na nb)
  (operation encryption-test (added-strand resp 3)
    (enc na nb a b
      (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))) (0 2))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))))
      (send nb)) ((send (cat b (exp (gen) ltxb))))
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa))
              (exp (gen) (mul x ltxb))))))))
  (label 1)
  (parent 0)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((ltxa ltxa) (ltxb ltxb) (a a) (b b) (x x) (y y) (na na)
        (nb nb))))
  (origs (nb (2 2)) (na (0 1))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 1) (0 2)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq ((exp (gen) y) (gen)))
  (non-orig ltxb)
  (uniq-gen ltxb x)
  (uniq-orig na)
  (operation encryption-test
    (added-listener
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
    (enc na nb a b
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))) (0 2))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat b (exp (gen) ltxb))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 2)
  (parent 0)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((2 1) (0 2)) ((3 1) (2 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq ((exp (gen) y) (gen)))
  (non-orig ltxb)
  (uniq-gen ltxb x)
  (uniq-orig na)
  (operation encryption-test
    (added-listener
      (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
    (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))) (2 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat b (exp (gen) ltxb))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 3)
  (parent 2)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) ltxb) x))
  (precedes ((0 1) (4 0)) ((1 0) (0 0)) ((2 1) (0 2)) ((3 1) (2 0))
    ((4 1) (3 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq ((exp (gen) y) (gen)))
  (non-orig ltxb)
  (uniq-gen ltxb x)
  (uniq-orig na)
  (operation nonce-test (added-listener (cat (exp (gen) ltxb) x))
    (exp (gen) (mul ltxb x)) (3 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat b (exp (gen) ltxb))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) ltxb) x)) (send (cat (exp (gen) ltxb) x))))
  (label 4)
  (parent 3)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhcr-umx diffie-hellman
  (defrole init
    (vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb))
    (uniq-orig na)
    (uniq-gen x)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) y) (gen)))
    (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb))))
  (defrole resp
    (vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb))
    (uniq-orig nb)
    (uniq-gen y)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) x) (gen)))
    (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb))
      (y (exp (gen) x))))
  (defrole ltx-gen
    (vars (self name) (l rndx))
    (trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
      (send l))
    (uniq-gen l)
    (fn-of ("ltx-of" (self l)) ("principal-of" (l self)))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (precedes ((1 0) (0 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (non-orig ltxb)
  (uniq-gen ltxb x)
  (uniq-orig na)
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat b (exp (gen) ltxb)))))
  (label 5)
  (unrealized (0 2))
  (origs (na (0 1)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxa ltxb rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (precedes ((0 1) (2 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x))
    (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) x) (gen)) (a b) ((exp (gen) y) (gen)))
  (non-orig ltxb)
  (uniq-gen y x ltxb)
  (uniq-orig na nb)
  (operation encryption-test (added-strand resp 3)
    (enc na nb a b
      (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))) (0 2))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))))
      (send nb)) ((send (cat b (exp (gen) ltxb))))
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa))
              (exp (gen) (mul x ltxb))))))))
  (label 6)
  (parent 5)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((ltxa ltxa) (ltxb ltxb) (a a) (b b) (x x) (y y) (na na)
        (nb nb))))
  (origs (nb (2 2)) (na (0 1))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 1) (0 2)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (non-orig ltxb)
  (uniq-gen ltxb x)
  (uniq-orig na)
  (operation encryption-test
    (added-listener
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
    (enc na nb a b
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))) (0 2))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat b (exp (gen) ltxb))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 7)
  (parent 5)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((2 1) (0 2)) ((3 1) (2 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (non-orig ltxb)
  (uniq-gen ltxb x)
  (uniq-orig na)
  (operation encryption-test
    (added-listener
      (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
    (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))) (2 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat b (exp (gen) ltxb))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 8)
  (parent 7)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) ltxb) x))
  (precedes ((0 1) (4 0)) ((1 0) (0 0)) ((2 1) (0 2)) ((3 1) (2 0))
    ((4 1) (3 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (non-orig ltxb)
  (uniq-gen ltxb x)
  (uniq-orig na)
  (operation nonce-test (added-listener (cat (exp (gen) ltxb) x))
    (exp (gen) (mul ltxb x)) (3 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat b (exp (gen) ltxb))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) ltxb) x)) (send (cat (exp (gen) ltxb) x))))
  (label 9)
  (parent 8)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhcr-umx diffie-hellman
  (defrole init
    (vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb))
    (uniq-orig na)
    (uniq-gen x)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) y) (gen)))
    (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb))))
  (defrole resp
    (vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb))
    (uniq-orig nb)
    (uniq-gen y)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) x) (gen)))
    (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb))
      (y (exp (gen) x))))
  (defrole ltx-gen
    (vars (self name) (l rndx))
    (trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
      (send l))
    (uniq-gen l)
    (fn-of ("ltx-of" (self l)) ("principal-of" (l self)))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b self self-0 name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self self) (l ltxa))
  (defstrand ltx-gen 1 (self self-0) (l ltxb))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (self-0 ltxb) (self ltxa) (a ltxa) (b ltxb))
    ("principal-of" (ltxb self-0) (ltxa self) (ltxa a) (ltxb b)))
  (neq (a b) ((exp (gen) y) (gen)))
  (non-orig ltxa ltxb)
  (uniq-gen ltxa ltxb x)
  (uniq-orig na)
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat self (exp (gen) ltxa))))
    ((send (cat self-0 (exp (gen) ltxb)))))
  (label 10)
  (unrealized (0 0) (0 2))
  (preskeleton)
  (origs (na (0 1)))
  (comment "Not a skeleton"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (precedes ((1 0) (0 0)) ((2 0) (0 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (non-orig ltxa ltxb)
  (uniq-gen ltxa ltxb x)
  (uniq-orig na)
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat a (exp (gen) ltxa))))
    ((send (cat b (exp (gen) ltxb)))))
  (label 11)
  (parent 10)
  (unrealized (0 2))
  (origs (na (0 1)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxa ltxb rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (precedes ((0 1) (3 1)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 0))
    ((2 0) (3 0)) ((3 2) (0 2)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x))
    (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) x) (gen)) (a b) ((exp (gen) y) (gen)))
  (non-orig ltxa ltxb)
  (uniq-gen y x ltxa ltxb)
  (uniq-orig na nb)
  (operation encryption-test (added-strand resp 3)
    (enc na nb a b
      (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))) (0 2))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))))
      (send nb)) ((send (cat a (exp (gen) ltxa))))
    ((send (cat b (exp (gen) ltxb))))
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa))
              (exp (gen) (mul x ltxb))))))))
  (label 12)
  (parent 11)
  (unrealized)
  (shape)
  (maps
    ((0 1 2)
      ((ltxa ltxa) (ltxb ltxb) (a a) (b b) (x x) (y y) (na na)
        (nb nb))))
  (origs (nb (3 2)) (na (0 1))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 1) (3 0)) ((1 0) (0 0)) ((2 0) (0 0)) ((3 1) (0 2)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (non-orig ltxa ltxb)
  (uniq-gen ltxa ltxb x)
  (uniq-orig na)
  (operation encryption-test
    (added-listener
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
    (enc na nb a b
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))) (0 2))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat a (exp (gen) ltxa))))
    ((send (cat b (exp (gen) ltxb))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 13)
  (parent 11)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 1) (4 0)) ((1 0) (0 0)) ((2 0) (0 0)) ((3 1) (0 2))
    ((4 1) (3 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (non-orig ltxa ltxb)
  (uniq-gen ltxa ltxb x)
  (uniq-orig na)
  (operation encryption-test
    (added-listener
      (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
    (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))) (3 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat a (exp (gen) ltxa))))
    ((send (cat b (exp (gen) ltxb))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 14)
  (parent 13)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) ltxb) x))
  (precedes ((0 1) (5 0)) ((1 0) (0 0)) ((2 0) (0 0)) ((3 1) (0 2))
    ((4 1) (3 0)) ((5 1) (4 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (non-orig ltxa ltxb)
  (uniq-gen ltxa ltxb x)
  (uniq-orig na)
  (operation nonce-test (added-listener (cat (exp (gen) ltxb) x))
    (exp (gen) (mul ltxb x)) (4 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb)) ((send (cat a (exp (gen) ltxa))))
    ((send (cat b (exp (gen) ltxb))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) ltxb) x)) (send (cat (exp (gen) ltxb) x))))
  (label 15)
  (parent 14)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhcr-umx diffie-hellman
  (defrole init
    (vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb))
    (uniq-orig na)
    (uniq-gen x)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) y) (gen)))
    (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb))))
  (defrole resp
    (vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb))
    (uniq-orig nb)
    (uniq-gen y)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) x) (gen)))
    (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb))
      (y (exp (gen) x))))
  (defrole ltx-gen
    (vars (self name) (l rndx))
    (trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
      (send l))
    (uniq-gen l)
    (fn-of ("ltx-of" (self l)) ("principal-of" (l self)))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b self self-0 name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self self) (l ltxa))
  (defstrand ltx-gen 1 (self self-0) (l ltxb))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (self-0 ltxb) (self ltxa) (a ltxa) (b ltxb))
    ("principal-of" (ltxb self-0) (ltxa self) (ltxa a) (ltxb b)))
  (neq (a b) ((exp (gen) x) (gen)))
  (non-orig ltxa ltxb)
  (uniq-gen ltxa ltxb y)
  (uniq-orig nb)
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat self (exp (gen) ltxa))))
    ((send (cat self-0 (exp (gen) ltxb)))))
  (label 16)
  (unrealized (0 0) (0 3))
  (preskeleton)
  (origs (nb (0 2)))
  (comment "Not a skeleton"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (precedes ((1 0) (0 0)) ((2 0) (0 0)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) x) (gen)))
  (non-orig ltxa ltxb)
  (uniq-gen ltxa ltxb y)
  (uniq-orig nb)
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((send (cat b (exp (gen) ltxb)))))
  (label 17)
  (parent 16)
  (unrealized (0 3))
  (origs (nb (0 2)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxa ltxb rndx))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 0))
    ((2 0) (3 0)) ((3 1) (0 1)) ((3 3) (0 3)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)) (y (exp (gen) ltxa))
    (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) y) (gen)) (a b) ((exp (gen) x) (gen)))
  (non-orig ltxa ltxb)
  (uniq-gen y x ltxa ltxb)
  (uniq-orig na nb)
  (operation nonce-test (added-strand init 4) nb (0 3)
    (enc na nb a b
      (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((send (cat b (exp (gen) ltxb))))
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))))
      (send nb)))
  (label 18)
  (parent 17)
  (unrealized)
  (shape)
  (maps
    ((0 1 2)
      ((ltxa ltxa) (ltxb ltxb) (a a) (b b) (y y) (x x) (na na)
        (nb nb))))
  (origs (na (3 1)) (nb (0 2))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((2 0) (0 0)) ((3 1) (0 3)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) x) (gen)))
  (non-orig ltxa ltxb)
  (uniq-gen ltxa ltxb y)
  (uniq-orig nb)
  (operation nonce-test
    (added-listener
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))) nb (0 3)
    (enc na nb a b
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((send (cat b (exp (gen) ltxb))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 19)
  (parent 17)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((2 0) (0 0)) ((3 1) (0 3))
    ((4 1) (3 0)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) x) (gen)))
  (non-orig ltxa ltxb)
  (uniq-gen ltxa ltxb y)
  (uniq-orig nb)
  (operation encryption-test
    (added-listener
      (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
    (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))) (3 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((send (cat b (exp (gen) ltxb))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 20)
  (parent 19)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (defstrand ltx-gen 1 (self b) (l ltxb))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) ltxa) y))
  (precedes ((0 2) (5 0)) ((1 0) (0 0)) ((2 0) (0 0)) ((3 1) (0 3))
    ((4 1) (3 0)) ((5 1) (4 0)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) x) (gen)))
  (non-orig ltxa ltxb)
  (uniq-gen ltxa ltxb y)
  (uniq-orig nb)
  (operation nonce-test (added-listener (cat (exp (gen) ltxa) y))
    (exp (gen) (mul ltxa y)) (4 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((send (cat b (exp (gen) ltxb))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) ltxa) y)) (send (cat (exp (gen) ltxa) y))))
  (label 21)
  (parent 20)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhcr-umx diffie-hellman
  (defrole init
    (vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb))
    (uniq-orig na)
    (uniq-gen x)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) y) (gen)))
    (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb))))
  (defrole resp
    (vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb))
    (uniq-orig nb)
    (uniq-gen y)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) x) (gen)))
    (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb))
      (y (exp (gen) x))))
  (defrole ltx-gen
    (vars (self name) (l rndx))
    (trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
      (send l))
    (uniq-gen l)
    (fn-of ("ltx-of" (self l)) ("principal-of" (l self)))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b self name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self self) (l ltxa))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (self ltxa) (a ltxa) (b ltxb))
    ("principal-of" (ltxa self) (ltxa a) (ltxb b)))
  (neq (a b) ((exp (gen) x) (gen)))
  (non-orig ltxa)
  (uniq-gen ltxa y)
  (uniq-orig nb)
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat self (exp (gen) ltxa)))))
  (label 22)
  (unrealized (0 0) (0 3))
  (preskeleton)
  (origs (nb (0 2)))
  (comment "Not a skeleton"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (precedes ((1 0) (0 0)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq (a b) ((exp (gen) x) (gen)))
  (non-orig ltxa)
  (uniq-gen ltxa y)
  (uniq-orig nb)
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa)))))
  (label 23)
  (parent 22)
  (unrealized (0 3))
  (origs (nb (0 2)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxa ltxb rndx))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((2 3) (0 3)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)) (y (exp (gen) ltxa))
    (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) y) (gen)) (a b) ((exp (gen) x) (gen)))
  (non-orig ltxa)
  (uniq-gen y x ltxa)
  (uniq-orig na nb)
  (operation nonce-test (added-strand init 4) nb (0 3)
    (enc na nb a b
      (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))))
      (send nb)))
  (label 24)
  (parent 23)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((ltxa ltxa) (ltxb ltxb) (a a) (b b) (y y) (x x) (na na)
        (nb nb))))
  (origs (na (2 1)) (nb (0 2))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 2) (2 0)) ((1 0) (0 0)) ((2 1) (0 3)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq (a b) ((exp (gen) x) (gen)))
  (non-orig ltxa)
  (uniq-gen ltxa y)
  (uniq-orig nb)
  (operation nonce-test
    (added-listener
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))) nb (0 3)
    (enc na nb a b
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 25)
  (parent 23)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((2 1) (0 3)) ((3 1) (2 0)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq (a b) ((exp (gen) x) (gen)))
  (non-orig ltxa)
  (uniq-gen ltxa y)
  (uniq-orig nb)
  (operation encryption-test
    (added-listener
      (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
    (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))) (2 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 26)
  (parent 25)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) ltxa) y))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((2 1) (0 3)) ((3 1) (2 0))
    ((4 1) (3 0)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq (a b) ((exp (gen) x) (gen)))
  (non-orig ltxa)
  (uniq-gen ltxa y)
  (uniq-orig nb)
  (operation nonce-test (added-listener (cat (exp (gen) ltxa) y))
    (exp (gen) (mul ltxa y)) (3 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) ltxa) y)) (send (cat (exp (gen) ltxa) y))))
  (label 27)
  (parent 26)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhcr-umx diffie-hellman
  (defrole init
    (vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb))
    (uniq-orig na)
    (uniq-gen x)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) y) (gen)))
    (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb))))
  (defrole resp
    (vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb))
    (uniq-orig nb)
    (uniq-gen y)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) x) (gen)))
    (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb))
      (y (exp (gen) x))))
  (defrole ltx-gen
    (vars (self name) (l rndx))
    (trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
      (send l))
    (uniq-gen l)
    (fn-of ("ltx-of" (self l)) ("principal-of" (l self)))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b self name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self self) (l ltxa))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (self ltxa) (a ltxa) (b ltxb))
    ("principal-of" (ltxa self) (ltxa a) (ltxb b)))
  (neq ((exp (gen) x) (gen)))
  (non-orig ltxa)
  (uniq-gen ltxa y)
  (uniq-orig nb)
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat self (exp (gen) ltxa)))))
  (label 28)
  (unrealized (0 0) (0 3))
  (preskeleton)
  (origs (nb (0 2)))
  (comment "Not a skeleton"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (precedes ((1 0) (0 0)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) x) (gen)))
  (non-orig ltxa)
  (uniq-gen ltxa y)
  (uniq-orig nb)
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa)))))
  (label 29)
  (parent 28)
  (unrealized (0 3))
  (origs (nb (0 2)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxa ltxb rndx))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((2 3) (0 3)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)) (y (exp (gen) ltxa))
    (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) y) (gen)) ((exp (gen) x) (gen)))
  (non-orig ltxa)
  (uniq-gen y x ltxa)
  (uniq-orig na nb)
  (operation nonce-test (added-strand init 4) nb (0 3)
    (enc na nb a b
      (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))))
      (send nb)))
  (label 30)
  (parent 29)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((ltxa ltxa) (ltxb ltxb) (a a) (b b) (y y) (x x) (na na)
        (nb nb))))
  (origs (na (2 1)) (nb (0 2))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 2) (2 0)) ((1 0) (0 0)) ((2 1) (0 3)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) x) (gen)))
  (non-orig ltxa)
  (uniq-gen ltxa y)
  (uniq-orig nb)
  (operation nonce-test
    (added-listener
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))) nb (0 3)
    (enc na nb a b
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 31)
  (parent 29)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((2 1) (0 3)) ((3 1) (2 0)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) x) (gen)))
  (non-orig ltxa)
  (uniq-gen ltxa y)
  (uniq-orig nb)
  (operation encryption-test
    (added-listener
      (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
    (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))) (2 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 32)
  (parent 31)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb y rndx) (x expt))
  (defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (defstrand ltx-gen 1 (self a) (l ltxa))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) ltxa) y))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((2 1) (0 3)) ((3 1) (2 0))
    ((4 1) (3 0)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) x) (gen)))
  (non-orig ltxa)
  (uniq-gen ltxa y)
  (uniq-orig nb)
  (operation nonce-test (added-listener (cat (exp (gen) ltxa) y))
    (exp (gen) (mul ltxa y)) (3 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb)) ((send (cat a (exp (gen) ltxa))))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) ltxa) y)) (send (cat (exp (gen) ltxa) y))))
  (label 33)
  (parent 32)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dhcr-umx diffie-hellman
  (defrole init
    (vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb))
    (uniq-orig na)
    (uniq-gen x)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) y) (gen)))
    (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb))))
  (defrole resp
    (vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
    (trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (recv nb))
    (uniq-orig nb)
    (uniq-gen y)
    (fn-of ("ltx-of" (a ltxa) (b ltxb))
      ("principal-of" (ltxa a) (ltxb b)))
    (neq ((exp (gen) x) (gen)))
    (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb))
      (y (exp (gen) x))))
  (defrole ltx-gen
    (vars (self name) (l rndx))
    (trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
      (send l))
    (uniq-gen l)
    (fn-of ("ltx-of" (self l)) ("principal-of" (l self)))))

(defskeleton dhcr-umx
  (vars (na nb data) (a b self self-0 name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (defstrand ltx-gen 3 (self self) (l ltxa))
  (defstrand ltx-gen 3 (self self-0) (l ltxb))
  (precedes ((0 3) (2 1)) ((0 3) (3 1)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (self-0 ltxb) (self ltxa) (a ltxa) (b ltxb))
    ("principal-of" (ltxb self-0) (ltxa self) (ltxa a) (ltxb b)))
  (neq (a b) ((exp (gen) y) (gen)))
  (uniq-gen ltxa ltxb x)
  (uniq-orig na)
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((send (cat self (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat self-0 (exp (gen) ltxb))) (recv "end-of-protocol")
      (send ltxb)))
  (label 34)
  (unrealized (0 0) (0 2) (1 0))
  (preskeleton)
  (origs (na (0 1)))
  (comment "Not a skeleton"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (defstrand ltx-gen 3 (self a) (l ltxa))
  (defstrand ltx-gen 3 (self b) (l ltxb))
  (precedes ((0 1) (1 0)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((3 0) (0 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (uniq-gen ltxa ltxb x)
  (uniq-orig na)
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((send (cat a (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat b (exp (gen) ltxb))) (recv "end-of-protocol")
      (send ltxb)))
  (label 35)
  (parent 34)
  (unrealized (0 2) (1 0))
  (origs (na (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (defstrand ltx-gen 3 (self a) (l ltxa))
  (defstrand ltx-gen 3 (self b) (l ltxb))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (precedes ((0 1) (4 0)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((3 0) (0 0)) ((4 1) (1 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (uniq-gen ltxa ltxb x)
  (uniq-orig na)
  (operation encryption-test
    (added-listener
      (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
    (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))) (1 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((send (cat a (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat b (exp (gen) ltxb))) (recv "end-of-protocol")
      (send ltxb))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
  (label 36)
  (parent 35)
  (unrealized (0 2) (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (defstrand ltx-gen 3 (self a) (l ltxa))
  (defstrand ltx-gen 3 (self b) (l ltxb))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) ltxb) x))
  (precedes ((0 1) (5 0)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((3 0) (0 0)) ((4 1) (1 0)) ((5 1) (4 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (uniq-gen ltxa ltxb x)
  (uniq-orig na)
  (operation nonce-test (added-listener (cat (exp (gen) ltxb) x))
    (exp (gen) (mul ltxb x)) (4 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((send (cat a (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat b (exp (gen) ltxb))) (recv "end-of-protocol")
      (send ltxb))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) ltxb) x)) (send (cat (exp (gen) ltxb) x))))
  (label 37)
  (parent 36)
  (unrealized (0 2) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa ltxb x rndx) (y expt))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (defstrand ltx-gen 3 (self a) (l ltxa))
  (defstrand ltx-gen 3 (self b) (l ltxb))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
  (deflistener (cat (exp (gen) x) ltxb))
  (precedes ((0 1) (5 0)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((3 0) (0 0)) ((4 1) (1 0)) ((5 1) (4 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (b ltxb) (a ltxa))
    ("principal-of" (ltxb b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (uniq-gen ltxa ltxb x)
  (uniq-orig na)
  (operation nonce-test (added-listener (cat (exp (gen) x) ltxb))
    (exp (gen) (mul ltxb x)) (4 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))))
      (send nb))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((send (cat a (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat b (exp (gen) ltxb))) (recv "end-of-protocol")
      (send ltxb))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
    ((recv (cat (exp (gen) x) ltxb)) (send (cat (exp (gen) x) ltxb))))
  (label 38)
  (parent 36)
  (unrealized (0 2) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa x rndx) (y expt) (l rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb l)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (defstrand ltx-gen 3 (self a) (l ltxa))
  (defstrand ltx-gen 3 (self b) (l l))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (deflistener (cat (exp (gen) x) l))
  (precedes ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0)) ((3 0) (0 0))
    ((3 2) (5 0)) ((4 1) (1 0)) ((5 1) (4 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) l)))
  (fn-of ("ltx-of" (b l) (a ltxa)) ("principal-of" (l b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (uniq-gen ltxa x l)
  (uniq-orig na)
  (operation nonce-test (displaced 6 3 ltx-gen 3) l (5 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) l)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))))
      (send nb))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((send (cat a (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat b (exp (gen) l))) (recv "end-of-protocol") (send l))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((recv (cat (exp (gen) x) l)) (send (cat (exp (gen) x) l))))
  (label 39)
  (parent 38)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxa ltxb rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))
  (defstrand ltx-gen 3 (self a) (l ltxa))
  (defstrand ltx-gen 3 (self b) (l ltxb))
  (deflistener (cat (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))
  (deflistener (cat (exp (gen) x) ltxb))
  (defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (precedes ((0 1) (6 1)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((2 0) (6 0)) ((3 0) (0 0)) ((3 0) (6 0)) ((3 2) (5 0))
    ((4 1) (1 0)) ((5 1) (4 0)) ((6 2) (0 2)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x))
    (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) x) (gen)) (a b) ((exp (gen) y) (gen)))
  (uniq-gen y x ltxa ltxb)
  (uniq-orig na nb)
  (operation encryption-test (added-strand resp 3)
    (enc na nb a b
      (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))) (0 2))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))))
      (send nb))
    ((recv (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))
      (send (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))))
    ((send (cat a (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat b (exp (gen) ltxb))) (recv "end-of-protocol")
      (send ltxb))
    ((recv (cat (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))
      (send (cat (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))))
    ((recv (cat (exp (gen) x) ltxb)) (send (cat (exp (gen) x) ltxb)))
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa))
              (exp (gen) (mul x ltxb))))))))
  (label 40)
  (parent 39)
  (unrealized (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa x rndx) (y expt) (l rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb l)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (defstrand ltx-gen 3 (self a) (l ltxa))
  (defstrand ltx-gen 3 (self b) (l l))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (deflistener (cat (exp (gen) x) l))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (precedes ((0 1) (6 0)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((3 0) (0 0)) ((3 2) (5 0)) ((4 1) (1 0)) ((5 1) (4 0))
    ((6 1) (0 2)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) l)))
  (fn-of ("ltx-of" (b l) (a ltxa)) ("principal-of" (l b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (uniq-gen ltxa x l)
  (uniq-orig na)
  (operation encryption-test
    (added-listener
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
    (enc na nb a b
      (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))) (0 2))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) l)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))))
      (send nb))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((send (cat a (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat b (exp (gen) l))) (recv "end-of-protocol") (send l))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((recv (cat (exp (gen) x) l)) (send (cat (exp (gen) x) l)))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))))
  (label 41)
  (parent 39)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxa ltxb rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))
  (defstrand ltx-gen 3 (self a) (l ltxa))
  (defstrand ltx-gen 3 (self b) (l ltxb))
  (deflistener (cat (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))
  (deflistener (cat (exp (gen) x) ltxb))
  (defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (deflistener (cat (exp (gen) y) ltxa))
  (precedes ((0 1) (6 1)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((2 0) (6 0)) ((3 0) (0 0)) ((3 0) (6 0)) ((3 2) (5 0))
    ((4 1) (1 0)) ((5 1) (4 0)) ((6 2) (0 2)) ((6 2) (7 0))
    ((7 1) (4 0)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x))
    (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) x) (gen)) (a b) ((exp (gen) y) (gen)))
  (uniq-gen y x ltxa ltxb)
  (uniq-orig na nb)
  (operation nonce-test (added-listener (cat (exp (gen) y) ltxa))
    (exp (gen) (mul y ltxa)) (4 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))))
      (send nb))
    ((recv (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))
      (send (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))))
    ((send (cat a (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat b (exp (gen) ltxb))) (recv "end-of-protocol")
      (send ltxb))
    ((recv (cat (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))
      (send (cat (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))))
    ((recv (cat (exp (gen) x) ltxb)) (send (cat (exp (gen) x) ltxb)))
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))))))
    ((recv (cat (exp (gen) y) ltxa)) (send (cat (exp (gen) y) ltxa))))
  (label 42)
  (parent 40)
  (unrealized (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxa ltxb rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))
  (defstrand ltx-gen 3 (self a) (l ltxa))
  (defstrand ltx-gen 3 (self b) (l ltxb))
  (deflistener (cat (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))
  (deflistener (cat (exp (gen) x) ltxb))
  (defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
    (y y) (x x))
  (deflistener (cat (exp (gen) ltxa) y))
  (precedes ((0 1) (6 1)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((2 0) (6 0)) ((3 0) (0 0)) ((3 0) (6 0)) ((3 2) (5 0))
    ((4 1) (1 0)) ((5 1) (4 0)) ((6 2) (0 2)) ((6 2) (7 0))
    ((7 1) (4 0)))
  (absent (y (exp (gen) ltxa)) (y (exp (gen) ltxb)) (y (exp (gen) x))
    (x (exp (gen) ltxa)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (a ltxa) (b ltxb))
    ("principal-of" (ltxa a) (ltxb b)))
  (neq ((exp (gen) x) (gen)) (a b) ((exp (gen) y) (gen)))
  (uniq-gen y x ltxa ltxb)
  (uniq-orig na nb)
  (operation nonce-test (added-listener (cat (exp (gen) ltxa) y))
    (exp (gen) (mul y ltxa)) (4 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))))
      (send nb))
    ((recv (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))
      (send (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))))
    ((send (cat a (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat b (exp (gen) ltxb))) (recv "end-of-protocol")
      (send ltxb))
    ((recv (cat (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))))
      (send (cat (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))))
    ((recv (cat (exp (gen) x) ltxb)) (send (cat (exp (gen) x) ltxb)))
    ((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb)))))))
    ((recv (cat (exp (gen) ltxa) y)) (send (cat (exp (gen) ltxa) y))))
  (label 43)
  (parent 40)
  (unrealized (7 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa x rndx) (y expt) (l rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb l)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (defstrand ltx-gen 3 (self a) (l ltxa))
  (defstrand ltx-gen 3 (self b) (l l))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (deflistener (cat (exp (gen) x) l))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (precedes ((0 1) (7 0)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((3 0) (0 0)) ((3 2) (5 0)) ((4 1) (1 0)) ((5 1) (4 0))
    ((6 1) (0 2)) ((7 1) (6 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) l)))
  (fn-of ("ltx-of" (b l) (a ltxa)) ("principal-of" (l b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (uniq-gen ltxa x l)
  (uniq-orig na)
  (operation encryption-test
    (added-listener
      (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
    (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))) (6 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) l)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))))
      (send nb))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((send (cat a (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat b (exp (gen) l))) (recv "end-of-protocol") (send l))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((recv (cat (exp (gen) x) l)) (send (cat (exp (gen) x) l)))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))))
  (label 44)
  (parent 41)
  (unrealized (7 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxb l rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb ltxb)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))
  (defstrand ltx-gen 3 (self a) (l l))
  (defstrand ltx-gen 3 (self b) (l ltxb))
  (deflistener (cat (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))
  (deflistener (cat (exp (gen) x) ltxb))
  (defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb ltxb)
    (y y) (x x))
  (deflistener (cat (exp (gen) y) l))
  (precedes ((0 1) (6 1)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((2 0) (6 0)) ((2 2) (7 0)) ((3 0) (0 0)) ((3 0) (6 0))
    ((3 2) (5 0)) ((4 1) (1 0)) ((5 1) (4 0)) ((6 2) (0 2))
    ((7 1) (4 0)))
  (absent (y (exp (gen) l)) (y (exp (gen) ltxb)) (y (exp (gen) x))
    (x (exp (gen) l)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (a l) (b ltxb)) ("principal-of" (l a) (ltxb b)))
  (neq ((exp (gen) x) (gen)) (a b) ((exp (gen) y) (gen)))
  (uniq-gen y x ltxb l)
  (uniq-orig na nb)
  (operation nonce-test (displaced 8 2 ltx-gen 3) l (7 0))
  (traces
    ((recv (cat (exp (gen) l) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))))
      (send nb))
    ((recv (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))
      (send (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb)))))
    ((send (cat a (exp (gen) l))) (recv "end-of-protocol") (send l))
    ((send (cat b (exp (gen) ltxb))) (recv "end-of-protocol")
      (send ltxb))
    ((recv (cat (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))
      (send (cat (exp (gen) (mul y l)) (exp (gen) (mul x ltxb)))))
    ((recv (cat (exp (gen) x) ltxb)) (send (cat (exp (gen) x) ltxb)))
    ((recv (cat (exp (gen) l) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb)))))))
    ((recv (cat (exp (gen) y) l)) (send (cat (exp (gen) y) l))))
  (label 45)
  (parent 42)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa x rndx) (y expt) (l rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb l)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (defstrand ltx-gen 3 (self a) (l ltxa))
  (defstrand ltx-gen 3 (self b) (l l))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (deflistener (cat (exp (gen) x) l))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (deflistener (cat (exp (gen) x) l))
  (precedes ((0 1) (8 0)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((3 0) (0 0)) ((3 2) (5 0)) ((4 1) (1 0)) ((5 1) (4 0))
    ((6 1) (0 2)) ((7 1) (6 0)) ((8 1) (7 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) l)))
  (fn-of ("ltx-of" (b l) (a ltxa)) ("principal-of" (l b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (uniq-gen ltxa x l)
  (uniq-orig na)
  (operation nonce-test (added-listener (cat (exp (gen) x) l))
    (exp (gen) (mul x l)) (7 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) l)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))))
      (send nb))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((send (cat a (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat b (exp (gen) l))) (recv "end-of-protocol") (send l))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((recv (cat (exp (gen) x) l)) (send (cat (exp (gen) x) l)))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((recv (cat (exp (gen) x) l)) (send (cat (exp (gen) x) l))))
  (label 46)
  (parent 44)
  (unrealized (8 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (ltxa x rndx) (y expt) (l rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb l)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (defstrand ltx-gen 3 (self a) (l ltxa))
  (defstrand ltx-gen 3 (self b) (l l))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (deflistener (cat (exp (gen) x) l))
  (deflistener (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (deflistener (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
  (deflistener (cat (exp (gen) l) x))
  (precedes ((0 1) (8 0)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((3 0) (0 0)) ((3 2) (5 0)) ((4 1) (1 0)) ((5 1) (4 0))
    ((6 1) (0 2)) ((7 1) (6 0)) ((8 1) (7 0)))
  (absent (x (exp (gen) ltxa)) (x (exp (gen) l)))
  (fn-of ("ltx-of" (b l) (a ltxa)) ("principal-of" (l b) (ltxa a)))
  (neq (a b) ((exp (gen) y) (gen)))
  (uniq-gen ltxa x l)
  (uniq-orig na)
  (operation nonce-test (added-listener (cat (exp (gen) l) x))
    (exp (gen) (mul x l)) (7 0))
  (traces
    ((recv (cat (exp (gen) ltxa) (exp (gen) l)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))))
      (send nb))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((send (cat a (exp (gen) ltxa))) (recv "end-of-protocol")
      (send ltxa))
    ((send (cat b (exp (gen) l))) (recv "end-of-protocol") (send l))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((recv (cat (exp (gen) x) l)) (send (cat (exp (gen) x) l)))
    ((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((recv (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l))))
      (send (cat (exp (gen) (mul ltxa y)) (exp (gen) (mul x l)))))
    ((recv (cat (exp (gen) l) x)) (send (cat (exp (gen) l) x))))
  (label 47)
  (parent 44)
  (unrealized (8 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxb l rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb ltxb)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))
  (defstrand ltx-gen 3 (self a) (l l))
  (defstrand ltx-gen 3 (self b) (l ltxb))
  (deflistener (cat (exp (gen) x) ltxb))
  (defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb ltxb)
    (y y) (x x))
  (deflistener (cat (exp (gen) y) l))
  (precedes ((0 1) (5 1)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((2 0) (5 0)) ((2 2) (6 0)) ((3 0) (0 0)) ((3 0) (5 0))
    ((3 2) (4 0)) ((4 1) (1 0)) ((5 2) (0 2)) ((6 1) (1 0)))
  (absent (y (exp (gen) l)) (y (exp (gen) ltxb)) (y (exp (gen) x))
    (x (exp (gen) l)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (a l) (b ltxb)) ("principal-of" (l a) (ltxb b)))
  (neq ((exp (gen) x) (gen)) (a b) ((exp (gen) y) (gen)))
  (uniq-gen y x ltxb l)
  (uniq-orig na nb)
  (operation generalization deleted (4 0))
  (traces
    ((recv (cat (exp (gen) l) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))))
      (send nb))
    ((recv (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))
      (send (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb)))))
    ((send (cat a (exp (gen) l))) (recv "end-of-protocol") (send l))
    ((send (cat b (exp (gen) ltxb))) (recv "end-of-protocol")
      (send ltxb))
    ((recv (cat (exp (gen) x) ltxb)) (send (cat (exp (gen) x) ltxb)))
    ((recv (cat (exp (gen) l) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb)))))))
    ((recv (cat (exp (gen) y) l)) (send (cat (exp (gen) y) l))))
  (label 48)
  (parent 45)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxb l rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb ltxb)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))
  (defstrand ltx-gen 3 (self a) (l l))
  (defstrand ltx-gen 3 (self b) (l ltxb))
  (defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb ltxb)
    (y y) (x x))
  (deflistener (cat (exp (gen) y) l))
  (precedes ((0 1) (4 1)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((2 0) (4 0)) ((2 2) (5 0)) ((3 0) (0 0)) ((3 0) (4 0))
    ((3 2) (1 0)) ((4 2) (0 2)) ((5 1) (1 0)))
  (absent (y (exp (gen) l)) (y (exp (gen) ltxb)) (y (exp (gen) x))
    (x (exp (gen) l)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (a l) (b ltxb)) ("principal-of" (l a) (ltxb b)))
  (neq ((exp (gen) x) (gen)) (a b) ((exp (gen) y) (gen)))
  (uniq-gen y x ltxb l)
  (uniq-orig na nb)
  (operation generalization deleted (4 0))
  (traces
    ((recv (cat (exp (gen) l) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))))
      (send nb))
    ((recv (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))
      (send (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb)))))
    ((send (cat a (exp (gen) l))) (recv "end-of-protocol") (send l))
    ((send (cat b (exp (gen) ltxb))) (recv "end-of-protocol")
      (send ltxb))
    ((recv (cat (exp (gen) l) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb)))))))
    ((recv (cat (exp (gen) y) l)) (send (cat (exp (gen) y) l))))
  (label 49)
  (parent 48)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhcr-umx
  (vars (na nb data) (a b name) (y x ltxb l rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb ltxb)
    (x x) (y y))
  (deflistener (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))
  (defstrand ltx-gen 3 (self a) (l l))
  (defstrand ltx-gen 3 (self b) (l ltxb))
  (defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb ltxb)
    (y y) (x x))
  (precedes ((0 1) (4 1)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
    ((2 0) (4 0)) ((2 2) (1 0)) ((3 0) (0 0)) ((3 0) (4 0))
    ((3 2) (1 0)) ((4 2) (0 2)))
  (absent (y (exp (gen) l)) (y (exp (gen) ltxb)) (y (exp (gen) x))
    (x (exp (gen) l)) (x (exp (gen) ltxb)))
  (fn-of ("ltx-of" (a l) (b ltxb)) ("principal-of" (l a) (ltxb b)))
  (neq ((exp (gen) x) (gen)) (a b) ((exp (gen) y) (gen)))
  (uniq-gen y x ltxb l)
  (uniq-orig na nb)
  (operation generalization deleted (5 0))
  (traces
    ((recv (cat (exp (gen) l) (exp (gen) ltxb)))
      (send (cat na a b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))))
      (send nb))
    ((recv (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))
      (send (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb)))))
    ((send (cat a (exp (gen) l))) (recv "end-of-protocol") (send l))
    ((send (cat b (exp (gen) ltxb))) (recv "end-of-protocol")
      (send ltxb))
    ((recv (cat (exp (gen) l) (exp (gen) ltxb)))
      (recv (cat na a b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb a b
            (hash (exp (gen) (mul y l)) (exp (gen) (mul x ltxb))))))))
  (label 50)
  (parent 49)
  (unrealized)
  (shape)
  (maps
    ((0 1 2 3)
      ((ltxa l) (ltxb ltxb) (x x) (y y) (a a) (b b) (na na) (nb nb))))
  (origs (nb (4 2)) (na (0 1))))

(comment "Nothing left to do")