(herald "IADH: unified model (UM)" (bound 20) (limit 2000)
  (algebra diffie-hellman))
(comment "CPSA 3.6.2")
(comment "All input read from iadh_um.scm")
(comment "Strand count bounded at 20")

Trees: 0 1842.

Tree 0.

(defprotocol iadh-um diffie-hellman
  (defrole participant
    (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 lp)) (exp (gen) (mul e ep))) 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)))))

Item 0, Child: 1.

(defskeleton iadh-um
  (vars (key data) (A B C D name) (eA lA eB lB rndx)
    (lp ep lp-0 ep-0 expt))
  (defstrand participant 5 (key key) (self A) (peer C) (l lA) (e eA)
    (lp lp) (ep ep))
  (defstrand participant 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 lp-0)) (exp (gen) (mul eB ep-0))) key)
      ((hash (exp (gen) (mul lA lp)) (exp (gen) (mul eA 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)
  (comment "Implicit authentication")
  (label 0)
  (unrealized (0 0) (0 1) (1 0) (1 1))
  (origs)
  (preskeleton)
  (comment "Not a skeleton"))

Item 1, Parent: 0, Child: 2.

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

Item 2, Parent: 1, Children: 3 4.

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

Item 3, Parent: 2, Children: 5 6.

(defskeleton iadh-um
  (vars (key data) (A B C name) (lA eA eB rndx) (ep expt) (l rndx))
  (defstrand participant 5 (key key) (self A) (peer C) (l lA) (e eA)
    (lp (mul (rec lA) l l)) (ep (mul (rec eA) eB ep)))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep ep))
  (defstrand ltx-gen 1 (self B) (l l))
  (precedes ((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 (rec lA) l l))))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eB ep))) key)))
  (neq (ep (one)) (eA eB) ((mul (rec eA) eB ep) (one)))
  (non-orig (privk A) (privk B) (privk C) lA l)
  (uniq-gen eA eB l)
  (operation encryption-test (displaced 3 2 ltx-gen 1)
    (enc "cert" (exp (gen) l-0) D (privk D)) (1 1))
  (label 3)
  (parent 2)
  (unrealized (0 0) (0 1) (0 3))
  (comment "2 in cohort - 2 not yet seen"))

Item 4, Parent: 2, Children: 7 8 9.

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

Item 5, Parent: 3, Child: 10.

(defskeleton iadh-um
  (vars (key data) (B C name) (eA eB rndx) (ep expt) (l rndx))
  (defstrand participant 5 (key key) (self B) (peer C) (l l) (e eA)
    (lp l) (ep (mul (rec eA) eB ep)))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep ep))
  (defstrand ltx-gen 1 (self B) (l l))
  (precedes ((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 l l)) (exp (gen) (mul eB ep))) key)))
  (neq (ep (one)) (eA eB) ((mul (rec eA) eB ep) (one)))
  (non-orig (privk B) (privk C) l)
  (uniq-gen eA eB l)
  (operation encryption-test (displaced 3 2 ltx-gen 1)
    (enc "cert" (exp (gen) l-0) A (privk A)) (0 0))
  (label 5)
  (parent 3)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 6, Parent: 3.

(defskeleton iadh-um
  (vars (key data) (A B C name) (eA eB rndx) (ep expt) (l l-0 rndx))
  (defstrand participant 5 (key key) (self A) (peer C) (l l-0) (e eA)
    (lp (mul l l (rec l-0))) (ep (mul (rec eA) eB ep)))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep ep))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self A) (l l-0))
  (precedes ((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 l l (rec l-0)))))
  (fn-of ("principal-of" (l-0 A) (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eB ep))) key)))
  (neq (ep (one)) (eA eB) ((mul (rec eA) eB ep) (one)))
  (non-orig (privk A) (privk B) (privk C) l l-0)
  (uniq-gen eA eB l l-0)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-0) A (privk A)) (0 0))
  (label 6)
  (parent 3)
  (unrealized (0 1) (0 3))
  (comment "empty cohort"))

Item 7, Parent: 4, Child: 11.

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

Item 8, Parent: 4, Child: 12.

(defskeleton iadh-um
  (vars (key data) (B C D name) (eA eB rndx) (ep expt) (l l-0 rndx))
  (defstrand participant 5 (key key) (self D) (peer C) (l l-0) (e eA)
    (lp l) (ep (mul (rec eA) eB ep)))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep ep))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (precedes ((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) l)))
  (fn-of ("principal-of" (l-0 D) (l B))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eB ep))) key)))
  (neq (ep (one)) (eA eB) ((mul (rec eA) eB ep) (one)))
  (non-orig (privk B) (privk C) (privk D) l l-0)
  (uniq-gen eA eB l l-0)
  (operation encryption-test (displaced 4 3 ltx-gen 1)
    (enc "cert" (exp (gen) l-1) A (privk A)) (0 0))
  (label 8)
  (parent 4)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 9, Parent: 4.

(defskeleton iadh-um
  (vars (key data) (A B C D name) (eA eB rndx) (ep expt)
    (l l-0 l-1 rndx))
  (defstrand participant 5 (key key) (self A) (peer C) (l l-1) (e eA)
    (lp (mul l l-0 (rec l-1))) (ep (mul (rec eA) eB ep)))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep ep))
  (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 ((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)) (eB (exp (gen) l-0)) (eA (exp (gen) l-1))
    (eA (exp (gen) (mul l l-0 (rec l-1)))))
  (fn-of ("principal-of" (l-1 A) (l-0 D) (l B))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eB ep))) key)))
  (neq (ep (one)) (eA eB) ((mul (rec eA) eB ep) (one)))
  (non-orig (privk A) (privk B) (privk C) (privk D) l l-1)
  (uniq-gen eA eB l l-0 l-1)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-1) A (privk A)) (0 0))
  (label 9)
  (parent 4)
  (unrealized (0 1) (0 3))
  (comment "empty cohort"))

Item 10, Parent: 5, Children: 13 14 15 16 17 18.

(defskeleton iadh-um
  (vars (key data) (B name) (eA eB rndx) (ep expt) (l rndx))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep (mul (rec eA) eB ep)))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep ep))
  (defstrand ltx-gen 1 (self B) (l l))
  (precedes ((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 l l)) (exp (gen) (mul eB ep))) key)))
  (neq (ep (one)) (eA eB) ((mul (rec eA) eB ep) (one)))
  (non-orig (privk B) l)
  (uniq-gen eA eB l)
  (operation encryption-test (displaced 3 2 ltx-gen 1)
    (enc "cert" (exp (gen) l) C (privk C)) (0 1))
  (label 10)
  (parent 5)
  (unrealized (0 3))
  (comment "6 in cohort - 6 not yet seen"))

Item 11, Parent: 7, Children: 19 20 21 22 23 24 25.

(defskeleton iadh-um
  (vars (key data) (B D name) (eA eB rndx) (ep expt) (l l-0 rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep (mul (rec eA) eB ep)))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep ep))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (precedes ((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 l l-0)) (exp (gen) (mul eB ep))) key)))
  (neq (ep (one)) (eA eB) ((mul (rec eA) eB ep) (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen eA eB l l-0)
  (operation encryption-test (displaced 4 3 ltx-gen 1)
    (enc "cert" (exp (gen) l-0) C (privk C)) (0 1))
  (label 11)
  (parent 7)
  (unrealized (0 3))
  (comment "7 in cohort - 7 not yet seen"))

Item 12, Parent: 8, Children: 26 27 28 29 30 31 32.

(defskeleton iadh-um
  (vars (key data) (B D name) (eA eB rndx) (ep expt) (l l-0 rndx))
  (defstrand participant 5 (key key) (self D) (peer B) (l l) (e eA)
    (lp l-0) (ep (mul (rec eA) eB ep)))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep ep))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (precedes ((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 l l-0)) (exp (gen) (mul eB ep))) key)))
  (neq (ep (one)) (eA eB) ((mul (rec eA) eB ep) (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen eA eB l l-0)
  (operation encryption-test (displaced 4 2 ltx-gen 1)
    (enc "cert" (exp (gen) l-0) C (privk C)) (0 1))
  (label 12)
  (parent 8)
  (unrealized (0 3))
  (comment "7 in cohort - 7 not yet seen"))

Item 13, Parent: 10, Child: 33.

(defskeleton iadh-um
  (vars (key data) (B name) (eB l e rndx))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e e)
    (lp l) (ep e))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul (rec eB) e e)))
  (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 (e (exp (gen) l)) (eB (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul e e))) key)))
  (neq ((mul (rec eB) e e) (one)) (e eB) (e (one)))
  (non-orig (privk B) l)
  (uniq-gen eB l e)
  (operation nonce-test (displaced 3 0 participant 3) (exp (gen) e-0)
    (0 3))
  (label 13)
  (parent 10)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 14, Parent: 10.

(defskeleton iadh-um
  (vars (key data) (B name) (eA l e rndx))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep e))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e e)
    (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 (e (exp (gen) l)) (eA (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eA e))) key)))
  (neq (eA (one)) (eA e) (e (one)))
  (non-orig (privk B) l)
  (uniq-gen eA l e)
  (operation nonce-test (displaced 3 1 participant 3) (exp (gen) e-0)
    (0 3))
  (label 14)
  (parent 10)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((key key) (A B) (B B) (C B) (D B) (lA l) (lB l) (lp l) (eA eA)
        (eB e) (ep eA))))
  (origs))

Item 15, Parent: 10, Child: 34.

(defskeleton iadh-um
  (vars (key data) (B self peer name) (l l-0 rndx) (lp expt)
    (eA eB e rndx))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep e))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec eB) e)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand participant 3 (self self) (peer peer) (l l-0) (e e)
    (lp lp))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 2) (0 3)) ((3 2) (1 3)))
  (absent (e (exp (gen) l-0)) (e (exp (gen) lp)) (eB (exp (gen) l))
    (eA (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eA e))) key)))
  (neq ((mul eA (rec eB) e) (one)) (eA eB) (e (one)))
  (non-orig (privk B) l)
  (uniq-gen l eA eB e)
  (operation nonce-test (added-strand participant 3) (exp (gen) e)
    (0 3))
  (label 15)
  (parent 10)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 16, Parent: 10, Child: 35.

(defskeleton iadh-um
  (vars (key data) (B name) (eA eB l rndx))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep l))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec eB) l)))
  (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 l l)) (exp (gen) (mul eA l))) key)))
  (neq ((mul eA (rec eB) l) (one)) (eA eB) (l (one)))
  (non-orig (privk B) l)
  (uniq-gen eA eB l)
  (operation nonce-test (displaced 3 2 ltx-gen 1) (exp (gen) l-0) (0 3))
  (label 16)
  (parent 10)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 17, Parent: 10, Child: 36.

(defskeleton iadh-um
  (vars (key data) (B self name) (l eA eB l-0 rndx))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep l-0))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec eB) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self self) (l l-0))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (0 3)) ((3 0) (1 3)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)))
  (fn-of ("principal-of" (l-0 self) (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eA l-0))) key)))
  (neq ((mul eA (rec eB) l-0) (one)) (eA eB) (l-0 (one)))
  (non-orig (privk B) l)
  (uniq-gen l eA eB l-0)
  (operation nonce-test (added-strand ltx-gen 1) (exp (gen) l-0) (0 3))
  (label 17)
  (parent 10)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 18, Parent: 10, Children: 37 38 39 40 41 42.

(defskeleton iadh-um
  (vars (key data) (B name) (eA eB rndx) (ep expt) (l rndx) (w expt))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep (mul (rec eA) eB ep)))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep ep))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) (mul (rec eA) eB ep (rec w))) w))
  (precedes ((0 2) (3 0)) ((1 2) (3 0)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 1) (0 3)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eB ep))) key)))
  (neq (ep (one)) (eA eB) ((mul (rec eA) eB ep) (one)))
  (non-orig (privk B) l)
  (uniq-gen eA eB l)
  (precur (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec eA) eB ep (rec w))) w))
    (exp (gen) (mul (rec eA) eB ep)) (0 3))
  (label 18)
  (parent 10)
  (unrealized (3 0))
  (comment "6 in cohort - 6 not yet seen"))

Item 19, Parent: 11, Child: 43.

(defskeleton iadh-um
  (vars (key data) (B D name) (eB l l-0 e rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e e)
    (lp l-0) (ep e))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul (rec eB) e e)))
  (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 (e (exp (gen) l)) (e (exp (gen) l-0)) (eB (exp (gen) l))
    (eB (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 D) (l B))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul e e))) key)))
  (neq ((mul (rec eB) e e) (one)) (e eB) (e (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen eB l l-0 e)
  (operation nonce-test (displaced 4 0 participant 3) (exp (gen) e-0)
    (0 3))
  (label 19)
  (parent 11)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 20, Parent: 11.

(defskeleton iadh-um
  (vars (key data) (B D name) (eA l l-0 e rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep e))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e e)
    (lp l-0) (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 0)) ((2 0) (1 0))
    ((3 0) (0 1)) ((3 0) (1 1)))
  (absent (e (exp (gen) l)) (e (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 l l-0)) (exp (gen) (mul eA e))) key)))
  (neq (eA (one)) (eA e) (e (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen eA l l-0 e)
  (operation nonce-test (displaced 4 1 participant 3) (exp (gen) e-0)
    (0 3))
  (label 20)
  (parent 11)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((key key) (A B) (B B) (C D) (D D) (lA l) (lB l) (lp l-0) (eA eA)
        (eB e) (ep eA))))
  (origs))

Item 21, Parent: 11, Child: 44.

(defskeleton iadh-um
  (vars (key data) (B D self peer name) (l l-0 l-1 rndx) (lp expt)
    (eA eB e rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep e))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec eB) e)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (defstrand participant 3 (self self) (peer peer) (l l-1) (e e)
    (lp lp))
  (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)) ((4 2) (0 3)) ((4 2) (1 3)))
  (absent (e (exp (gen) l-1)) (e (exp (gen) lp)) (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 l l-0)) (exp (gen) (mul eA e))) key)))
  (neq ((mul eA (rec eB) e) (one)) (eA eB) (e (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen l l-0 eA eB e)
  (operation nonce-test (added-strand participant 3) (exp (gen) e)
    (0 3))
  (label 21)
  (parent 11)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 22, Parent: 11, Child: 45.

(defskeleton iadh-um
  (vars (key data) (B D name) (l eA eB l-0 rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eA)
    (lp l) (ep l-0))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec eB) l-0)))
  (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) (0 1)) ((3 0) (1 1)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l)))
  (fn-of ("principal-of" (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eA l-0))) key)))
  (neq ((mul eA (rec eB) l-0) (one)) (eA eB) (l-0 (one)))
  (non-orig (privk B) (privk D) l-0)
  (uniq-gen l eA eB l-0)
  (operation nonce-test (displaced 4 2 ltx-gen 1) (exp (gen) l-1) (0 3))
  (label 22)
  (parent 11)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 23, Parent: 11, Child: 46.

(defskeleton iadh-um
  (vars (key data) (B D name) (l eA eB l-0 rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep l-0))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec eB) 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 l l-0)) (exp (gen) (mul eA l-0))) key)))
  (neq ((mul eA (rec eB) l-0) (one)) (eA eB) (l-0 (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen l eA eB l-0)
  (operation nonce-test (displaced 4 3 ltx-gen 1) (exp (gen) l-1) (0 3))
  (label 23)
  (parent 11)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 24, Parent: 11, Child: 47.

(defskeleton iadh-um
  (vars (key data) (B D self name) (l l-0 eA eB l-1 rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep l-1))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec eB) l-1)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (defstrand ltx-gen 1 (self self) (l l-1))
  (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)) ((4 0) (0 3)) ((4 0) (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-1 self) (l-0 D) (l B))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eA l-1))) key)))
  (neq ((mul eA (rec eB) l-1) (one)) (eA eB) (l-1 (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen l l-0 eA eB l-1)
  (operation nonce-test (added-strand ltx-gen 1) (exp (gen) l-1) (0 3))
  (label 24)
  (parent 11)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 25, Parent: 11, Children: 48 49 50 51 52 53 54.

(defskeleton iadh-um
  (vars (key data) (B D name) (eA eB rndx) (ep expt) (l l-0 rndx)
    (w expt))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep (mul (rec eA) eB ep)))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep ep))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (exp (gen) (mul (rec eA) eB ep (rec w))) w))
  (precedes ((0 2) (4 0)) ((1 2) (4 0)) ((2 0) (0 0)) ((2 0) (1 0))
    ((3 0) (0 1)) ((3 0) (1 1)) ((4 1) (0 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 l l-0)) (exp (gen) (mul eB ep))) key)))
  (neq (ep (one)) (eA eB) ((mul (rec eA) eB ep) (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen eA eB l l-0)
  (precur (4 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec eA) eB ep (rec w))) w))
    (exp (gen) (mul (rec eA) eB ep)) (0 3))
  (label 25)
  (parent 11)
  (unrealized (4 0))
  (comment "7 in cohort - 7 not yet seen"))

Item 26, Parent: 12, Child: 55.

(defskeleton iadh-um
  (vars (key data) (B D name) (eB l l-0 e rndx))
  (defstrand participant 5 (key key) (self D) (peer B) (l l) (e e)
    (lp l-0) (ep e))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul (rec eB) e e)))
  (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 (e (exp (gen) l)) (e (exp (gen) l-0)) (eB (exp (gen) l-0))
    (eB (exp (gen) l)))
  (fn-of ("principal-of" (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul e e))) key)))
  (neq ((mul (rec eB) e e) (one)) (e eB) (e (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen eB l l-0 e)
  (operation nonce-test (displaced 4 0 participant 3) (exp (gen) e-0)
    (0 3))
  (label 26)
  (parent 12)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 27, Parent: 12.

(defskeleton iadh-um
  (vars (key data) (B D name) (eA l l-0 e rndx))
  (defstrand participant 5 (key key) (self D) (peer B) (l l-0) (e eA)
    (lp l) (ep e))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e e)
    (lp l-0) (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 (e (exp (gen) l)) (e (exp (gen) l-0)) (eA (exp (gen) l-0))
    (eA (exp (gen) l)))
  (fn-of ("principal-of" (l B) (l-0 D))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eA e))) key)))
  (neq (eA (one)) (eA e) (e (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen eA l l-0 e)
  (operation nonce-test (displaced 4 1 participant 3) (exp (gen) e-0)
    (0 3))
  (label 27)
  (parent 12)
  (unrealized)
  (shape)
  (maps
    ((0 1)
      ((key key) (A D) (B B) (C B) (D D) (lA l-0) (lB l) (lp l-0)
        (eA eA) (eB e) (ep eA))))
  (origs))

Item 28, Parent: 12, Child: 56.

(defskeleton iadh-um
  (vars (key data) (B D self peer name) (l l-0 l-1 rndx) (lp expt)
    (eA eB e rndx))
  (defstrand participant 5 (key key) (self D) (peer B) (l l) (e eA)
    (lp l-0) (ep e))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec eB) e)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand participant 3 (self self) (peer peer) (l l-1) (e e)
    (lp lp))
  (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 2) (0 3)) ((4 2) (1 3)))
  (absent (e (exp (gen) l-1)) (e (exp (gen) lp)) (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 l l-0)) (exp (gen) (mul eA e))) key)))
  (neq ((mul eA (rec eB) e) (one)) (eA eB) (e (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen l l-0 eA eB e)
  (operation nonce-test (added-strand participant 3) (exp (gen) e)
    (0 3))
  (label 28)
  (parent 12)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 29, Parent: 12, Child: 57.

(defskeleton iadh-um
  (vars (key data) (B D name) (l eA eB l-0 rndx))
  (defstrand participant 5 (key key) (self D) (peer B) (l l) (e eA)
    (lp l-0) (ep l-0))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec eB) l-0)))
  (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 l l-0)) (exp (gen) (mul eA l-0))) key)))
  (neq ((mul eA (rec eB) l-0) (one)) (eA eB) (l-0 (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen l eA eB l-0)
  (operation nonce-test (displaced 4 2 ltx-gen 1) (exp (gen) l-1) (0 3))
  (label 29)
  (parent 12)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 30, Parent: 12, Child: 58.

(defskeleton iadh-um
  (vars (key data) (B D name) (l eA eB l-0 rndx))
  (defstrand participant 5 (key key) (self D) (peer B) (l l-0) (e eA)
    (lp l) (ep l-0))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec eB) 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))
    (eA (exp (gen) l)))
  (fn-of ("principal-of" (l-0 D) (l B))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eA l-0))) key)))
  (neq ((mul eA (rec eB) l-0) (one)) (eA eB) (l-0 (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen l eA eB l-0)
  (operation nonce-test (displaced 4 3 ltx-gen 1) (exp (gen) l-1) (0 3))
  (label 30)
  (parent 12)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 31, Parent: 12, Child: 59.

(defskeleton iadh-um
  (vars (key data) (B D self name) (l l-0 eA eB l-1 rndx))
  (defstrand participant 5 (key key) (self D) (peer B) (l l) (e eA)
    (lp l-0) (ep l-1))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec eB) l-1)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand ltx-gen 1 (self self) (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 3)) ((4 0) (1 3)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l))
    (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-1 self) (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eA l-1))) key)))
  (neq ((mul eA (rec eB) l-1) (one)) (eA eB) (l-1 (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen l l-0 eA eB l-1)
  (operation nonce-test (added-strand ltx-gen 1) (exp (gen) l-1) (0 3))
  (label 31)
  (parent 12)
  (unrealized (1 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 32, Parent: 12, Children: 60 61 62 63 64 65 66.

(defskeleton iadh-um
  (vars (key data) (B D name) (eA eB rndx) (ep expt) (l l-0 rndx)
    (w expt))
  (defstrand participant 5 (key key) (self D) (peer B) (l l) (e eA)
    (lp l-0) (ep (mul (rec eA) eB ep)))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep ep))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (deflistener (cat (exp (gen) (mul (rec eA) eB ep (rec w))) w))
  (precedes ((0 2) (4 0)) ((1 2) (4 0)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 0) (0 0)) ((3 0) (1 1)) ((4 1) (0 3)))
  (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 l l-0)) (exp (gen) (mul eB ep))) key)))
  (neq (ep (one)) (eA eB) ((mul (rec eA) eB ep) (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen eA eB l l-0)
  (precur (4 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec eA) eB ep (rec w))) w))
    (exp (gen) (mul (rec eA) eB ep)) (0 3))
  (label 32)
  (parent 12)
  (unrealized (4 0))
  (comment "7 in cohort - 7 not yet seen"))

Item 33, Parent: 13, Children: 67 68 69 70 71 72.

(defskeleton iadh-um
  (vars (key data) (B name) (eB l e rndx) (w expt))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e e)
    (lp l) (ep e))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul (rec eB) e e)))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) (mul (rec eB) e e (rec w))) w))
  (precedes ((0 2) (3 0)) ((1 2) (0 3)) ((1 2) (3 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 1) (1 3)))
  (absent (e (exp (gen) l)) (eB (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul e e))) key)))
  (neq ((mul (rec eB) e e) (one)) (e eB) (e (one)))
  (non-orig (privk B) l)
  (uniq-gen eB l e)
  (precur (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec eB) e e (rec w))) w))
    (exp (gen) (mul (rec eB) e e)) (1 3))
  (label 33)
  (parent 13)
  (unrealized (3 0))
  (comment "6 in cohort - 6 not yet seen"))

Item 34, Parent: 15, Children: 73 74 75 76 77 78 79.

(defskeleton iadh-um
  (vars (key data) (B self peer name) (l l-0 rndx) (lp expt)
    (eA eB e rndx) (w expt))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep e))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec eB) e)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand participant 3 (self self) (peer peer) (l l-0) (e e)
    (lp lp))
  (deflistener (cat (exp (gen) (mul eA (rec eB) e (rec w))) w))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (4 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 2) (0 3)) ((3 2) (4 0)) ((4 1) (1 3)))
  (absent (e (exp (gen) l-0)) (e (exp (gen) lp)) (eB (exp (gen) l))
    (eA (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eA e))) key)))
  (neq ((mul eA (rec eB) e) (one)) (eA eB) (e (one)))
  (non-orig (privk B) l)
  (uniq-gen l eA eB e)
  (precur (4 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec eB) e (rec w))) w))
    (exp (gen) (mul eA (rec eB) e)) (1 3))
  (label 34)
  (parent 15)
  (unrealized (4 0))
  (comment "7 in cohort - 7 not yet seen"))

Item 35, Parent: 16, Children: 80 81 82 83 84 85.

(defskeleton iadh-um
  (vars (key data) (B name) (eA eB l rndx) (w expt))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep l))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec eB) l)))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec eB) l (rec w))) w))
  (precedes ((0 2) (3 0)) ((1 2) (0 3)) ((1 2) (3 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 1) (1 3)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eA l))) key)))
  (neq ((mul eA (rec eB) l) (one)) (eA eB) (l (one)))
  (non-orig (privk B) l)
  (uniq-gen eA eB l)
  (precur (3 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec eB) l (rec w))) w))
    (exp (gen) (mul eA (rec eB) l)) (1 3))
  (label 35)
  (parent 16)
  (unrealized (3 0))
  (comment "6 in cohort - 6 not yet seen"))

Item 36, Parent: 17, Children: 86 87 88 89 90 91 92.

(defskeleton iadh-um
  (vars (key data) (B self name) (l eA eB l-0 rndx) (w expt))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep l-0))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec eB) l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self self) (l l-0))
  (deflistener (cat (exp (gen) (mul eA (rec eB) l-0 (rec w))) w))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (4 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 0) (0 3)) ((3 0) (4 0)) ((4 1) (1 3)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)))
  (fn-of ("principal-of" (l-0 self) (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eA l-0))) key)))
  (neq ((mul eA (rec eB) l-0) (one)) (eA eB) (l-0 (one)))
  (non-orig (privk B) l)
  (uniq-gen l eA eB l-0)
  (precur (4 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec eB) l-0 (rec w))) w))
    (exp (gen) (mul eA (rec eB) l-0)) (1 3))
  (label 36)
  (parent 17)
  (unrealized (4 0))
  (comment "7 in cohort - 7 not yet seen"))

Item 37, Parent: 18, Children: 93 94 95 96 97 98.

(defskeleton iadh-um
  (vars (key data) (B name) (l eA eB rndx) (w expt))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep w))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec eB) w)))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (gen) w))
  (precedes ((0 2) (1 3)) ((0 2) (3 0)) ((1 2) (3 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 1) (0 3)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eA w))) key)))
  (neq ((mul eA (rec eB) w) (one)) (eA eB) (w (one)))
  (non-orig (privk B) l)
  (uniq-gen l eA eB)
  (precur (3 0))
  (operation nonce-test
    (contracted (eA-0 eA) (eB-0 eB) (ep (mul eA (rec eB) w)) (w-0 w))
    (gen) (3 0))
  (label 37)
  (parent 18)
  (unrealized (1 3))
  (comment "6 in cohort - 6 not yet seen"))

Item 38, Parent: 18, Children: 99 100 101 102 103 104.

(defskeleton iadh-um
  (vars (key data) (B name) (eB rndx) (w expt) (l e rndx))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e e)
    (lp l) (ep (mul w e)))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul (rec eB) w e e)))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) e) w))
  (precedes ((0 2) (1 3)) ((0 2) (3 0)) ((1 2) (3 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 1) (0 3)))
  (absent (e (exp (gen) l)) (eB (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul w e e))) key)))
  (neq ((mul (rec eB) w e e) (one)) (e eB) ((mul w e) (one)))
  (non-orig (privk B) l)
  (precur (3 0))
  (uniq-gen eB l e)
  (operation nonce-test (displaced 4 0 participant 3) (exp (gen) e-0)
    (3 0))
  (label 38)
  (parent 18)
  (unrealized (1 3))
  (comment "6 in cohort - 6 not yet seen"))

Item 39, Parent: 18, Child: 105.

(defskeleton iadh-um
  (vars (key data) (B name) (eA rndx) (w expt) (l e rndx))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep (mul w e)))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e e)
    (lp l) (ep (mul eA w)))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) e) w))
  (precedes ((0 2) (1 3)) ((0 2) (3 0)) ((1 2) (3 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 1) (0 3)))
  (absent (e (exp (gen) l)) (eA (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eA w e))) key)))
  (neq ((mul eA w) (one)) (eA e) ((mul w e) (one)))
  (non-orig (privk B) l)
  (precur (3 0))
  (uniq-gen eA l e)
  (operation nonce-test (displaced 4 1 participant 3) (exp (gen) e-0)
    (3 0))
  (label 39)
  (parent 18)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

Item 40, Parent: 18, Children: 106 107 108 109 110 111 112.

(defskeleton iadh-um
  (vars (key data) (B self peer name) (l l-0 rndx) (lp expt)
    (eA eB rndx) (w expt) (e rndx))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep (mul w e)))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec eB) w e)))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) e) w))
  (defstrand participant 3 (self self) (peer peer) (l l-0) (e e)
    (lp lp))
  (precedes ((0 2) (1 3)) ((0 2) (3 0)) ((1 2) (3 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 1) (0 3)) ((4 2) (1 3)) ((4 2) (3 0)))
  (absent (e (exp (gen) l-0)) (e (exp (gen) lp)) (eB (exp (gen) l))
    (eA (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eA w e))) key)))
  (neq ((mul eA (rec eB) w e) (one)) (eA eB) ((mul w e) (one)))
  (non-orig (privk B) l)
  (precur (3 0))
  (uniq-gen l eA eB e)
  (operation nonce-test (added-strand participant 3) (exp (gen) e)
    (3 0))
  (label 40)
  (parent 18)
  (unrealized (1 3))
  (comment "7 in cohort - 7 not yet seen"))

Item 41, Parent: 18, Children: 113 114 115 116 117 118.

(defskeleton iadh-um
  (vars (key data) (B name) (eA eB rndx) (w expt) (l rndx))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep (mul w l)))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec eB) w l)))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) l) w))
  (precedes ((0 2) (1 3)) ((0 2) (3 0)) ((1 2) (3 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 1) (0 3)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eA w l))) key)))
  (neq ((mul eA (rec eB) w l) (one)) (eA eB) ((mul w l) (one)))
  (non-orig (privk B) l)
  (precur (3 0))
  (uniq-gen eA eB l)
  (operation nonce-test (displaced 4 2 ltx-gen 1) (exp (gen) l-0) (3 0))
  (label 41)
  (parent 18)
  (unrealized (1 3))
  (comment "6 in cohort - 6 not yet seen"))

Item 42, Parent: 18, Children: 119 120 121 122 123 124 125.

(defskeleton iadh-um
  (vars (key data) (B self name) (l eA eB rndx) (w expt) (l-0 rndx))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eA)
    (lp l) (ep (mul w l-0)))
  (defstrand participant 5 (key key) (self B) (peer B) (l l) (e eB)
    (lp l) (ep (mul eA (rec eB) w l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) l-0) w))
  (defstrand ltx-gen 1 (self self) (l l-0))
  (precedes ((0 2) (1 3)) ((0 2) (3 0)) ((1 2) (3 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 1) (0 3)) ((4 0) (1 3)) ((4 0) (3 0)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l)))
  (fn-of ("principal-of" (l-0 self) (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eA w l-0))) key)))
  (neq ((mul eA (rec eB) w l-0) (one)) (eA eB) ((mul w l-0) (one)))
  (non-orig (privk B) l)
  (precur (3 0))
  (uniq-gen l eA eB l-0)
  (operation nonce-test (added-strand ltx-gen 1) (exp (gen) l-0) (3 0))
  (label 42)
  (parent 18)
  (unrealized (1 3))
  (comment "7 in cohort - 7 not yet seen"))

Item 43, Parent: 19, Children: 126 127 128 129 130 131 132.

(defskeleton iadh-um
  (vars (key data) (B D name) (eB l l-0 e rndx) (w expt))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e e)
    (lp l-0) (ep e))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul (rec eB) e e)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (exp (gen) (mul (rec eB) e e (rec w))) w))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (4 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 0) (0 1)) ((3 0) (1 1)) ((4 1) (1 3)))
  (absent (e (exp (gen) l)) (e (exp (gen) l-0)) (eB (exp (gen) l))
    (eB (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 D) (l B))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul e e))) key)))
  (neq ((mul (rec eB) e e) (one)) (e eB) (e (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen eB l l-0 e)
  (precur (4 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec eB) e e (rec w))) w))
    (exp (gen) (mul (rec eB) e e)) (1 3))
  (label 43)
  (parent 19)
  (unrealized (4 0))
  (comment "7 in cohort - 7 not yet seen"))

Item 44, Parent: 21, Children: 133 134 135 136 137 138 139 140.

(defskeleton iadh-um
  (vars (key data) (B D self peer name) (l l-0 l-1 rndx) (lp expt)
    (eA eB e rndx) (w expt))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep e))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec eB) e)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (defstrand participant 3 (self self) (peer peer) (l l-1) (e e)
    (lp lp))
  (deflistener (cat (exp (gen) (mul eA (rec eB) e (rec w))) w))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((1 2) (5 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 0) (0 1)) ((3 0) (1 1)) ((4 2) (0 3))
    ((4 2) (5 0)) ((5 1) (1 3)))
  (absent (e (exp (gen) l-1)) (e (exp (gen) lp)) (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 l l-0)) (exp (gen) (mul eA e))) key)))
  (neq ((mul eA (rec eB) e) (one)) (eA eB) (e (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen l l-0 eA eB e)
  (precur (5 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec eB) e (rec w))) w))
    (exp (gen) (mul eA (rec eB) e)) (1 3))
  (label 44)
  (parent 21)
  (unrealized (5 0))
  (comment "8 in cohort - 8 not yet seen"))

Item 45, Parent: 22, Children: 141 142 143 144 145 146 147.

(defskeleton iadh-um
  (vars (key data) (B D name) (l eA eB l-0 rndx) (w expt))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eA)
    (lp l) (ep l-0))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec eB) l-0)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (deflistener (cat (exp (gen) (mul eA (rec eB) l-0 (rec w))) w))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (4 0)) ((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-0)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l)))
  (fn-of ("principal-of" (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eA l-0))) key)))
  (neq ((mul eA (rec eB) l-0) (one)) (eA eB) (l-0 (one)))
  (non-orig (privk B) (privk D) l-0)
  (uniq-gen l eA eB l-0)
  (precur (4 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec eB) l-0 (rec w))) w))
    (exp (gen) (mul eA (rec eB) l-0)) (1 3))
  (label 45)
  (parent 22)
  (unrealized (4 0))
  (comment "7 in cohort - 7 not yet seen"))

Item 46, Parent: 23, Children: 148 149 150 151 152 153 154.

(defskeleton iadh-um
  (vars (key data) (B D name) (l eA eB l-0 rndx) (w expt))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep l-0))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec eB) 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 eB) l-0 (rec w))) w))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (4 0)) ((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 l l-0)) (exp (gen) (mul eA l-0))) key)))
  (neq ((mul eA (rec eB) l-0) (one)) (eA eB) (l-0 (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen l eA eB l-0)
  (precur (4 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec eB) l-0 (rec w))) w))
    (exp (gen) (mul eA (rec eB) l-0)) (1 3))
  (label 46)
  (parent 23)
  (unrealized (4 0))
  (comment "7 in cohort - 7 not yet seen"))

Item 47, Parent: 24, Children: 155 156 157 158 159 160 161 162.

(defskeleton iadh-um
  (vars (key data) (B D self name) (l l-0 eA eB l-1 rndx) (w expt))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep l-1))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec eB) l-1)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (defstrand ltx-gen 1 (self self) (l l-1))
  (deflistener (cat (exp (gen) (mul eA (rec eB) l-1 (rec w))) w))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((1 2) (5 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 0) (0 1)) ((3 0) (1 1)) ((4 0) (0 3))
    ((4 0) (5 0)) ((5 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-1 self) (l-0 D) (l B))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eA l-1))) key)))
  (neq ((mul eA (rec eB) l-1) (one)) (eA eB) (l-1 (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen l l-0 eA eB l-1)
  (precur (5 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec eB) l-1 (rec w))) w))
    (exp (gen) (mul eA (rec eB) l-1)) (1 3))
  (label 47)
  (parent 24)
  (unrealized (5 0))
  (comment "8 in cohort - 8 not yet seen"))

Item 48, Parent: 25, Children: 163 164 165 166 167 168 169.

(defskeleton iadh-um
  (vars (key data) (B D name) (l l-0 eA eB rndx) (w expt))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep w))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec eB) w)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (gen) w))
  (precedes ((0 2) (1 3)) ((0 2) (4 0)) ((1 2) (4 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 0) (0 1)) ((3 0) (1 1)) ((4 1) (0 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 l l-0)) (exp (gen) (mul eA w))) key)))
  (neq ((mul eA (rec eB) w) (one)) (eA eB) (w (one)))
  (non-orig (privk B) (privk D) l)
  (uniq-gen l l-0 eA eB)
  (precur (4 0))
  (operation nonce-test
    (contracted (eA-0 eA) (eB-0 eB) (ep (mul eA (rec eB) w)) (w-0 w))
    (gen) (4 0))
  (label 48)
  (parent 25)
  (unrealized (1 3))
  (comment "7 in cohort - 7 not yet seen"))

Item 49, Parent: 25, Children: 170 171 172 173 174 175 176.

(defskeleton iadh-um
  (vars (key data) (B D name) (eB rndx) (w expt) (l l-0 e rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e e)
    (lp l-0) (ep (mul w e)))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul (rec eB) w e e)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (exp (gen) e) w))
  (precedes ((0 2) (1 3)) ((0 2) (4 0)) ((1 2) (4 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 0) (0 1)) ((3 0) (1 1)) ((4 1) (0 3)))
  (absent (e (exp (gen) l)) (e (exp (gen) l-0)) (eB (exp (gen) l))
    (eB (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 D) (l B))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul w e e))) key)))
  (neq ((mul (rec eB) w e e) (one)) (e eB) ((mul w e) (one)))
  (non-orig (privk B) (privk D) l)
  (precur (4 0))
  (uniq-gen eB l l-0 e)
  (operation nonce-test (displaced 5 0 participant 3) (exp (gen) e-0)
    (4 0))
  (label 49)
  (parent 25)
  (unrealized (1 3))
  (comment "7 in cohort - 7 not yet seen"))

Item 50, Parent: 25, Child: 177.

(defskeleton iadh-um
  (vars (key data) (B D name) (eA rndx) (w expt) (l l-0 e rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep (mul w e)))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e e)
    (lp l-0) (ep (mul eA w)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (exp (gen) e) w))
  (precedes ((0 2) (1 3)) ((0 2) (4 0)) ((1 2) (4 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 0) (0 1)) ((3 0) (1 1)) ((4 1) (0 3)))
  (absent (e (exp (gen) l)) (e (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 l l-0)) (exp (gen) (mul eA w e))) key)))
  (neq ((mul eA w) (one)) (eA e) ((mul w e) (one)))
  (non-orig (privk B) (privk D) l)
  (precur (4 0))
  (uniq-gen eA l l-0 e)
  (operation nonce-test (displaced 5 1 participant 3) (exp (gen) e-0)
    (4 0))
  (label 50)
  (parent 25)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

Item 51, Parent: 25, Children: 178 179 180 181 182 183 184 185.

(defskeleton iadh-um
  (vars (key data) (B D self peer name) (l l-0 l-1 rndx) (lp expt)
    (eA eB rndx) (w expt) (e rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep (mul w e)))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec eB) w e)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (exp (gen) e) w))
  (defstrand participant 3 (self self) (peer peer) (l l-1) (e e)
    (lp lp))
  (precedes ((0 2) (1 3)) ((0 2) (4 0)) ((1 2) (4 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 0) (0 1)) ((3 0) (1 1)) ((4 1) (0 3))
    ((5 2) (1 3)) ((5 2) (4 0)))
  (absent (e (exp (gen) l-1)) (e (exp (gen) lp)) (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 l l-0)) (exp (gen) (mul eA w e))) key)))
  (neq ((mul eA (rec eB) w e) (one)) (eA eB) ((mul w e) (one)))
  (non-orig (privk B) (privk D) l)
  (precur (4 0))
  (uniq-gen l l-0 eA eB e)
  (operation nonce-test (added-strand participant 3) (exp (gen) e)
    (4 0))
  (label 51)
  (parent 25)
  (unrealized (1 3))
  (comment "8 in cohort - 8 not yet seen"))

Item 52, Parent: 25, Children: 186 187 188 189 190 191 192.

(defskeleton iadh-um
  (vars (key data) (B D name) (l eA eB rndx) (w expt) (l-0 rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eA)
    (lp l) (ep (mul w l-0)))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec eB) w l-0)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (deflistener (cat (exp (gen) l-0) w))
  (precedes ((0 2) (1 3)) ((0 2) (4 0)) ((1 2) (4 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 0) (0 1)) ((3 0) (1 1)) ((4 1) (0 3)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-0))
    (eA (exp (gen) l)))
  (fn-of ("principal-of" (l-0 B) (l D))
    (foo
      ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eA w l-0))) key)))
  (neq ((mul eA (rec eB) w l-0) (one)) (eA eB) ((mul w l-0) (one)))
  (non-orig (privk B) (privk D) l-0)
  (precur (4 0))
  (uniq-gen l eA eB l-0)
  (operation nonce-test (displaced 5 2 ltx-gen 1) (exp (gen) l-1) (4 0))
  (label 52)
  (parent 25)
  (unrealized (1 3))
  (comment "7 in cohort - 7 not yet seen"))

Item 53, Parent: 25, Children: 193 194 195 196 197 198 199.

(defskeleton iadh-um
  (vars (key data) (B D name) (l eA eB rndx) (w expt) (l-0 rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep (mul w l-0)))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec eB) w l-0)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (exp (gen) l-0) w))
  (precedes ((0 2) (1 3)) ((0 2) (4 0)) ((1 2) (4 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 0) (0 1)) ((3 0) (1 1)) ((4 1) (0 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 l l-0)) (exp (gen) (mul eA w l-0))) key)))
  (neq ((mul eA (rec eB) w l-0) (one)) (eA eB) ((mul w l-0) (one)))
  (non-orig (privk B) (privk D) l)
  (precur (4 0))
  (uniq-gen l eA eB l-0)
  (operation nonce-test (displaced 5 3 ltx-gen 1) (exp (gen) l-1) (4 0))
  (label 53)
  (parent 25)
  (unrealized (1 3))
  (comment "7 in cohort - 7 not yet seen"))

Item 54, Parent: 25, Children: 200 201 202 203 204 205 206 207.

(defskeleton iadh-um
  (vars (key data) (B D self name) (l l-0 eA eB rndx) (w expt)
    (l-1 rndx))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eA)
    (lp l-0) (ep (mul w l-1)))
  (defstrand participant 5 (key key) (self B) (peer D) (l l) (e eB)
    (lp l-0) (ep (mul eA (rec eB) w l-1)))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (exp (gen) l-1) w))
  (defstrand ltx-gen 1 (self self) (l l-1))
  (precedes ((0 2) (1 3)) ((0 2) (4 0)) ((1 2) (4 0)) ((2 0) (0 0))
    ((2 0) (1 0)) ((3 0) (0 1)) ((3 0) (1 1)) ((4 1) (0 3))
    ((5 0) (1 3)) ((5 0) (4 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-1 self) (l-0 D) (l B))
    (foo
      ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eA w l-1))) key)))
  (neq ((mul eA (rec eB) w l-1) (one)) (eA eB) ((mul w l-1) (one)))
  (non-orig (privk B) (privk D) l)
  (precur (4 0))
  (uniq-gen l l-0 eA eB l-1)
  (operation nonce-test (added-strand ltx-gen 1) (exp (gen) l-1) (4 0))
  (label 54)
  (parent 25)
  (unrealized (1 3))
  (comment "8 in cohort - 8 not yet seen"))

Item 55, Parent: 26, Children: 208 209 210 211 212 213 214.

(defskeleton iadh-um
  (vars (key data) (B D name) (eB l l-0 e rndx) (w expt))
  (defstrand participant 5 (key key) (self D) (peer B) (l l) (e e)
    (lp l-0) (ep e))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul (rec eB) e e)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (deflistener (cat (exp (gen) (mul (rec eB) e e (rec w))) w))
  (precedes ((0 2) (4 0)) ((1 2) (0 3)) ((1 2) (4 0)) ((2 0) (0 1))
    ((2 0) (1 0)) ((3 0) (0 0)) ((3 0) (1 1)) ((4 1) (1 3)))
  (absent (e (exp (gen) l)) (e (exp (gen) l-0)) (eB (exp (gen) l-0))
    (eB (exp (gen) l)))
  (fn-of ("principal-of" (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul e e))) key)))
  (neq ((mul (rec eB) e e) (one)) (e eB) (e (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen eB l l-0 e)
  (precur (4 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec eB) e e (rec w))) w))
    (exp (gen) (mul (rec eB) e e)) (1 3))
  (label 55)
  (parent 26)
  (unrealized (4 0))
  (comment "7 in cohort - 7 not yet seen"))

Item 56, Parent: 28, Children: 215 216 217 218 219 220 221 222.

(defskeleton iadh-um
  (vars (key data) (B D self peer name) (l l-0 l-1 rndx) (lp expt)
    (eA eB e rndx) (w expt))
  (defstrand participant 5 (key key) (self D) (peer B) (l l) (e eA)
    (lp l-0) (ep e))
  (defstrand participant 5 (key key) (self B) (peer D) (l l-0) (e eB)
    (lp l) (ep (mul eA (rec eB) e)))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (defstrand participant 3 (self self) (peer peer) (l l-1) (e e)
    (lp lp))
  (deflistener (cat (exp (gen) (mul eA (rec eB) e (rec w))) w))
  (precedes ((0 2) (5 0)) ((1 2) (0 3)) ((1 2) (5 0)) ((2 0) (0 1))
    ((2 0) (1 0)) ((3 0) (0 0)) ((3 0) (1 1)) ((4 2) (0 3))
    ((4 2) (5 0)) ((5 1) (1 3)))
  (absent (e (exp (gen) l-1)) (e (exp (gen) lp)) (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 l l-0)) (exp (gen) (mul eA e))) key)))
  (neq ((mul eA (rec eB) e) (one)) (eA eB) (e (one)))
  (non-orig (privk B) (privk D) l l-0)
  (uniq-gen l l-0 eA eB e)
  (precur (5 0))
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul eA (rec eB) e (rec w))) w))
    (exp (gen) (mul eA (rec eB) e)) (1 3))
  (label 56)
  (parent 28)
  (unrealized (5 0))
  (comment "8 in cohort - 8 not yet seen"))