(herald "IADH: unified model (UM), criss-cross variant" (bound 20)
  (limit 2000) (algebra diffie-hellman))

(comment "CPSA 3.6.8")
(comment "All input read from tst/iadh_umx.scm")
(comment "Strand count bounded at 20")

(defprotocol iadh-umx diffie-hellman
  (defrole participant1
    (vars (l e rndx) (lp ep expt) (self peer name) (key data))
    (trace (recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e)) (recv (exp (gen) ep)) (send key))
    (uniq-gen e)
    (fn-of
      (foo ((hash (exp (gen) (mul e lp)) (exp (gen) (mul l ep))) key)))
    (neq (ep (one)))
    (absent (e (exp (gen) l)) (e (exp (gen) lp))))
  (defrole participant2
    (vars (l e rndx) (lp ep expt) (self peer name) (key data))
    (trace (recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e)) (recv (exp (gen) ep)) (send key))
    (uniq-gen e)
    (fn-of
      (foo ((hash (exp (gen) (mul l ep)) (exp (gen) (mul e lp))) key)))
    (neq (ep (one)))
    (absent (e (exp (gen) l)) (e (exp (gen) lp))))
  (defrole ltx-gen
    (vars (self name) (l rndx))
    (trace (send (enc "cert" (exp (gen) l) self (privk self))) (send l))
    (uniq-gen l)
    (fn-of ("principal-of" (l self)))))

(defskeleton iadh-umx
  (vars (key data) (A B C D name) (eA lA eB lB rndx)
    (lp ep lp-0 ep-0 expt))
  (defstrand participant1 5 (key key) (self A) (peer C) (l lA) (e eA)
    (lp lp) (ep ep))
  (defstrand participant2 5 (key key) (self B) (peer D) (l lB) (e eB)
    (lp lp-0) (ep ep-0))
  (absent (eB (exp (gen) lB)) (eB (exp (gen) lp-0)) (eA (exp (gen) lA))
    (eA (exp (gen) lp)))
  (fn-of
    (foo
      ((hash (exp (gen) (mul lB ep-0)) (exp (gen) (mul eB lp-0))) key)
      ((hash (exp (gen) (mul eA lp)) (exp (gen) (mul lA ep))) key)))
  (neq (ep-0 (one)) (eA eB) (ep (one)))
  (non-orig (privk A) (privk B) (privk C) (privk D) lA lB)
  (uniq-gen eA eB)
  (traces
    ((recv (enc "cert" (exp (gen) lA) A (privk A)))
      (recv (enc "cert" (exp (gen) lp) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) ep)) (send key))
    ((recv (enc "cert" (exp (gen) lB) B (privk B)))
      (recv (enc "cert" (exp (gen) lp-0) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) ep-0)) (send key)))
  (label 0)
  (unrealized (0 0) (0 1) (1 0) (1 1))
  (preskeleton)
  (origs)
  (comment "Not a skeleton"))

(defskeleton iadh-umx
  (vars (key data) (A B C D name) (lB rndx) (ep expt) (lA eB rndx)
    (lp expt) (eA rndx))
  (defstrand participant1 5 (key key) (self A) (peer C) (l lA) (e eA)
    (lp (mul lB ep)) (ep (mul (rec lA) eB lp)))
  (defstrand participant2 5 (key key) (self B) (peer D) (l lB) (e eB)
    (lp lp) (ep (mul ep eA)))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)))
  (absent (eB (exp (gen) lB)) (eB (exp (gen) lp)) (eA (exp (gen) lA))
    (eA (exp (gen) (mul lB ep))))
  (fn-of
    (foo
      ((hash (exp (gen) (mul lB ep eA)) (exp (gen) (mul eB lp))) key)))
  (neq ((mul ep eA) (one)) (eA eB) ((mul (rec lA) eB lp) (one)))
  (non-orig (privk A) (privk B) (privk C) (privk D) lB lA)
  (uniq-gen eB eA)
  (traces
    ((recv (enc "cert" (exp (gen) lA) A (privk A)))
      (recv (enc "cert" (exp (gen) (mul lB ep)) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul (rec lA) eB lp)))
      (send key))
    ((recv (enc "cert" (exp (gen) lB) B (privk B)))
      (recv (enc "cert" (exp (gen) lp) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul ep eA))) (send key)))
  (label 1)
  (parent 0)
  (unrealized (0 0) (0 1) (0 3) (1 0) (1 1))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B C D name) (ep expt) (lA eB rndx) (lp expt)
    (eA l rndx))
  (defstrand participant1 5 (key key) (self A) (peer C) (l lA) (e eA)
    (lp (mul ep l)) (ep (mul (rec lA) eB lp)))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp lp) (ep (mul ep eA)))
  (defstrand ltx-gen 1 (self B) (l l))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) lp)) (eA (exp (gen) lA))
    (eA (exp (gen) (mul ep l))))
  (fn-of ("principal-of" (l B))
    (foo
      ((hash (exp (gen) (mul ep eA l)) (exp (gen) (mul eB lp))) key)))
  (neq ((mul ep eA) (one)) (eA eB) ((mul (rec lA) eB lp) (one)))
  (non-orig (privk A) (privk B) (privk C) (privk D) lA l)
  (uniq-gen eB eA l)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l) B (privk B)) (1 0))
  (traces
    ((recv (enc "cert" (exp (gen) lA) A (privk A)))
      (recv (enc "cert" (exp (gen) (mul ep l)) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul (rec lA) eB lp)))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) lp) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul ep eA))) (send key))
    ((send (enc "cert" (exp (gen) l) B (privk B)))))
  (label 2)
  (parent 1)
  (unrealized (0 0) (0 1) (0 3) (1 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B C name) (ep expt) (lA eB eA l rndx))
  (defstrand participant1 5 (key key) (self A) (peer C) (l lA) (e eA)
    (lp (mul ep l)) (ep (mul (rec lA) eB l)))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul ep eA)))
  (defstrand ltx-gen 1 (self B) (l l))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) lA))
    (eA (exp (gen) (mul ep l))))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul ep eA l)) (exp (gen) (mul eB l))) key)))
  (neq ((mul ep eA) (one)) (eA eB) ((mul (rec lA) eB l) (one)))
  (non-orig (privk A) (privk B) (privk C) lA l)
  (uniq-gen eB eA l)
  (operation encryption-test (displaced 3 2 ltx-gen 1)
    (enc "cert" (exp (gen) l-0) D (privk D)) (1 1))
  (traces
    ((recv (enc "cert" (exp (gen) lA) A (privk A)))
      (recv (enc "cert" (exp (gen) (mul ep l)) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul (rec lA) eB l)))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul ep eA))) (send key))
    ((send (enc "cert" (exp (gen) l) B (privk B)))))
  (label 3)
  (parent 2)
  (unrealized (0 0) (0 1) (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B C D name) (ep expt) (lA eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self A) (peer C) (l lA) (e eA)
    (lp (mul ep l)) (ep (mul (rec lA) eB l-0)))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul ep eA)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (1 1)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) l-0)) (eA (exp (gen) lA))
    (eA (exp (gen) (mul ep l))))
  (fn-of ("principal-of" (l-0 D) (l B))
    (foo
      ((hash (exp (gen) (mul ep eA l)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul ep eA) (one)) (eA eB) ((mul (rec lA) eB l-0) (one)))
  (non-orig (privk A) (privk B) (privk C) (privk D) lA l)
  (uniq-gen eB eA l l-0)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-0) D (privk D)) (1 1))
  (traces
    ((recv (enc "cert" (exp (gen) lA) A (privk A)))
      (recv (enc "cert" (exp (gen) (mul ep l)) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul (rec lA) eB l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul ep eA))) (send key))
    ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) D (privk D)))))
  (label 4)
  (parent 2)
  (unrealized (0 0) (0 1) (0 3))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B C name) (ep expt) (eB eA l rndx))
  (defstrand participant1 5 (key key) (self B) (peer C) (l l) (e eA)
    (lp (mul ep l)) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul ep eA)))
  (defstrand ltx-gen 1 (self B) (l l))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l))
    (eA (exp (gen) (mul ep l))))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul ep eA l)) (exp (gen) (mul eB l))) key)))
  (neq ((mul ep eA) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk C) l)
  (uniq-gen eB eA l)
  (operation encryption-test (displaced 3 2 ltx-gen 1)
    (enc "cert" (exp (gen) l-0) A (privk A)) (0 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) (mul ep l)) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul ep eA))) (send key))
    ((send (enc "cert" (exp (gen) l) B (privk B)))))
  (label 5)
  (parent 3)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B C name) (ep expt) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self A) (peer C) (l l-0) (e eA)
    (lp (mul ep l)) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul ep eA)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) (mul ep l))))
  (fn-of ("principal-of" (l-0 A) (l B))
    (foo ((hash (exp (gen) (mul ep eA l)) (exp (gen) (mul eB l))) key)))
  (neq ((mul ep eA) (one)) (eA eB) ((mul eB l (rec l-0)) (one)))
  (non-orig (privk A) (privk B) (privk C) l l-0)
  (uniq-gen eB eA l l-0)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-0) A (privk A)) (0 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) (mul ep l)) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul ep eA))) (send key))
    ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A)))))
  (label 6)
  (parent 3)
  (unrealized (0 1) (0 3))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B C D name) (ep expt) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer C) (l l-0) (e eA)
    (lp (mul ep l-0)) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul ep eA)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (1 1)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) (mul ep l-0))))
  (fn-of ("principal-of" (l-0 B) (l D))
    (foo
      ((hash (exp (gen) (mul ep eA l-0)) (exp (gen) (mul eB l))) key)))
  (neq ((mul ep eA) (one)) (eA eB) ((mul eB l (rec l-0)) (one)))
  (non-orig (privk B) (privk C) (privk D) l-0)
  (uniq-gen eB eA l l-0)
  (operation encryption-test (displaced 4 2 ltx-gen 1)
    (enc "cert" (exp (gen) l-1) A (privk A)) (0 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) (mul ep l-0)) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul ep eA))) (send key))
    ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D)))))
  (label 7)
  (parent 4)
  (unrealized (0 1) (0 3))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B C D name) (ep expt) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self D) (peer C) (l l-0) (e eA)
    (lp (mul ep l)) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul ep eA)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (1 1)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) l-0)) (eA (exp (gen) l-0))
    (eA (exp (gen) (mul ep l))))
  (fn-of ("principal-of" (l-0 D) (l B))
    (foo
      ((hash (exp (gen) (mul ep eA l)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul ep eA) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk C) (privk D) l l-0)
  (uniq-gen eB eA l l-0)
  (operation encryption-test (displaced 4 3 ltx-gen 1)
    (enc "cert" (exp (gen) l-1) A (privk A)) (0 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (recv (enc "cert" (exp (gen) (mul ep l)) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul ep eA))) (send key))
    ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) D (privk D)))))
  (label 8)
  (parent 4)
  (unrealized (0 1))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B C D name) (ep expt) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer C) (l l-1) (e eA)
    (lp (mul ep l)) (ep (mul eB l-0 (rec l-1))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul ep eA)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (defstrand ltx-gen 1 (self A) (l l-1))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 0)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) l-0)) (eA (exp (gen) l-1))
    (eA (exp (gen) (mul ep l))))
  (fn-of ("principal-of" (l-1 A) (l-0 D) (l B))
    (foo
      ((hash (exp (gen) (mul ep eA l)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul ep eA) (one)) (eA eB) ((mul eB l-0 (rec l-1)) (one)))
  (non-orig (privk A) (privk B) (privk C) (privk D) l l-1)
  (uniq-gen eB eA l l-0 l-1)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-1) A (privk A)) (0 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-1) A (privk A)))
      (recv (enc "cert" (exp (gen) (mul ep l)) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l-0 (rec l-1))))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul ep eA))) (send key))
    ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) D (privk D))))
    ((send (enc "cert" (exp (gen) l-1) A (privk A)))))
  (label 9)
  (parent 4)
  (unrealized (0 1) (0 3))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B name) (eB eA l rndx))
  (defstrand participant1 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul eA l)) (exp (gen) (mul eB l))) key)))
  (neq (eA (one)) (eA eB) (eB (one)))
  (non-orig (privk B) l)
  (uniq-gen eB eA l)
  (operation encryption-test (displaced 3 2 ltx-gen 1)
    (enc "cert" (exp (gen) l-0) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l) B (privk B)))))
  (label 10)
  (parent 5)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((key key) (A B) (B B) (C B) (D B) (lB l) (ep (one)) (lA l)
        (eB eB) (lp l) (eA eA))))
  (origs))

(defskeleton iadh-umx
  (vars (key data) (B C name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer C) (l l) (e eA)
    (lp l-0) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self C) (l l-0))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (0 1)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 C) (l B))
    (foo ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk C) l)
  (uniq-gen eB eA l l-0)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-0) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) C (privk C)))))
  (label 11)
  (parent 5)
  (unrealized (1 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l) (e eA)
    (lp l-0) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l-0) (e eB)
    (lp l-0) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self A) (l l))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)))
  (absent (eB (exp (gen) l-0)) (eA (exp (gen) l)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 B) (l A))
    (foo
      ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l-0))) key)))
  (neq (eA (one)) (eA eB) ((mul eB (rec l) l-0) (one)))
  (non-orig (privk A) (privk B) l l-0)
  (uniq-gen eB eA l l-0)
  (operation encryption-test (displaced 4 2 ltx-gen 1)
    (enc "cert" (exp (gen) l-1) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) A (privk A)))))
  (label 12)
  (parent 6)
  (unrealized (0 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self A) (peer A) (l l-0) (e eA)
    (lp l-0) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 A) (l B))
    (foo ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB)
    ((mul eB l (rec l-0)) (one)))
  (non-orig (privk A) (privk B) l l-0)
  (uniq-gen eB eA l l-0)
  (operation encryption-test (displaced 4 3 ltx-gen 1)
    (enc "cert" (exp (gen) l-1) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A)))))
  (label 13)
  (parent 6)
  (unrealized (0 3) (1 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B C name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer C) (l l) (e eA)
    (lp l-1) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l-0) (e eB)
    (lp l-0) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self A) (l l))
  (defstrand ltx-gen 1 (self C) (l l-1))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((4 0) (0 1)))
  (absent (eB (exp (gen) l-0)) (eA (exp (gen) l)) (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 C) (l A) (l-0 B))
    (foo
      ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB (rec l) l-0) (one)))
  (non-orig (privk A) (privk B) (privk C) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-1) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((send (enc "cert" (exp (gen) l-1) C (privk C)))))
  (label 14)
  (parent 6)
  (unrealized (0 3) (1 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B D name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer B) (l l-0) (e eA)
    (lp l-0) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (1 1)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l))) key)))
  (neq (eA (one)) (eA eB) ((mul eB l (rec l-0)) (one)))
  (non-orig (privk B) (privk D) l-0)
  (uniq-gen eB eA l l-0)
  (operation encryption-test (displaced 4 2 ltx-gen 1)
    (enc "cert" (exp (gen) l-1) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D)))))
  (label 15)
  (parent 7)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B D name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (0 1)) ((3 0) (1 1)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) l-0)) (eA (exp (gen) l))
    (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 D) (l B))
    (foo
      ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB)
    ((mul eB (rec l) l-0) (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen eB eA l l-0)
  (operation encryption-test (displaced 4 3 ltx-gen 1)
    (enc "cert" (exp (gen) l-1) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) D (privk D)))))
  (label 16)
  (parent 7)
  (unrealized (0 3) (1 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B C D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self B) (peer C) (l l-0) (e eA)
    (lp l-1) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self C) (l l-1))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 1)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 C) (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB l (rec l-0)) (one)))
  (non-orig (privk B) (privk C) (privk D) l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-1) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-1) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-1) C (privk C)))))
  (label 17)
  (parent 7)
  (unrealized (0 3) (1 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B D name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self D) (peer B) (l l) (e eA)
    (lp l-0) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (1 1)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l))
    (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l))) key)))
  (neq (eA (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen eB eA l l-0)
  (operation encryption-test (displaced 4 2 ltx-gen 1)
    (enc "cert" (exp (gen) l-1) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l) D (privk D)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D)))))
  (label 18)
  (parent 8)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((key key) (A D) (B B) (C B) (D D) (lB l-0) (ep (one)) (lA l)
        (eB eB) (lp l) (eA eA))))
  (origs))

(defskeleton iadh-umx
  (vars (key data) (B D name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self D) (peer D) (l l-0) (e eA)
    (lp l-0) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (1 1)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) l-0)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 D) (l B))
    (foo
      ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen eB eA l l-0)
  (operation encryption-test (displaced 4 3 ltx-gen 1)
    (enc "cert" (exp (gen) l-1) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) D (privk D)))))
  (label 19)
  (parent 8)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B C D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self D) (peer C) (l l) (e eA)
    (lp l-1) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self C) (l l-1))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (1 1)) ((4 0) (0 1)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 C) (l D) (l-0 B))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk C) (privk D) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-1) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l) D (privk D)))
      (recv (enc "cert" (exp (gen) l-1) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-1) C (privk C)))))
  (label 20)
  (parent 8)
  (unrealized (1 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l-0) (e eA)
    (lp l-1) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-1) (e eB)
    (lp l) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l-1))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 0)))
  (absent (eB (exp (gen) l-1)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 B) (l-0 A) (l D))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq (eA (one)) (eA eB) ((mul eB l (rec l-0)) (one)))
  (non-orig (privk A) (privk B) (privk D) l-0 l-1)
  (uniq-gen eB eA l l-0 l-1)
  (operation encryption-test (displaced 5 2 ltx-gen 1)
    (enc "cert" (exp (gen) l-2) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l-1) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A)))))
  (label 21)
  (parent 9)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer D) (l l) (e eA)
    (lp l-1) (ep (mul eB (rec l) l-1)))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l-1) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l-1))
  (defstrand ltx-gen 1 (self A) (l l))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 1)) ((3 0) (1 1)) ((4 0) (0 0)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l-1)) (eA (exp (gen) l))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 D) (l A) (l-0 B))
    (foo
      ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l-1))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB (rec l) l-1) (one)))
  (non-orig (privk A) (privk B) (privk D) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation encryption-test (displaced 5 3 ltx-gen 1)
    (enc "cert" (exp (gen) l-2) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) D (privk D)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-1)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-1) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l-1) D (privk D))))
    ((send (enc "cert" (exp (gen) l) A (privk A)))))
  (label 22)
  (parent 9)
  (unrealized (0 3) (1 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer A) (l l-1) (e eA)
    (lp l-1) (ep (mul eB l (rec l-1))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self A) (l l-1))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 0)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 A) (l D) (l-0 B))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB l (rec l-1)) (one)))
  (non-orig (privk A) (privk B) (privk D) l-0 l-1)
  (uniq-gen eB eA l l-0 l-1)
  (operation encryption-test (displaced 5 4 ltx-gen 1)
    (enc "cert" (exp (gen) l-2) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l-1) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) A (privk A)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-1))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-1) A (privk A)))))
  (label 23)
  (parent 9)
  (unrealized (0 3) (1 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B C D name) (eB eA l l-0 l-1 l-2 rndx))
  (defstrand participant1 5 (key key) (self A) (peer C) (l l-0) (e eA)
    (lp l-2) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-1) (e eB)
    (lp l) (ep (mul eA (rec l-1) l-2)))
  (defstrand ltx-gen 1 (self B) (l l-1))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (defstrand ltx-gen 1 (self C) (l l-2))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 0)) ((5 0) (0 1)))
  (absent (eB (exp (gen) l-1)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-2)))
  (fn-of ("principal-of" (l-2 C) (l-0 A) (l D) (l-1 B))
    (foo ((hash (exp (gen) (mul eA l-2)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-1) l-2) (one)) (eA eB)
    ((mul eB l (rec l-0)) (one)))
  (non-orig (privk A) (privk B) (privk C) (privk D) l-0 l-1)
  (uniq-gen eB eA l l-0 l-1 l-2)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-2) C (privk C)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) l-2) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-1) l-2)))
      (send key)) ((send (enc "cert" (exp (gen) l-1) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A))))
    ((send (enc "cert" (exp (gen) l-2) C (privk C)))))
  (label 24)
  (parent 9)
  (unrealized (0 3) (1 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B C name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer C) (l l) (e eA)
    (lp l-0) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self C) (l l-0))
  (deflistener (cat (exp (gen) (mul eA (rec l))) l-0))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (0 1)) ((4 1) (1 3)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 C) (l B))
    (foo ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk C) l)
  (uniq-gen eB eA l l-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec l))) l-0))
    (exp (gen) (mul eA (rec l) l-0)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) C (privk C))))
    ((recv (cat (exp (gen) (mul eA (rec l))) l-0))
      (send (cat (exp (gen) (mul eA (rec l))) l-0))))
  (label 25)
  (parent 11)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B C name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer C) (l l) (e eA)
    (lp l-0) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self C) (l l-0))
  (deflistener (cat (exp (gen) (mul (rec l) l-0)) eA))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (0 1)) ((4 1) (1 3)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 C) (l B))
    (foo ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk C) l)
  (uniq-gen eB eA l l-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec l) l-0)) eA))
    (exp (gen) (mul eA (rec l) l-0)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) C (privk C))))
    ((recv (cat (exp (gen) (mul (rec l) l-0)) eA))
      (send (cat (exp (gen) (mul (rec l) l-0)) eA))))
  (label 26)
  (parent 11)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (A B name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l) (e eA)
    (lp l-0) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l-0) (e eB)
    (lp l-0) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self A) (l l))
  (deflistener (cat (exp (gen) (mul (rec l) l-0)) eB))
  (precedes ((0 2) (1 3)) ((1 2) (4 0)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (4 0)) ((4 1) (0 3)))
  (absent (eB (exp (gen) l-0)) (eA (exp (gen) l)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 B) (l A))
    (foo
      ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l-0))) key)))
  (neq (eA (one)) (eA eB) ((mul eB (rec l) l-0) (one)))
  (non-orig (privk A) (privk B) l l-0)
  (uniq-gen eB eA l l-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec l) l-0)) eB))
    (exp (gen) (mul eB (rec l) l-0)) (0 3))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((recv (cat (exp (gen) (mul (rec l) l-0)) eB))
      (send (cat (exp (gen) (mul (rec l) l-0)) eB))))
  (label 27)
  (parent 12)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (A B name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self A) (peer A) (l l-0) (e eA)
    (lp l-0) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (deflistener (cat (exp (gen) (mul (rec l) l-0)) eA))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((4 1) (1 3)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 A) (l B))
    (foo ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB)
    ((mul eB l (rec l-0)) (one)))
  (non-orig (privk A) (privk B) l l-0)
  (uniq-gen eB eA l l-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec l) l-0)) eA))
    (exp (gen) (mul eA (rec l) l-0)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A))))
    ((recv (cat (exp (gen) (mul (rec l) l-0)) eA))
      (send (cat (exp (gen) (mul (rec l) l-0)) eA))))
  (label 28)
  (parent 13)
  (unrealized (0 3) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (A B C name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer C) (l l) (e eA)
    (lp l-1) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l-0) (e eB)
    (lp l-0) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self A) (l l))
  (defstrand ltx-gen 1 (self C) (l l-1))
  (deflistener (cat (exp (gen) (mul eA (rec l-0))) l-1))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((4 0) (0 1)) ((5 1) (1 3)))
  (absent (eB (exp (gen) l-0)) (eA (exp (gen) l)) (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 C) (l A) (l-0 B))
    (foo
      ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB (rec l) l-0) (one)))
  (non-orig (privk A) (privk B) (privk C) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec l-0))) l-1))
    (exp (gen) (mul eA (rec l-0) l-1)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((send (enc "cert" (exp (gen) l-1) C (privk C))))
    ((recv (cat (exp (gen) (mul eA (rec l-0))) l-1))
      (send (cat (exp (gen) (mul eA (rec l-0))) l-1))))
  (label 29)
  (parent 14)
  (unrealized (0 3) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B C name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer C) (l l) (e eA)
    (lp l-1) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l-0) (e eB)
    (lp l-0) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self A) (l l))
  (defstrand ltx-gen 1 (self C) (l l-1))
  (deflistener (cat (exp (gen) (mul (rec l-0) l-1)) eA))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((4 0) (0 1)) ((5 1) (1 3)))
  (absent (eB (exp (gen) l-0)) (eA (exp (gen) l)) (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 C) (l A) (l-0 B))
    (foo
      ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB (rec l) l-0) (one)))
  (non-orig (privk A) (privk B) (privk C) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec l-0) l-1)) eA))
    (exp (gen) (mul eA (rec l-0) l-1)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((send (enc "cert" (exp (gen) l-1) C (privk C))))
    ((recv (cat (exp (gen) (mul (rec l-0) l-1)) eA))
      (send (cat (exp (gen) (mul (rec l-0) l-1)) eA))))
  (label 30)
  (parent 14)
  (unrealized (0 3) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (B D name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer B) (l l-0) (e eA)
    (lp l-0) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (deflistener (cat (exp (gen) (mul eB (rec l-0))) l))
  (precedes ((0 2) (1 3)) ((1 2) (4 0)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 1) (0 3)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l))) key)))
  (neq (eA (one)) (eA eB) ((mul eB l (rec l-0)) (one)))
  (non-orig (privk B) (privk D) l-0)
  (uniq-gen eB eA l l-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eB (rec l-0))) l))
    (exp (gen) (mul eB l (rec l-0))) (0 3))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((recv (cat (exp (gen) (mul eB (rec l-0))) l))
      (send (cat (exp (gen) (mul eB (rec l-0))) l))))
  (label 31)
  (parent 15)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B D name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer B) (l l-0) (e eA)
    (lp l-0) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (deflistener (cat (exp (gen) (mul l (rec l-0))) eB))
  (precedes ((0 2) (1 3)) ((1 2) (4 0)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 1) (0 3)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l))) key)))
  (neq (eA (one)) (eA eB) ((mul eB l (rec l-0)) (one)))
  (non-orig (privk B) (privk D) l-0)
  (uniq-gen eB eA l l-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul l (rec l-0))) eB))
    (exp (gen) (mul eB l (rec l-0))) (0 3))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((recv (cat (exp (gen) (mul l (rec l-0))) eB))
      (send (cat (exp (gen) (mul l (rec l-0))) eB))))
  (label 32)
  (parent 15)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (B D name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (exp (gen) (mul eA (rec l))) l-0))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (0 1)) ((3 0) (1 1)) ((4 1) (1 3)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) l-0)) (eA (exp (gen) l))
    (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 D) (l B))
    (foo
      ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB)
    ((mul eB (rec l) l-0) (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen eB eA l l-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec l))) l-0))
    (exp (gen) (mul eA (rec l) l-0)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) D (privk D))))
    ((recv (cat (exp (gen) (mul eA (rec l))) l-0))
      (send (cat (exp (gen) (mul eA (rec l))) l-0))))
  (label 33)
  (parent 16)
  (unrealized (0 3) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B D name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (exp (gen) (mul (rec l) l-0)) eA))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (0 1)) ((3 0) (1 1)) ((4 1) (1 3)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) l-0)) (eA (exp (gen) l))
    (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 D) (l B))
    (foo
      ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB)
    ((mul eB (rec l) l-0) (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen eB eA l l-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec l) l-0)) eA))
    (exp (gen) (mul eA (rec l) l-0)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) D (privk D))))
    ((recv (cat (exp (gen) (mul (rec l) l-0)) eA))
      (send (cat (exp (gen) (mul (rec l) l-0)) eA))))
  (label 34)
  (parent 16)
  (unrealized (0 3) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (B C D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self B) (peer C) (l l-0) (e eA)
    (lp l-1) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self C) (l l-1))
  (deflistener (cat (exp (gen) (mul eA (rec l-0))) l-1))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 1)) ((5 1) (1 3)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 C) (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB l (rec l-0)) (one)))
  (non-orig (privk B) (privk C) (privk D) l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec l-0))) l-1))
    (exp (gen) (mul eA (rec l-0) l-1)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-1) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-1) C (privk C))))
    ((recv (cat (exp (gen) (mul eA (rec l-0))) l-1))
      (send (cat (exp (gen) (mul eA (rec l-0))) l-1))))
  (label 35)
  (parent 17)
  (unrealized (0 3) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B C D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self B) (peer C) (l l-0) (e eA)
    (lp l-1) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self C) (l l-1))
  (deflistener (cat (exp (gen) (mul (rec l-0) l-1)) eA))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 1)) ((5 1) (1 3)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 C) (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB l (rec l-0)) (one)))
  (non-orig (privk B) (privk C) (privk D) l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec l-0) l-1)) eA))
    (exp (gen) (mul eA (rec l-0) l-1)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-1) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-1) C (privk C))))
    ((recv (cat (exp (gen) (mul (rec l-0) l-1)) eA))
      (send (cat (exp (gen) (mul (rec l-0) l-1)) eA))))
  (label 36)
  (parent 17)
  (unrealized (0 3) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (B D name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self D) (peer D) (l l-0) (e eA)
    (lp l-0) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (exp (gen) (mul (rec l) l-0)) eA))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (1 1)) ((4 1) (1 3)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) l-0)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 D) (l B))
    (foo
      ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen eB eA l l-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec l) l-0)) eA))
    (exp (gen) (mul eA (rec l) l-0)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((send (enc "cert" (exp (gen) l-0) D (privk D))))
    ((recv (cat (exp (gen) (mul (rec l) l-0)) eA))
      (send (cat (exp (gen) (mul (rec l) l-0)) eA))))
  (label 37)
  (parent 19)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (B C D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self D) (peer C) (l l) (e eA)
    (lp l-1) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self C) (l l-1))
  (deflistener (cat (exp (gen) (mul eA (rec l-0))) l-1))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (1 1)) ((4 0) (0 1)) ((5 1) (1 3)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 C) (l D) (l-0 B))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk C) (privk D) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec l-0))) l-1))
    (exp (gen) (mul eA (rec l-0) l-1)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l) D (privk D)))
      (recv (enc "cert" (exp (gen) l-1) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-1) C (privk C))))
    ((recv (cat (exp (gen) (mul eA (rec l-0))) l-1))
      (send (cat (exp (gen) (mul eA (rec l-0))) l-1))))
  (label 38)
  (parent 20)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B C D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self D) (peer C) (l l) (e eA)
    (lp l-1) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self C) (l l-1))
  (deflistener (cat (exp (gen) (mul (rec l-0) l-1)) eA))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (1 1)) ((4 0) (0 1)) ((5 1) (1 3)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 C) (l D) (l-0 B))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk C) (privk D) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec l-0) l-1)) eA))
    (exp (gen) (mul eA (rec l-0) l-1)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l) D (privk D)))
      (recv (enc "cert" (exp (gen) l-1) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-1) C (privk C))))
    ((recv (cat (exp (gen) (mul (rec l-0) l-1)) eA))
      (send (cat (exp (gen) (mul (rec l-0) l-1)) eA))))
  (label 39)
  (parent 20)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (A B D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l-0) (e eA)
    (lp l-1) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-1) (e eB)
    (lp l) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l-1))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (deflistener (cat (exp (gen) (mul eB (rec l-0))) l))
  (precedes ((0 2) (1 3)) ((1 2) (5 0)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 0)) ((4 0) (5 0)) ((5 1) (0 3)))
  (absent (eB (exp (gen) l-1)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 B) (l-0 A) (l D))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq (eA (one)) (eA eB) ((mul eB l (rec l-0)) (one)))
  (non-orig (privk A) (privk B) (privk D) l-0 l-1)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eB (rec l-0))) l))
    (exp (gen) (mul eB l (rec l-0))) (0 3))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l-1) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A))))
    ((recv (cat (exp (gen) (mul eB (rec l-0))) l))
      (send (cat (exp (gen) (mul eB (rec l-0))) l))))
  (label 40)
  (parent 21)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l-0) (e eA)
    (lp l-1) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-1) (e eB)
    (lp l) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l-1))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (deflistener (cat (exp (gen) (mul l (rec l-0))) eB))
  (precedes ((0 2) (1 3)) ((1 2) (5 0)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 0)) ((4 0) (5 0)) ((5 1) (0 3)))
  (absent (eB (exp (gen) l-1)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 B) (l-0 A) (l D))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq (eA (one)) (eA eB) ((mul eB l (rec l-0)) (one)))
  (non-orig (privk A) (privk B) (privk D) l-0 l-1)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul l (rec l-0))) eB))
    (exp (gen) (mul eB l (rec l-0))) (0 3))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l-1) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A))))
    ((recv (cat (exp (gen) (mul l (rec l-0))) eB))
      (send (cat (exp (gen) (mul l (rec l-0))) eB))))
  (label 41)
  (parent 21)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (A B D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer D) (l l) (e eA)
    (lp l-1) (ep (mul eB (rec l) l-1)))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l-1) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l-1))
  (defstrand ltx-gen 1 (self A) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l-0))) l-1))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 1)) ((3 0) (1 1)) ((4 0) (0 0)) ((5 1) (1 3)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l-1)) (eA (exp (gen) l))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 D) (l A) (l-0 B))
    (foo
      ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l-1))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB (rec l) l-1) (one)))
  (non-orig (privk A) (privk B) (privk D) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec l-0))) l-1))
    (exp (gen) (mul eA (rec l-0) l-1)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) D (privk D)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-1)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-1) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l-1) D (privk D))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((recv (cat (exp (gen) (mul eA (rec l-0))) l-1))
      (send (cat (exp (gen) (mul eA (rec l-0))) l-1))))
  (label 42)
  (parent 22)
  (unrealized (0 3) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer D) (l l) (e eA)
    (lp l-1) (ep (mul eB (rec l) l-1)))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l-1) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l-1))
  (defstrand ltx-gen 1 (self A) (l l))
  (deflistener (cat (exp (gen) (mul (rec l-0) l-1)) eA))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 1)) ((3 0) (1 1)) ((4 0) (0 0)) ((5 1) (1 3)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l-1)) (eA (exp (gen) l))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 D) (l A) (l-0 B))
    (foo
      ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l-1))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB (rec l) l-1) (one)))
  (non-orig (privk A) (privk B) (privk D) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec l-0) l-1)) eA))
    (exp (gen) (mul eA (rec l-0) l-1)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) D (privk D)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-1)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-1) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l-1) D (privk D))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((recv (cat (exp (gen) (mul (rec l-0) l-1)) eA))
      (send (cat (exp (gen) (mul (rec l-0) l-1)) eA))))
  (label 43)
  (parent 22)
  (unrealized (0 3) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (A B D name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer A) (l l-1) (e eA)
    (lp l-1) (ep (mul eB l (rec l-1))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self A) (l l-1))
  (deflistener (cat (exp (gen) (mul (rec l-0) l-1)) eA))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 0)) ((5 1) (1 3)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 A) (l D) (l-0 B))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB l (rec l-1)) (one)))
  (non-orig (privk A) (privk B) (privk D) l-0 l-1)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec l-0) l-1)) eA))
    (exp (gen) (mul eA (rec l-0) l-1)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l-1) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) A (privk A)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-1))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-1) A (privk A))))
    ((recv (cat (exp (gen) (mul (rec l-0) l-1)) eA))
      (send (cat (exp (gen) (mul (rec l-0) l-1)) eA))))
  (label 44)
  (parent 23)
  (unrealized (0 3) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (A B C D name) (eB eA l l-0 l-1 l-2 rndx))
  (defstrand participant1 5 (key key) (self A) (peer C) (l l-0) (e eA)
    (lp l-2) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-1) (e eB)
    (lp l) (ep (mul eA (rec l-1) l-2)))
  (defstrand ltx-gen 1 (self B) (l l-1))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (defstrand ltx-gen 1 (self C) (l l-2))
  (deflistener (cat (exp (gen) (mul eA (rec l-1))) l-2))
  (precedes ((0 2) (6 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 0)) ((5 0) (0 1)) ((6 1) (1 3)))
  (absent (eB (exp (gen) l-1)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-2)))
  (fn-of ("principal-of" (l-2 C) (l-0 A) (l D) (l-1 B))
    (foo ((hash (exp (gen) (mul eA l-2)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-1) l-2) (one)) (eA eB)
    ((mul eB l (rec l-0)) (one)))
  (non-orig (privk A) (privk B) (privk C) (privk D) l-0 l-1)
  (uniq-gen eB eA l l-0 l-1 l-2)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec l-1))) l-2))
    (exp (gen) (mul eA (rec l-1) l-2)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) l-2) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-1) l-2)))
      (send key)) ((send (enc "cert" (exp (gen) l-1) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A))))
    ((send (enc "cert" (exp (gen) l-2) C (privk C))))
    ((recv (cat (exp (gen) (mul eA (rec l-1))) l-2))
      (send (cat (exp (gen) (mul eA (rec l-1))) l-2))))
  (label 45)
  (parent 24)
  (unrealized (0 3) (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B C D name) (eB eA l l-0 l-1 l-2 rndx))
  (defstrand participant1 5 (key key) (self A) (peer C) (l l-0) (e eA)
    (lp l-2) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-1) (e eB)
    (lp l) (ep (mul eA (rec l-1) l-2)))
  (defstrand ltx-gen 1 (self B) (l l-1))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (defstrand ltx-gen 1 (self C) (l l-2))
  (deflistener (cat (exp (gen) (mul (rec l-1) l-2)) eA))
  (precedes ((0 2) (6 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 0)) ((5 0) (0 1)) ((6 1) (1 3)))
  (absent (eB (exp (gen) l-1)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-2)))
  (fn-of ("principal-of" (l-2 C) (l-0 A) (l D) (l-1 B))
    (foo ((hash (exp (gen) (mul eA l-2)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-1) l-2) (one)) (eA eB)
    ((mul eB l (rec l-0)) (one)))
  (non-orig (privk A) (privk B) (privk C) (privk D) l-0 l-1)
  (uniq-gen eB eA l l-0 l-1 l-2)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec l-1) l-2)) eA))
    (exp (gen) (mul eA (rec l-1) l-2)) (1 3))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) l-2) C (privk C)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-1) l-2)))
      (send key)) ((send (enc "cert" (exp (gen) l-1) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A))))
    ((send (enc "cert" (exp (gen) l-2) C (privk C))))
    ((recv (cat (exp (gen) (mul (rec l-1) l-2)) eA))
      (send (cat (exp (gen) (mul (rec l-1) l-2)) eA))))
  (label 46)
  (parent 24)
  (unrealized (0 3) (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (B self name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer self) (l l) (e eA)
    (lp l-0) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l))) l-0))
  (defstrand ltx-gen 2 (self self) (l l-0))
  (precedes ((0 2) (3 0)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 1) (1 3)) ((4 0) (0 1)) ((4 1) (3 0)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 self) (l B))
    (foo ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk self) l)
  (uniq-gen eB eA l l-0)
  (operation nonce-test (displaced 3 5 ltx-gen 2) l-0 (4 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((recv (cat (exp (gen) (mul eA (rec l))) l-0))
      (send (cat (exp (gen) (mul eA (rec l))) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self (privk self))) (send l-0)))
  (label 47)
  (parent 25)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B self name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer self) (l l) (e eA)
    (lp l-1) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l-0) (e eB)
    (lp l-0) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self A) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l-0))) l-1))
  (defstrand ltx-gen 2 (self self) (l l-1))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((4 1) (1 3)) ((5 0) (0 1)) ((5 1) (4 0)))
  (absent (eB (exp (gen) l-0)) (eA (exp (gen) l)) (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 self) (l A) (l-0 B))
    (foo
      ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB (rec l) l-0) (one)))
  (non-orig (privk A) (privk B) (privk self) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test (displaced 4 6 ltx-gen 2) l-1 (5 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((recv (cat (exp (gen) (mul eA (rec l-0))) l-1))
      (send (cat (exp (gen) (mul eA (rec l-0))) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self (privk self))) (send l-1)))
  (label 48)
  (parent 29)
  (unrealized (0 3) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B self name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer self) (l l) (e eB)
    (lp l-0) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) (mul eB (rec l))) l-0))
  (defstrand ltx-gen 2 (self self) (l l-0))
  (precedes ((0 2) (1 3)) ((1 2) (3 0)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 1) (0 3)) ((4 0) (1 1)) ((4 1) (3 0)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) l-0)) (eA (exp (gen) l)))
  (fn-of ("principal-of" (l-0 self) (l B))
    (foo ((hash (exp (gen) (mul eA l)) (exp (gen) (mul eB l-0))) key)))
  (neq (eA (one)) (eA eB) ((mul eB (rec l) l-0) (one)))
  (non-orig (privk B) (privk self) l)
  (uniq-gen eB eA l l-0)
  (operation nonce-test (displaced 3 5 ltx-gen 2) l-0 (4 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) self (privk self)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((recv (cat (exp (gen) (mul eB (rec l))) l-0))
      (send (cat (exp (gen) (mul eB (rec l))) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self (privk self))) (send l-0)))
  (label 49)
  (parent 31)
  (unrealized (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B self name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer self) (l l) (e eA)
    (lp l-0) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer self) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l))) l-0))
  (defstrand ltx-gen 2 (self self) (l l-0))
  (precedes ((0 2) (3 0)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 1) (1 3)) ((4 0) (0 1)) ((4 0) (1 1)) ((4 1) (3 0)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) l-0)) (eA (exp (gen) l))
    (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 self) (l B))
    (foo
      ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB)
    ((mul eB (rec l) l-0) (one)))
  (non-orig (privk B) (privk self) l)
  (uniq-gen eB eA l l-0)
  (operation nonce-test (displaced 3 5 ltx-gen 2) l-0 (4 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) self (privk self)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((recv (cat (exp (gen) (mul eA (rec l))) l-0))
      (send (cat (exp (gen) (mul eA (rec l))) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self (privk self))) (send l-0)))
  (label 50)
  (parent 33)
  (unrealized (0 3) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B D self name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self B) (peer self) (l l-0)
    (e eA) (lp l-1) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l-0))) l-1))
  (defstrand ltx-gen 2 (self self) (l l-1))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 1) (1 3)) ((5 0) (0 1)) ((5 1) (4 0)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 self) (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB l (rec l-0)) (one)))
  (non-orig (privk B) (privk D) (privk self) l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test (displaced 4 6 ltx-gen 2) l-1 (5 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-1) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((recv (cat (exp (gen) (mul eA (rec l-0))) l-1))
      (send (cat (exp (gen) (mul eA (rec l-0))) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self (privk self))) (send l-1)))
  (label 51)
  (parent 35)
  (unrealized (0 3) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B D self name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self D) (peer self) (l l) (e eA)
    (lp l-1) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l-0))) l-1))
  (defstrand ltx-gen 2 (self self) (l l-1))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (1 1)) ((4 1) (1 3)) ((5 0) (0 1))
    ((5 1) (4 0)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 self) (l D) (l-0 B))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk D) (privk self) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test (displaced 4 6 ltx-gen 2) l-1 (5 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) D (privk D)))
      (recv (enc "cert" (exp (gen) l-1) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((recv (cat (exp (gen) (mul eA (rec l-0))) l-1))
      (send (cat (exp (gen) (mul eA (rec l-0))) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self (privk self))) (send l-1)))
  (label 52)
  (parent 38)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B self name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l) (e eA)
    (lp l-0) (ep (mul eB (rec l) l-1)))
  (defstrand participant2 5 (key key) (self B) (peer self) (l l-0)
    (e eB) (lp l-1) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self A) (l l))
  (deflistener (cat (exp (gen) (mul eB (rec l))) l-1))
  (defstrand ltx-gen 2 (self self) (l l-1))
  (precedes ((0 2) (1 3)) ((1 2) (4 0)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (4 0)) ((4 1) (0 3)) ((5 0) (1 1))
    ((5 1) (4 0)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l-1)) (eA (exp (gen) l))
    (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-1 self) (l-0 B) (l A))
    (foo
      ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l-1))) key)))
  (neq (eA (one)) (eA eB) ((mul eB (rec l) l-1) (one)))
  (non-orig (privk A) (privk B) (privk self) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test (displaced 3 6 ltx-gen 2) l-1 (5 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-1)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-1) self (privk self)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((recv (cat (exp (gen) (mul eB (rec l))) l-1))
      (send (cat (exp (gen) (mul eB (rec l))) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self (privk self))) (send l-1)))
  (label 53)
  (parent 40)
  (unrealized (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B self name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer self) (l l) (e eA)
    (lp l-1) (ep (mul eB (rec l) l-1)))
  (defstrand participant2 5 (key key) (self B) (peer self) (l l-0)
    (e eB) (lp l-1) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self A) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l-0))) l-1))
  (defstrand ltx-gen 2 (self self) (l l-1))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((4 1) (1 3)) ((5 0) (0 1)) ((5 0) (1 1))
    ((5 1) (4 0)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l-1)) (eA (exp (gen) l))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 self) (l A) (l-0 B))
    (foo
      ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l-1))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB (rec l) l-1) (one)))
  (non-orig (privk A) (privk B) (privk self) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test (displaced 3 6 ltx-gen 2) l-1 (5 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-1)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-1) self (privk self)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((recv (cat (exp (gen) (mul eA (rec l-0))) l-1))
      (send (cat (exp (gen) (mul eA (rec l-0))) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self (privk self))) (send l-1)))
  (label 54)
  (parent 42)
  (unrealized (0 3) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B D self name) (eB eA l l-0 l-1 l-2 rndx))
  (defstrand participant1 5 (key key) (self A) (peer self) (l l-0)
    (e eA) (lp l-2) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-1) (e eB)
    (lp l) (ep (mul eA (rec l-1) l-2)))
  (defstrand ltx-gen 1 (self B) (l l-1))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (deflistener (cat (exp (gen) (mul eA (rec l-1))) l-2))
  (defstrand ltx-gen 2 (self self) (l l-2))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 0)) ((5 1) (1 3)) ((6 0) (0 1))
    ((6 1) (5 0)))
  (absent (eB (exp (gen) l-1)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-2)))
  (fn-of ("principal-of" (l-2 self) (l-0 A) (l D) (l-1 B))
    (foo ((hash (exp (gen) (mul eA l-2)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-1) l-2) (one)) (eA eB)
    ((mul eB l (rec l-0)) (one)))
  (non-orig (privk A) (privk B) (privk D) (privk self) l-0 l-1)
  (uniq-gen eB eA l l-0 l-1 l-2)
  (operation nonce-test (displaced 5 7 ltx-gen 2) l-2 (6 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) l-2) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-1) l-2)))
      (send key)) ((send (enc "cert" (exp (gen) l-1) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A))))
    ((recv (cat (exp (gen) (mul eA (rec l-1))) l-2))
      (send (cat (exp (gen) (mul eA (rec l-1))) l-2)))
    ((send (enc "cert" (exp (gen) l-2) self (privk self))) (send l-2)))
  (label 55)
  (parent 45)
  (unrealized (0 3) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B self name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer self) (l l) (e eA)
    (lp l-0) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l))) l-0))
  (defstrand ltx-gen 2 (self self) (l l-0))
  (deflistener (cat (exp (gen) (rec l)) eA))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 1) (1 3)) ((4 0) (0 1)) ((4 1) (3 0)) ((5 1) (3 0)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 self) (l B))
    (foo ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk self) l)
  (uniq-gen eB eA l l-0)
  (operation nonce-test (added-listener (cat (exp (gen) (rec l)) eA))
    (exp (gen) (mul eA (rec l))) (3 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((recv (cat (exp (gen) (mul eA (rec l))) l-0))
      (send (cat (exp (gen) (mul eA (rec l))) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self (privk self))) (send l-0))
    ((recv (cat (exp (gen) (rec l)) eA))
      (send (cat (exp (gen) (rec l)) eA))))
  (label 56)
  (parent 47)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (A B self name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer self) (l l) (e eA)
    (lp l-1) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer B) (l l-0) (e eB)
    (lp l-0) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self A) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l-0))) l-1))
  (defstrand ltx-gen 2 (self self) (l l-1))
  (deflistener (cat (exp (gen) (rec l-0)) eA))
  (precedes ((0 2) (6 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((4 1) (1 3)) ((5 0) (0 1)) ((5 1) (4 0))
    ((6 1) (4 0)))
  (absent (eB (exp (gen) l-0)) (eA (exp (gen) l)) (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 self) (l A) (l-0 B))
    (foo
      ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB (rec l) l-0) (one)))
  (non-orig (privk A) (privk B) (privk self) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test (added-listener (cat (exp (gen) (rec l-0)) eA))
    (exp (gen) (mul eA (rec l-0))) (4 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((recv (cat (exp (gen) (mul eA (rec l-0))) l-1))
      (send (cat (exp (gen) (mul eA (rec l-0))) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self (privk self))) (send l-1))
    ((recv (cat (exp (gen) (rec l-0)) eA))
      (send (cat (exp (gen) (rec l-0)) eA))))
  (label 57)
  (parent 48)
  (unrealized (0 3) (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (B self name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer self) (l l) (e eB)
    (lp l-0) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) (mul eB (rec l))) l-0))
  (defstrand ltx-gen 2 (self self) (l l-0))
  (deflistener (cat (exp (gen) (rec l)) eB))
  (precedes ((0 2) (1 3)) ((1 2) (5 0)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 1) (0 3)) ((4 0) (1 1)) ((4 1) (3 0)) ((5 1) (3 0)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) l-0)) (eA (exp (gen) l)))
  (fn-of ("principal-of" (l-0 self) (l B))
    (foo ((hash (exp (gen) (mul eA l)) (exp (gen) (mul eB l-0))) key)))
  (neq (eA (one)) (eA eB) ((mul eB (rec l) l-0) (one)))
  (non-orig (privk B) (privk self) l)
  (uniq-gen eB eA l l-0)
  (operation nonce-test (added-listener (cat (exp (gen) (rec l)) eB))
    (exp (gen) (mul eB (rec l))) (3 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) self (privk self)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((recv (cat (exp (gen) (mul eB (rec l))) l-0))
      (send (cat (exp (gen) (mul eB (rec l))) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self (privk self))) (send l-0))
    ((recv (cat (exp (gen) (rec l)) eB))
      (send (cat (exp (gen) (rec l)) eB))))
  (label 58)
  (parent 49)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (B self name) (eB eA l l-0 rndx))
  (defstrand participant1 5 (key key) (self B) (peer self) (l l) (e eA)
    (lp l-0) (ep (mul eB (rec l) l-0)))
  (defstrand participant2 5 (key key) (self B) (peer self) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec l) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l))) l-0))
  (defstrand ltx-gen 2 (self self) (l l-0))
  (deflistener (cat (exp (gen) (rec l)) eA))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 1) (1 3)) ((4 0) (0 1)) ((4 0) (1 1)) ((4 1) (3 0))
    ((5 1) (3 0)))
  (absent (eB (exp (gen) l)) (eB (exp (gen) l-0)) (eA (exp (gen) l))
    (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 self) (l B))
    (foo
      ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l-0))) key)))
  (neq ((mul eA (rec l) l-0) (one)) (eA eB)
    ((mul eB (rec l) l-0) (one)))
  (non-orig (privk B) (privk self) l)
  (uniq-gen eB eA l l-0)
  (operation nonce-test (added-listener (cat (exp (gen) (rec l)) eA))
    (exp (gen) (mul eA (rec l))) (3 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-0)))
      (send key))
    ((recv (enc "cert" (exp (gen) l) B (privk B)))
      (recv (enc "cert" (exp (gen) l-0) self (privk self)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l) l-0)))
      (send key)) ((send (enc "cert" (exp (gen) l) B (privk B))))
    ((recv (cat (exp (gen) (mul eA (rec l))) l-0))
      (send (cat (exp (gen) (mul eA (rec l))) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self (privk self))) (send l-0))
    ((recv (cat (exp (gen) (rec l)) eA))
      (send (cat (exp (gen) (rec l)) eA))))
  (label 59)
  (parent 50)
  (unrealized (0 3) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (B D self name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self B) (peer self) (l l-0)
    (e eA) (lp l-1) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l-0))) l-1))
  (defstrand ltx-gen 2 (self self) (l l-1))
  (deflistener (cat (exp (gen) (rec l-0)) eA))
  (precedes ((0 2) (6 0)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 1) (1 3)) ((5 0) (0 1)) ((5 1) (4 0))
    ((6 1) (4 0)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 self) (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB l (rec l-0)) (one)))
  (non-orig (privk B) (privk D) (privk self) l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test (added-listener (cat (exp (gen) (rec l-0)) eA))
    (exp (gen) (mul eA (rec l-0))) (4 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-1) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((recv (cat (exp (gen) (mul eA (rec l-0))) l-1))
      (send (cat (exp (gen) (mul eA (rec l-0))) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self (privk self))) (send l-1))
    ((recv (cat (exp (gen) (rec l-0)) eA))
      (send (cat (exp (gen) (rec l-0)) eA))))
  (label 60)
  (parent 51)
  (unrealized (0 3) (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (B D self name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self D) (peer self) (l l) (e eA)
    (lp l-1) (ep eB))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l-0))) l-1))
  (defstrand ltx-gen 2 (self self) (l l-1))
  (deflistener (cat (exp (gen) (rec l-0)) eA))
  (precedes ((0 2) (6 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (1 1)) ((4 1) (1 3)) ((5 0) (0 1))
    ((5 1) (4 0)) ((6 1) (4 0)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 self) (l D) (l-0 B))
    (foo ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB) (eB (one)))
  (non-orig (privk B) (privk D) (privk self) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test (added-listener (cat (exp (gen) (rec l-0)) eA))
    (exp (gen) (mul eA (rec l-0))) (4 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) D (privk D)))
      (recv (enc "cert" (exp (gen) l-1) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) eB)) (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((recv (cat (exp (gen) (mul eA (rec l-0))) l-1))
      (send (cat (exp (gen) (mul eA (rec l-0))) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self (privk self))) (send l-1))
    ((recv (cat (exp (gen) (rec l-0)) eA))
      (send (cat (exp (gen) (rec l-0)) eA))))
  (label 61)
  (parent 52)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (A B self name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l) (e eA)
    (lp l-0) (ep (mul eB (rec l) l-1)))
  (defstrand participant2 5 (key key) (self B) (peer self) (l l-0)
    (e eB) (lp l-1) (ep eA))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self A) (l l))
  (deflistener (cat (exp (gen) (mul eB (rec l))) l-1))
  (defstrand ltx-gen 2 (self self) (l l-1))
  (deflistener (cat (exp (gen) (rec l)) eB))
  (precedes ((0 2) (1 3)) ((1 2) (6 0)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (6 0)) ((4 1) (0 3)) ((5 0) (1 1))
    ((5 1) (4 0)) ((6 1) (4 0)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l-1)) (eA (exp (gen) l))
    (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-1 self) (l-0 B) (l A))
    (foo
      ((hash (exp (gen) (mul eA l-0)) (exp (gen) (mul eB l-1))) key)))
  (neq (eA (one)) (eA eB) ((mul eB (rec l) l-1) (one)))
  (non-orig (privk A) (privk B) (privk self) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test (added-listener (cat (exp (gen) (rec l)) eB))
    (exp (gen) (mul eB (rec l))) (4 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-1)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-1) self (privk self)))
      (send (exp (gen) eB)) (recv (exp (gen) eA)) (send key))
    ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((recv (cat (exp (gen) (mul eB (rec l))) l-1))
      (send (cat (exp (gen) (mul eB (rec l))) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self (privk self))) (send l-1))
    ((recv (cat (exp (gen) (rec l)) eB))
      (send (cat (exp (gen) (rec l)) eB))))
  (label 62)
  (parent 53)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (A B self name) (eB eA l l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self A) (peer self) (l l) (e eA)
    (lp l-1) (ep (mul eB (rec l) l-1)))
  (defstrand participant2 5 (key key) (self B) (peer self) (l l-0)
    (e eB) (lp l-1) (ep (mul eA (rec l-0) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self A) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec l-0))) l-1))
  (defstrand ltx-gen 2 (self self) (l l-1))
  (deflistener (cat (exp (gen) (rec l-0)) eA))
  (precedes ((0 2) (6 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((4 1) (1 3)) ((5 0) (0 1)) ((5 0) (1 1))
    ((5 1) (4 0)) ((6 1) (4 0)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l-1)) (eA (exp (gen) l))
    (eA (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 self) (l A) (l-0 B))
    (foo
      ((hash (exp (gen) (mul eA l-1)) (exp (gen) (mul eB l-1))) key)))
  (neq ((mul eA (rec l-0) l-1) (one)) (eA eB)
    ((mul eB (rec l) l-1) (one)))
  (non-orig (privk A) (privk B) (privk self) l l-0)
  (uniq-gen eB eA l l-0 l-1)
  (operation nonce-test (added-listener (cat (exp (gen) (rec l-0)) eA))
    (exp (gen) (mul eA (rec l-0))) (4 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) l-1) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB (rec l) l-1)))
      (send key))
    ((recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (recv (enc "cert" (exp (gen) l-1) self (privk self)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-0) l-1)))
      (send key)) ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((recv (cat (exp (gen) (mul eA (rec l-0))) l-1))
      (send (cat (exp (gen) (mul eA (rec l-0))) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self (privk self))) (send l-1))
    ((recv (cat (exp (gen) (rec l-0)) eA))
      (send (cat (exp (gen) (rec l-0)) eA))))
  (label 63)
  (parent 54)
  (unrealized (0 3) (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (A B D self name) (eB eA l l-0 l-1 l-2 rndx))
  (defstrand participant1 5 (key key) (self A) (peer self) (l l-0)
    (e eA) (lp l-2) (ep (mul eB l (rec l-0))))
  (defstrand participant2 5 (key key) (self B) (peer D) (l l-1) (e eB)
    (lp l) (ep (mul eA (rec l-1) l-2)))
  (defstrand ltx-gen 1 (self B) (l l-1))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (deflistener (cat (exp (gen) (mul eA (rec l-1))) l-2))
  (defstrand ltx-gen 2 (self self) (l l-2))
  (deflistener (cat (exp (gen) (rec l-1)) eA))
  (precedes ((0 2) (7 0)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (1 1)) ((4 0) (0 0)) ((5 1) (1 3)) ((6 0) (0 1))
    ((6 1) (5 0)) ((7 1) (5 0)))
  (absent (eB (exp (gen) l-1)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l-2)))
  (fn-of ("principal-of" (l-2 self) (l-0 A) (l D) (l-1 B))
    (foo ((hash (exp (gen) (mul eA l-2)) (exp (gen) (mul eB l))) key)))
  (neq ((mul eA (rec l-1) l-2) (one)) (eA eB)
    ((mul eB l (rec l-0)) (one)))
  (non-orig (privk A) (privk B) (privk D) (privk self) l-0 l-1)
  (uniq-gen eB eA l l-0 l-1 l-2)
  (operation nonce-test (added-listener (cat (exp (gen) (rec l-1)) eA))
    (exp (gen) (mul eA (rec l-1))) (5 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) l-2) self (privk self)))
      (send (exp (gen) eA)) (recv (exp (gen) (mul eB l (rec l-0))))
      (send key))
    ((recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (recv (enc "cert" (exp (gen) l) D (privk D)))
      (send (exp (gen) eB)) (recv (exp (gen) (mul eA (rec l-1) l-2)))
      (send key)) ((send (enc "cert" (exp (gen) l-1) B (privk B))))
    ((send (enc "cert" (exp (gen) l) D (privk D))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A))))
    ((recv (cat (exp (gen) (mul eA (rec l-1))) l-2))
      (send (cat (exp (gen) (mul eA (rec l-1))) l-2)))
    ((send (enc "cert" (exp (gen) l-2) self (privk self))) (send l-2))
    ((recv (cat (exp (gen) (rec l-1)) eA))
      (send (cat (exp (gen) (rec l-1)) eA))))
  (label 64)
  (parent 55)
  (unrealized (0 3) (7 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol iadh-umx diffie-hellman
  (defrole participant1
    (vars (l e rndx) (lp ep expt) (self peer name) (key data))
    (trace (recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e)) (recv (exp (gen) ep)) (send key))
    (uniq-gen e)
    (fn-of
      (foo ((hash (exp (gen) (mul e lp)) (exp (gen) (mul l ep))) key)))
    (neq (ep (one)))
    (absent (e (exp (gen) l)) (e (exp (gen) lp))))
  (defrole participant2
    (vars (l e rndx) (lp ep expt) (self peer name) (key data))
    (trace (recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e)) (recv (exp (gen) ep)) (send key))
    (uniq-gen e)
    (fn-of
      (foo ((hash (exp (gen) (mul l ep)) (exp (gen) (mul e lp))) key)))
    (neq (ep (one)))
    (absent (e (exp (gen) l)) (e (exp (gen) lp))))
  (defrole ltx-gen
    (vars (self name) (l rndx))
    (trace (send (enc "cert" (exp (gen) l) self (privk self))) (send l))
    (uniq-gen l)
    (fn-of ("principal-of" (l self)))))

(defskeleton iadh-umx
  (vars (key data) (A B self peer name) (e1 e2 l rndx) (lp expt)
    (l-0 rndx) (lp-0 expt))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l) (e e1)
    (lp lp) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l-0) (e e2)
    (lp lp-0))
  (deflistener (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l))))
  (absent (e2 (exp (gen) l-0)) (e2 (exp (gen) lp-0)) (e1 (exp (gen) l))
    (e1 (exp (gen) lp)))
  (fn-of
    (foo ((hash (exp (gen) (mul e1 lp)) (exp (gen) (mul e2 l))) key)))
  (neq (e2 (one)))
  (non-orig (privk A) (privk B))
  (uniq-gen e1 e2)
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l-0) self (privk self)))
      (recv (enc "cert" (exp (gen) lp-0) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l))))
      (send (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l))))))
  (label 65)
  (unrealized (0 0) (0 1) (0 3) (2 0))
  (preskeleton)
  (origs)
  (comment "Not a skeleton"))

(defskeleton iadh-umx
  (vars (key data) (A B self peer name) (e1 e2 l rndx) (lp expt)
    (l-0 rndx) (lp-0 expt))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l) (e e1)
    (lp lp) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l-0) (e e2)
    (lp lp-0))
  (deflistener (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l))))
  (precedes ((0 2) (2 0)) ((1 2) (0 3)) ((1 2) (2 0)))
  (absent (e2 (exp (gen) l-0)) (e2 (exp (gen) lp-0)) (e1 (exp (gen) l))
    (e1 (exp (gen) lp)))
  (fn-of
    (foo ((hash (exp (gen) (mul e1 lp)) (exp (gen) (mul e2 l))) key)))
  (neq (e2 (one)))
  (non-orig (privk A) (privk B))
  (uniq-gen e1 e2)
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l-0) self (privk self)))
      (recv (enc "cert" (exp (gen) lp-0) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l))))
      (send (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l))))))
  (label 66)
  (parent 65)
  (unrealized (0 0) (0 1))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B name) (l rndx) (lp expt) (e2 rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l) (e e2)
    (lp lp) (ep e2))
  (deflistener (hash (exp (gen) (mul lp e2)) (exp (gen) (mul l e2))))
  (precedes ((0 2) (1 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)))
  (fn-of
    (foo ((hash (exp (gen) (mul lp e2)) (exp (gen) (mul l e2))) key)))
  (neq (e2 (one)))
  (non-orig (privk A) (privk B))
  (uniq-gen e2)
  (operation collapsed 1 0)
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e2)) (recv (exp (gen) e2)) (send key))
    ((recv (hash (exp (gen) (mul lp e2)) (exp (gen) (mul l e2))))
      (send (hash (exp (gen) (mul lp e2)) (exp (gen) (mul l e2))))))
  (label 67)
  (parent 66)
  (unrealized (0 0) (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B self peer name) (e1 e2 rndx) (lp expt) (l rndx)
    (lp-0 expt) (l-0 rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l-0) (e e1)
    (lp lp) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp-0))
  (deflistener (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (precedes ((0 2) (2 0)) ((1 2) (0 3)) ((1 2) (2 0)) ((3 0) (0 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp-0)) (e1 (exp (gen) l-0))
    (e1 (exp (gen) lp)))
  (fn-of ("principal-of" (l-0 A))
    (foo ((hash (exp (gen) (mul e1 lp)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk A) (privk B))
  (uniq-gen e1 e2 l-0)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-0) A (privk A)) (0 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp-0) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0)))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A)))))
  (label 68)
  (parent 66)
  (unrealized (0 1) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B name) (lp expt) (e2 l rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l) (e e2)
    (lp lp) (ep e2))
  (deflistener (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
  (defstrand ltx-gen 1 (self A) (l l))
  (precedes ((0 2) (1 0)) ((2 0) (0 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)))
  (fn-of ("principal-of" (l A))
    (foo ((hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))) key)))
  (neq (e2 (one)))
  (non-orig (privk A) (privk B))
  (uniq-gen e2 l)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l) A (privk A)) (0 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e2)) (recv (exp (gen) e2)) (send key))
    ((recv (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
      (send (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l)))))
    ((send (enc "cert" (exp (gen) l) A (privk A)))))
  (label 69)
  (parent 67)
  (unrealized (0 1) (1 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B self peer name) (e1 e2 rndx) (lp expt) (l rndx)
    (lp-0 expt) (l-0 rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l-0) (e e1)
    (lp lp) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp-0))
  (deflistener (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (deflistener (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (4 0)) ((3 0) (0 0))
    ((4 1) (2 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp-0)) (e1 (exp (gen) l-0))
    (e1 (exp (gen) lp)))
  (fn-of ("principal-of" (l-0 A))
    (foo ((hash (exp (gen) (mul e1 lp)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk A) (privk B))
  (uniq-gen e1 e2 l-0)
  (operation encryption-test
    (added-listener
      (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
    (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))) (2 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp-0) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0)))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A))))
    ((recv (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
      (send (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))))
  (label 70)
  (parent 68)
  (unrealized (0 1) (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B name) (lp expt) (e2 l rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l) (e e2)
    (lp lp) (ep e2))
  (deflistener (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
  (defstrand ltx-gen 1 (self A) (l l))
  (deflistener (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
  (precedes ((0 2) (3 0)) ((2 0) (0 0)) ((3 1) (1 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)))
  (fn-of ("principal-of" (l A))
    (foo ((hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))) key)))
  (neq (e2 (one)))
  (non-orig (privk A) (privk B))
  (uniq-gen e2 l)
  (operation encryption-test
    (added-listener
      (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
    (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))) (1 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e2)) (recv (exp (gen) e2)) (send key))
    ((recv (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
      (send (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l)))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((recv (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
      (send (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))))
  (label 71)
  (parent 69)
  (unrealized (0 1) (3 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B self peer name) (e1 e2 rndx) (lp expt) (l rndx)
    (lp-0 expt) (l-0 rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l-0) (e e1)
    (lp lp) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp-0))
  (deflistener (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (deflistener (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) e1) l-0))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((1 2) (4 0)) ((3 0) (0 0))
    ((4 1) (2 0)) ((5 1) (4 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp-0)) (e1 (exp (gen) l-0))
    (e1 (exp (gen) lp)))
  (fn-of ("principal-of" (l-0 A))
    (foo ((hash (exp (gen) (mul e1 lp)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk A) (privk B))
  (uniq-gen e1 e2 l-0)
  (operation nonce-test (added-listener (cat (exp (gen) e1) l-0))
    (exp (gen) (mul e1 l-0)) (4 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp-0) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0)))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A))))
    ((recv (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
      (send (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) e1) l-0)) (send (cat (exp (gen) e1) l-0))))
  (label 72)
  (parent 70)
  (unrealized (0 1) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B self peer name) (e1 e2 rndx) (lp expt) (l rndx)
    (lp-0 expt) (l-0 rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l-0) (e e1)
    (lp lp) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp-0))
  (deflistener (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (deflistener (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) l-0) e1))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((1 2) (4 0)) ((3 0) (0 0))
    ((4 1) (2 0)) ((5 1) (4 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp-0)) (e1 (exp (gen) l-0))
    (e1 (exp (gen) lp)))
  (fn-of ("principal-of" (l-0 A))
    (foo ((hash (exp (gen) (mul e1 lp)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk A) (privk B))
  (uniq-gen e1 e2 l-0)
  (operation nonce-test (added-listener (cat (exp (gen) l-0) e1))
    (exp (gen) (mul e1 l-0)) (4 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) A (privk A)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp-0) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0)))))
    ((send (enc "cert" (exp (gen) l-0) A (privk A))))
    ((recv (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
      (send (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) l-0) e1)) (send (cat (exp (gen) l-0) e1))))
  (label 73)
  (parent 70)
  (unrealized (0 1) (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (A B name) (lp expt) (e2 l rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l) (e e2)
    (lp lp) (ep e2))
  (deflistener (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
  (defstrand ltx-gen 1 (self A) (l l))
  (deflistener (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) e2) l))
  (precedes ((0 2) (4 0)) ((2 0) (0 0)) ((3 1) (1 0)) ((4 1) (3 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)))
  (fn-of ("principal-of" (l A))
    (foo ((hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))) key)))
  (neq (e2 (one)))
  (non-orig (privk A) (privk B))
  (uniq-gen e2 l)
  (operation nonce-test (added-listener (cat (exp (gen) e2) l))
    (exp (gen) (mul e2 l)) (3 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e2)) (recv (exp (gen) e2)) (send key))
    ((recv (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
      (send (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l)))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((recv (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
      (send (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) e2) l)) (send (cat (exp (gen) e2) l))))
  (label 74)
  (parent 71)
  (unrealized (0 1) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (A B name) (lp expt) (e2 l rndx))
  (defstrand participant1 5 (key key) (self A) (peer B) (l l) (e e2)
    (lp lp) (ep e2))
  (deflistener (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
  (defstrand ltx-gen 1 (self A) (l l))
  (deflistener (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) l) e2))
  (precedes ((0 2) (4 0)) ((2 0) (0 0)) ((3 1) (1 0)) ((4 1) (3 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)))
  (fn-of ("principal-of" (l A))
    (foo ((hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))) key)))
  (neq (e2 (one)))
  (non-orig (privk A) (privk B))
  (uniq-gen e2 l)
  (operation nonce-test (added-listener (cat (exp (gen) l) e2))
    (exp (gen) (mul e2 l)) (3 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) A (privk A)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e2)) (recv (exp (gen) e2)) (send key))
    ((recv (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
      (send (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l)))))
    ((send (enc "cert" (exp (gen) l) A (privk A))))
    ((recv (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
      (send (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) l) e2)) (send (cat (exp (gen) l) e2))))
  (label 75)
  (parent 71)
  (unrealized (0 1) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (B self peer self-0 name) (e1 e2 rndx) (lp expt)
    (l rndx) (lp-0 expt) (l-0 rndx))
  (defstrand participant1 5 (key key) (self self-0) (peer B) (l l-0)
    (e e1) (lp lp) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp-0))
  (deflistener (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) e1) l-0))
  (defstrand ltx-gen 2 (self self-0) (l l-0))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (3 0)) ((3 1) (2 0))
    ((4 1) (3 0)) ((5 0) (0 0)) ((5 1) (4 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp-0)) (e1 (exp (gen) l-0))
    (e1 (exp (gen) lp)))
  (fn-of ("principal-of" (l-0 self-0))
    (foo ((hash (exp (gen) (mul e1 lp)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk B) (privk self-0))
  (uniq-gen e1 e2 l-0)
  (operation nonce-test (displaced 3 6 ltx-gen 2) l-0 (5 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp-0) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0))))
      (send (cat (exp (gen) (mul e2 lp)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) e1) l-0)) (send (cat (exp (gen) e1) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send l-0)))
  (label 76)
  (parent 72)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B self name) (lp expt) (e2 l rndx))
  (defstrand participant1 5 (key key) (self self) (peer B) (l l) (e e2)
    (lp lp) (ep e2))
  (deflistener (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) e2) l))
  (defstrand ltx-gen 2 (self self) (l l))
  (precedes ((0 2) (3 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 0) (0 0))
    ((4 1) (3 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)))
  (fn-of ("principal-of" (l self))
    (foo ((hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))) key)))
  (neq (e2 (one)))
  (non-orig (privk B) (privk self))
  (uniq-gen e2 l)
  (operation nonce-test (displaced 2 5 ltx-gen 2) l (4 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) B (privk B)))
      (send (exp (gen) e2)) (recv (exp (gen) e2)) (send key))
    ((recv (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
      (send (hash (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l))))
      (send (cat (exp (gen) (mul lp e2)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) e2) l)) (send (cat (exp (gen) e2) l)))
    ((send (enc "cert" (exp (gen) l) self (privk self))) (send l)))
  (label 77)
  (parent 74)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (self peer self-0 name) (e1 e2 l rndx) (lp expt)
    (l-0 rndx))
  (defstrand participant1 5 (key key) (self self-0) (peer self-0)
    (l l-0) (e e1) (lp l-0) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp))
  (deflistener (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) e1) l-0))
  (defstrand ltx-gen 2 (self self-0) (l l-0))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (3 0)) ((3 1) (2 0))
    ((4 1) (3 0)) ((5 0) (0 0)) ((5 1) (4 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)) (e1 (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 self-0))
    (foo
      ((hash (exp (gen) (mul e1 l-0)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk self-0))
  (uniq-gen e1 e2 l-0)
  (operation encryption-test (displaced 6 5 ltx-gen 1)
    (enc "cert" (exp (gen) l-1) B (privk B)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e1 l-0))))
      (send (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) e1) l-0)) (send (cat (exp (gen) e1) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send l-0)))
  (label 78)
  (parent 76)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B self peer self-0 name) (e1 e2 l rndx) (lp expt)
    (l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self self-0) (peer B) (l l-0)
    (e e1) (lp l-1) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp))
  (deflistener (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) e1) l-0))
  (defstrand ltx-gen 2 (self self-0) (l l-0))
  (defstrand ltx-gen 1 (self B) (l l-1))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (3 0)) ((3 1) (2 0))
    ((4 1) (3 0)) ((5 0) (0 0)) ((5 1) (4 0)) ((6 0) (0 1)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)) (e1 (exp (gen) l-0))
    (e1 (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 B) (l-0 self-0))
    (foo
      ((hash (exp (gen) (mul e1 l-1)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk B) (privk self-0))
  (uniq-gen e1 e2 l-0 l-1)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-1) B (privk B)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
      (send (cat (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) e1) l-0)) (send (cat (exp (gen) e1) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send l-0)) ((send (enc "cert" (exp (gen) l-1) B (privk B)))))
  (label 79)
  (parent 76)
  (unrealized (3 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (self name) (e2 l rndx))
  (defstrand participant1 5 (key key) (self self) (peer self) (l l)
    (e e2) (lp l) (ep e2))
  (deflistener (hash (exp (gen) (mul e2 l)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) (mul e2 l)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) e2) l))
  (defstrand ltx-gen 2 (self self) (l l))
  (precedes ((0 2) (3 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 0) (0 0))
    ((4 1) (3 0)))
  (absent (e2 (exp (gen) l)))
  (fn-of ("principal-of" (l self))
    (foo ((hash (exp (gen) (mul e2 l)) (exp (gen) (mul e2 l))) key)))
  (neq (e2 (one)))
  (non-orig (privk self))
  (uniq-gen e2 l)
  (operation encryption-test (displaced 5 4 ltx-gen 1)
    (enc "cert" (exp (gen) l-0) B (privk B)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) l) self (privk self)))
      (send (exp (gen) e2)) (recv (exp (gen) e2)) (send key))
    ((recv (hash (exp (gen) (mul e2 l)) (exp (gen) (mul e2 l))))
      (send (hash (exp (gen) (mul e2 l)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) (mul e2 l)) (exp (gen) (mul e2 l))))
      (send (cat (exp (gen) (mul e2 l)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) e2) l)) (send (cat (exp (gen) e2) l)))
    ((send (enc "cert" (exp (gen) l) self (privk self))) (send l)))
  (label 80)
  (parent 77)
  (unrealized)
  (shape)
  (maps)
  (origs))

(defskeleton iadh-umx
  (vars (key data) (B self name) (e2 l l-0 rndx))
  (defstrand participant1 5 (key key) (self self) (peer B) (l l) (e e2)
    (lp l-0) (ep e2))
  (deflistener (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) e2) l))
  (defstrand ltx-gen 2 (self self) (l l))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (precedes ((0 2) (3 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 0) (0 0))
    ((4 1) (3 0)) ((5 0) (0 1)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 B) (l self))
    (foo ((hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))) key)))
  (neq (e2 (one)))
  (non-orig (privk B) (privk self))
  (uniq-gen e2 l l-0)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-0) B (privk B)) (0 1))
  (traces
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) e2)) (recv (exp (gen) e2)) (send key))
    ((recv (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
      (send (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
      (send (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) e2) l)) (send (cat (exp (gen) e2) l)))
    ((send (enc "cert" (exp (gen) l) self (privk self))) (send l))
    ((send (enc "cert" (exp (gen) l-0) B (privk B)))))
  (label 81)
  (parent 77)
  (unrealized (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (self peer self-0 name) (e1 e2 l rndx) (lp expt)
    (l-0 rndx))
  (defstrand participant1 5 (key key) (self self-0) (peer self-0)
    (l l-0) (e e1) (lp l-0) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp))
  (deflistener (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) e1) l-0))
  (defstrand ltx-gen 2 (self self-0) (l l-0))
  (precedes ((0 2) (3 0)) ((1 2) (0 3)) ((1 2) (2 0)) ((3 1) (2 0))
    ((4 0) (0 0)) ((4 1) (3 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)) (e1 (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 self-0))
    (foo
      ((hash (exp (gen) (mul e1 l-0)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk self-0))
  (uniq-gen e1 e2 l-0)
  (operation generalization deleted (3 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) e1) l-0)) (send (cat (exp (gen) e1) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send l-0)))
  (label 82)
  (parent 78)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B self peer self-0 name) (e1 e2 l rndx) (lp expt)
    (l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self self-0) (peer B) (l l-0)
    (e e1) (lp l-1) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp))
  (deflistener (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) e1) l-0))
  (defstrand ltx-gen 2 (self self-0) (l l-0))
  (defstrand ltx-gen 1 (self B) (l l-1))
  (deflistener (cat (exp (gen) e2) l-1))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (7 0)) ((3 1) (2 0))
    ((4 1) (3 0)) ((5 0) (0 0)) ((5 1) (4 0)) ((6 0) (0 1))
    ((6 0) (7 0)) ((7 1) (3 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)) (e1 (exp (gen) l-0))
    (e1 (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 B) (l-0 self-0))
    (foo
      ((hash (exp (gen) (mul e1 l-1)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk B) (privk self-0))
  (uniq-gen e1 e2 l-0 l-1)
  (operation nonce-test (added-listener (cat (exp (gen) e2) l-1))
    (exp (gen) (mul e2 l-1)) (3 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
      (send (cat (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) e1) l-0)) (send (cat (exp (gen) e1) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send l-0)) ((send (enc "cert" (exp (gen) l-1) B (privk B))))
    ((recv (cat (exp (gen) e2) l-1)) (send (cat (exp (gen) e2) l-1))))
  (label 83)
  (parent 79)
  (unrealized (7 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B self peer self-0 name) (e1 e2 l rndx) (lp expt)
    (l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self self-0) (peer B) (l l-0)
    (e e1) (lp l-1) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp))
  (deflistener (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) e1) l-0))
  (defstrand ltx-gen 2 (self self-0) (l l-0))
  (defstrand ltx-gen 1 (self B) (l l-1))
  (deflistener (cat (exp (gen) l-1) e2))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (7 0)) ((3 1) (2 0))
    ((4 1) (3 0)) ((5 0) (0 0)) ((5 1) (4 0)) ((6 0) (0 1))
    ((6 0) (7 0)) ((7 1) (3 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)) (e1 (exp (gen) l-0))
    (e1 (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 B) (l-0 self-0))
    (foo
      ((hash (exp (gen) (mul e1 l-1)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk B) (privk self-0))
  (uniq-gen e1 e2 l-0 l-1)
  (operation nonce-test (added-listener (cat (exp (gen) l-1) e2))
    (exp (gen) (mul e2 l-1)) (3 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (recv (enc "cert" (exp (gen) l-1) B (privk B)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
      (send (cat (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) e1) l-0)) (send (cat (exp (gen) e1) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send l-0)) ((send (enc "cert" (exp (gen) l-1) B (privk B))))
    ((recv (cat (exp (gen) l-1) e2)) (send (cat (exp (gen) l-1) e2))))
  (label 84)
  (parent 79)
  (unrealized (7 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (B self name) (e2 l l-0 rndx))
  (defstrand participant1 5 (key key) (self self) (peer B) (l l) (e e2)
    (lp l-0) (ep e2))
  (deflistener (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) e2) l))
  (defstrand ltx-gen 2 (self self) (l l))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (deflistener (cat (exp (gen) e2) l-0))
  (precedes ((0 2) (3 0)) ((0 2) (6 0)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 0) (0 0)) ((4 1) (3 0)) ((5 0) (0 1)) ((6 1) (2 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 B) (l self))
    (foo ((hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))) key)))
  (neq (e2 (one)))
  (non-orig (privk B) (privk self))
  (uniq-gen e2 l l-0)
  (operation nonce-test (added-listener (cat (exp (gen) e2) l-0))
    (exp (gen) (mul e2 l-0)) (2 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) e2)) (recv (exp (gen) e2)) (send key))
    ((recv (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
      (send (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
      (send (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) e2) l)) (send (cat (exp (gen) e2) l)))
    ((send (enc "cert" (exp (gen) l) self (privk self))) (send l))
    ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((recv (cat (exp (gen) e2) l-0)) (send (cat (exp (gen) e2) l-0))))
  (label 85)
  (parent 81)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (B self name) (e2 l l-0 rndx))
  (defstrand participant1 5 (key key) (self self) (peer B) (l l) (e e2)
    (lp l-0) (ep e2))
  (deflistener (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) e2) l))
  (defstrand ltx-gen 2 (self self) (l l))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (deflistener (cat (exp (gen) l-0) e2))
  (precedes ((0 2) (3 0)) ((0 2) (6 0)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 0) (0 0)) ((4 1) (3 0)) ((5 0) (0 1)) ((6 1) (2 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 B) (l self))
    (foo ((hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))) key)))
  (neq (e2 (one)))
  (non-orig (privk B) (privk self))
  (uniq-gen e2 l l-0)
  (operation nonce-test (added-listener (cat (exp (gen) l-0) e2))
    (exp (gen) (mul e2 l-0)) (2 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) l-0) B (privk B)))
      (send (exp (gen) e2)) (recv (exp (gen) e2)) (send key))
    ((recv (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
      (send (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
      (send (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) e2) l)) (send (cat (exp (gen) e2) l)))
    ((send (enc "cert" (exp (gen) l) self (privk self))) (send l))
    ((send (enc "cert" (exp (gen) l-0) B (privk B))))
    ((recv (cat (exp (gen) l-0) e2)) (send (cat (exp (gen) l-0) e2))))
  (label 86)
  (parent 81)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton iadh-umx
  (vars (key data) (self peer self-0 name) (e1 e2 l rndx) (lp expt)
    (l-0 rndx))
  (defstrand participant1 5 (key key) (self self-0) (peer self-0)
    (l l-0) (e e1) (lp l-0) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp))
  (deflistener (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e1 l-0))))
  (defstrand ltx-gen 2 (self self-0) (l l-0))
  (precedes ((0 2) (2 0)) ((1 2) (0 3)) ((1 2) (2 0)) ((3 0) (0 0))
    ((3 1) (2 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)) (e1 (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 self-0))
    (foo
      ((hash (exp (gen) (mul e1 l-0)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk self-0))
  (uniq-gen e1 e2 l-0)
  (operation generalization deleted (3 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e1 l-0)))))
    ((send (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send l-0)))
  (label 87)
  (parent 82)
  (unrealized)
  (shape)
  (maps
    ((0 1 2)
      ((e1 e1) (e2 e2) (l l-0) (lp l-0) (A self-0) (B self-0) (key key)
        (l-0 l) (lp-0 lp) (self self) (peer peer))))
  (origs))

(defskeleton iadh-umx
  (vars (key data) (self peer self-0 self-1 name) (e1 e2 l rndx)
    (lp expt) (l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self self-0) (peer self-1)
    (l l-0) (e e1) (lp l-1) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp))
  (deflistener (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) e1) l-0))
  (defstrand ltx-gen 2 (self self-0) (l l-0))
  (deflistener (cat (exp (gen) e2) l-1))
  (defstrand ltx-gen 2 (self self-1) (l l-1))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (6 0)) ((3 1) (2 0))
    ((4 1) (3 0)) ((5 0) (0 0)) ((5 1) (4 0)) ((6 1) (3 0))
    ((7 0) (0 1)) ((7 1) (6 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)) (e1 (exp (gen) l-0))
    (e1 (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 self-1) (l-0 self-0))
    (foo
      ((hash (exp (gen) (mul e1 l-1)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk self-0) (privk self-1))
  (uniq-gen e1 e2 l-0 l-1)
  (operation nonce-test (displaced 6 8 ltx-gen 2) l-1 (7 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (recv (enc "cert" (exp (gen) l-1) self-1 (privk self-1)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
      (send (cat (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) e1) l-0)) (send (cat (exp (gen) e1) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send l-0))
    ((recv (cat (exp (gen) e2) l-1)) (send (cat (exp (gen) e2) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self-1 (privk self-1)))
      (send l-1)))
  (label 88)
  (parent 83)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (self self-0 name) (e2 l l-0 rndx))
  (defstrand participant1 5 (key key) (self self) (peer self-0) (l l)
    (e e2) (lp l-0) (ep e2))
  (deflistener (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
  (deflistener (cat (exp (gen) e2) l))
  (defstrand ltx-gen 2 (self self) (l l))
  (deflistener (cat (exp (gen) e2) l-0))
  (defstrand ltx-gen 2 (self self-0) (l l-0))
  (precedes ((0 2) (3 0)) ((0 2) (5 0)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 0) (0 0)) ((4 1) (3 0)) ((5 1) (2 0)) ((6 0) (0 1))
    ((6 1) (5 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 self-0) (l self))
    (foo ((hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))) key)))
  (neq (e2 (one)))
  (non-orig (privk self) (privk self-0))
  (uniq-gen e2 l l-0)
  (operation nonce-test (displaced 5 7 ltx-gen 2) l-0 (6 0))
  (traces
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send (exp (gen) e2)) (recv (exp (gen) e2)) (send key))
    ((recv (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
      (send (hash (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l))))
      (send (cat (exp (gen) (mul e2 l-0)) (exp (gen) (mul e2 l)))))
    ((recv (cat (exp (gen) e2) l)) (send (cat (exp (gen) e2) l)))
    ((send (enc "cert" (exp (gen) l) self (privk self))) (send l))
    ((recv (cat (exp (gen) e2) l-0)) (send (cat (exp (gen) e2) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send l-0)))
  (label 89)
  (parent 85)
  (unrealized)
  (shape)
  (maps)
  (origs))

(defskeleton iadh-umx
  (vars (key data) (self peer self-0 self-1 name) (e1 e2 l rndx)
    (lp expt) (l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self self-0) (peer self-1)
    (l l-0) (e e1) (lp l-1) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp))
  (deflistener (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
  (deflistener (cat (exp (gen) e1) l-0))
  (defstrand ltx-gen 2 (self self-0) (l l-0))
  (deflistener (cat (exp (gen) e2) l-1))
  (defstrand ltx-gen 2 (self self-1) (l l-1))
  (precedes ((0 2) (3 0)) ((1 2) (0 3)) ((1 2) (5 0)) ((3 1) (2 0))
    ((4 0) (0 0)) ((4 1) (3 0)) ((5 1) (2 0)) ((6 0) (0 1))
    ((6 1) (5 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)) (e1 (exp (gen) l-0))
    (e1 (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 self-1) (l-0 self-0))
    (foo
      ((hash (exp (gen) (mul e1 l-1)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk self-0) (privk self-1))
  (uniq-gen e1 e2 l-0 l-1)
  (operation generalization deleted (3 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (recv (enc "cert" (exp (gen) l-1) self-1 (privk self-1)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0)))))
    ((recv (cat (exp (gen) e1) l-0)) (send (cat (exp (gen) e1) l-0)))
    ((send (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send l-0))
    ((recv (cat (exp (gen) e2) l-1)) (send (cat (exp (gen) e2) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self-1 (privk self-1)))
      (send l-1)))
  (label 90)
  (parent 88)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (self peer self-0 self-1 name) (e1 e2 l rndx)
    (lp expt) (l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self self-0) (peer self-1)
    (l l-0) (e e1) (lp l-1) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp))
  (deflistener (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
  (defstrand ltx-gen 2 (self self-0) (l l-0))
  (deflistener (cat (exp (gen) e2) l-1))
  (defstrand ltx-gen 2 (self self-1) (l l-1))
  (precedes ((0 2) (2 0)) ((1 2) (0 3)) ((1 2) (4 0)) ((3 0) (0 0))
    ((3 1) (2 0)) ((4 1) (2 0)) ((5 0) (0 1)) ((5 1) (4 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)) (e1 (exp (gen) l-0))
    (e1 (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 self-1) (l-0 self-0))
    (foo
      ((hash (exp (gen) (mul e1 l-1)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk self-0) (privk self-1))
  (uniq-gen e1 e2 l-0 l-1)
  (operation generalization deleted (3 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (recv (enc "cert" (exp (gen) l-1) self-1 (privk self-1)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0)))))
    ((send (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send l-0))
    ((recv (cat (exp (gen) e2) l-1)) (send (cat (exp (gen) e2) l-1)))
    ((send (enc "cert" (exp (gen) l-1) self-1 (privk self-1)))
      (send l-1)))
  (label 91)
  (parent 90)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton iadh-umx
  (vars (key data) (self peer self-0 self-1 name) (e1 e2 l rndx)
    (lp expt) (l-0 l-1 rndx))
  (defstrand participant1 5 (key key) (self self-0) (peer self-1)
    (l l-0) (e e1) (lp l-1) (ep e2))
  (defstrand participant2 3 (self self) (peer peer) (l l) (e e2)
    (lp lp))
  (deflistener (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
  (defstrand ltx-gen 2 (self self-0) (l l-0))
  (defstrand ltx-gen 2 (self self-1) (l l-1))
  (precedes ((0 2) (2 0)) ((1 2) (0 3)) ((1 2) (2 0)) ((3 0) (0 0))
    ((3 1) (2 0)) ((4 0) (0 1)) ((4 1) (2 0)))
  (absent (e2 (exp (gen) l)) (e2 (exp (gen) lp)) (e1 (exp (gen) l-0))
    (e1 (exp (gen) l-1)))
  (fn-of ("principal-of" (l-1 self-1) (l-0 self-0))
    (foo
      ((hash (exp (gen) (mul e1 l-1)) (exp (gen) (mul e2 l-0))) key)))
  (neq (e2 (one)))
  (non-orig (privk self-0) (privk self-1))
  (uniq-gen e1 e2 l-0 l-1)
  (operation generalization deleted (4 0))
  (traces
    ((recv (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (recv (enc "cert" (exp (gen) l-1) self-1 (privk self-1)))
      (send (exp (gen) e1)) (recv (exp (gen) e2)) (send key))
    ((recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" (exp (gen) lp) peer (privk peer)))
      (send (exp (gen) e2)))
    ((recv (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0))))
      (send (hash (exp (gen) (mul e2 l-1)) (exp (gen) (mul e1 l-0)))))
    ((send (enc "cert" (exp (gen) l-0) self-0 (privk self-0)))
      (send l-0))
    ((send (enc "cert" (exp (gen) l-1) self-1 (privk self-1)))
      (send l-1)))
  (label 92)
  (parent 91)
  (unrealized)
  (shape)
  (maps
    ((0 1 2)
      ((e1 e1) (e2 e2) (l l-0) (lp l-1) (A self-0) (B self-1) (key key)
        (l-0 l) (lp-0 lp) (self self) (peer peer))))
  (origs))

(comment "Nothing left to do")