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

Trees: 0 1922.

Tree 0.

(defprotocol iadh-um diffie-hellman
  (defrole participant
    (vars (l e expn) (hl he base) (self peer name) (key data))
    (trace (recv (enc "cert" (exp (gen) l) self (privk self)))
      (recv (enc "cert" hl peer (privk peer))) (send (exp (gen) e))
      (recv he) (send key))
    (uniq-gen e)
    (fn-of (foo ((hash (exp hl l) (exp he e)) key)))
    (neq (he (gen)))
    (absent (e (exp (gen) l)) (e hl)))
  (defrole ltx-gen
    (vars (self name) (l expn))
    (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) (hl he hl-0 he-0 base)
    (eA lA eB lB expn))
  (defstrand participant 5 (key key) (self A) (peer C) (hl hl) (he he)
    (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer D) (hl hl-0)
    (he he-0) (l lB) (e eB))
  (absent (eB (exp (gen) lB)) (eB hl-0) (eA (exp (gen) lA)) (eA hl))
  (fn-of
    (foo ((hash (exp hl-0 lB) (exp he-0 eB)) key)
      ((hash (exp hl lA) (exp he eA)) key)))
  (neq (he-0 (gen)) (eA eB) (he (gen)))
  (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))
  (preskeleton)
  (comment "Not a skeleton"))

Item 1, Parent: 0, Child: 2.

(defskeleton iadh-um
  (vars (key data) (A B C D name) (hl he base) (lA lB eA eB expn))
  (defstrand participant 5 (key key) (self A) (peer C) (hl hl) (he he)
    (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp hl (mul lA (rec lB)))) (he (exp he (mul eA (rec eB))))
    (l lB) (e eB))
  (precedes ((0 2) (1 3)))
  (absent (eB (exp (gen) lB)) (eB (exp hl (mul lA (rec lB))))
    (eA (exp (gen) lA)) (eA hl))
  (fn-of (foo ((hash (exp hl lA) (exp he eA)) key)))
  (neq ((exp he (mul eA (rec eB))) (gen)) (eA eB) (he (gen)))
  (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) (1 0) (1 1) (1 3))
  (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) (hl he base) (lA eA eB l expn))
  (defstrand participant 5 (key key) (self A) (peer C) (hl hl) (he he)
    (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp hl (mul lA (rec l)))) (he (exp he (mul eA (rec eB)))) (l l)
    (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (precedes ((0 2) (1 3)) ((2 0) (1 0)))
  (absent (eB (exp (gen) l)) (eB (exp hl (mul lA (rec l))))
    (eA (exp (gen) lA)) (eA hl))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp hl lA) (exp he eA)) key)))
  (neq ((exp he (mul eA (rec eB))) (gen)) (eA eB) (he (gen)))
  (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) (1 1) (1 3))
  (comment "2 in cohort - 2 not yet seen"))

Item 3, Parent: 2, Children: 5 6 7 8 9 10.

(defskeleton iadh-um
  (vars (key data) (A B C name) (he base) (lA eA eB l expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l))) (he he) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp he (mul eA (rec eB)))) (l l) (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (precedes ((0 2) (1 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 he eA)) key)))
  (neq ((exp he (mul eA (rec eB))) (gen)) (eA eB) (he (gen)))
  (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) (1 3))
  (comment "6 in cohort - 6 not yet seen"))

Item 4, Parent: 2, Children: 11 12 13 14 15 16 17.

(defskeleton iadh-um
  (vars (key data) (A B C D name) (he base) (lA eA eB l l-0 expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l-0))) (he he) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l-0)) (he (exp he (mul eA (rec eB)))) (l l) (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (precedes ((0 2) (1 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 he eA)) key)))
  (neq ((exp he (mul eA (rec eB))) (gen)) (eA eB) (he (gen)))
  (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) (1 3))
  (comment "7 in cohort - 7 not yet seen"))

Item 5, Parent: 3, Children: 18 19.

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

Item 6, Parent: 3, Children: 20 21.

(defskeleton iadh-um
  (vars (key data) (A B C name) (lA eA l e expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l)))
    (he (exp (gen) (mul (rec eA) e e))) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) e)) (l l) (e e))
  (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 (e (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 e e))) key)))
  (neq ((exp (gen) e) (gen)) (eA e)
    ((exp (gen) (mul (rec eA) e e)) (gen)))
  (non-orig (privk A) (privk B) (privk C) lA l)
  (uniq-gen eA l e)
  (operation nonce-test (displaced 3 1 participant 3) (exp (gen) e-0)
    (1 3))
  (label 6)
  (parent 3)
  (unrealized (0 0) (0 1) (0 3))
  (comment "2 in cohort - 2 not yet seen"))

Item 7, Parent: 3, Children: 22 23.

(defskeleton iadh-um
  (vars (key data) (A B C self peer name) (hl base)
    (lA eA eB l l-0 e expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l)))
    (he (exp (gen) (mul (rec eA) eB e))) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) e)) (l l) (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand participant 3 (self self) (peer peer) (hl hl) (l l-0)
    (e e))
  (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 2) (0 3)) ((3 2) (1 3)))
  (absent (e (exp (gen) l-0)) (e hl) (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 e))) key)))
  (neq ((exp (gen) e) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB e)) (gen)))
  (non-orig (privk A) (privk B) (privk C) lA l)
  (uniq-gen eA eB l e)
  (operation nonce-test (added-strand participant 3) (exp (gen) e)
    (1 3))
  (label 7)
  (parent 3)
  (unrealized (0 0) (0 1) (0 3))
  (comment "2 in cohort - 2 not yet seen"))

Item 8, Parent: 3, Children: 24 25.

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

Item 9, Parent: 3, Children: 26 27 28.

(defskeleton iadh-um
  (vars (key data) (A B C self name) (lA eA eB l l-0 expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l)))
    (he (exp (gen) (mul (rec eA) eB l-0))) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) l-0)) (l l) (e eB))
  (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 1)) ((2 0) (1 0))
    ((3 0) (0 3)) ((3 0) (1 3)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) lA))
    (eA (exp (gen) (mul (rec lA) l l))))
  (fn-of ("principal-of" (l-0 self) (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eB l-0))) key)))
  (neq ((exp (gen) l-0) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l-0)) (gen)))
  (non-orig (privk A) (privk B) (privk C) lA l)
  (uniq-gen eA eB l l-0)
  (operation nonce-test (added-strand ltx-gen 1) (exp (gen) l-0) (1 3))
  (label 9)
  (parent 3)
  (unrealized (0 0) (0 1) (0 3))
  (comment "3 in cohort - 3 not yet seen"))

Item 10, Parent: 3, Children: 29 30 31 32 33 34.

(defskeleton iadh-um
  (vars (key data) (A B C name) (he base) (lA eA eB l expn) (w expr))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l))) (he he) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp he (mul eA (rec eB)))) (l l) (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp he (mul eA (rec eB) (rec w))) w))
  (precedes ((0 2) (3 0)) ((1 2) (3 0)) ((2 0) (0 1)) ((2 0) (1 0))
    ((3 1) (1 3)))
  (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 he eA)) key)))
  (neq ((exp he (mul eA (rec eB))) (gen)) (eA eB) (he (gen)))
  (non-orig (privk A) (privk B) (privk C) lA l)
  (uniq-gen eA eB l)
  (precur (3 0))
  (operation nonce-test
    (added-listener (cat (exp he (mul eA (rec eB) (rec w))) w))
    (exp he (mul eA (rec eB))) (1 3))
  (label 10)
  (parent 3)
  (unrealized (0 0) (0 1) (3 0))
  (comment "6 in cohort - 6 not yet seen"))

Item 11, Parent: 4, Children: 35 36 37.

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

Item 12, Parent: 4, Children: 38 39 40.

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

Item 13, Parent: 4, Children: 41 42 43.

(defskeleton iadh-um
  (vars (key data) (A B C D self peer name) (hl base)
    (lA eA eB l l-0 l-1 e expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l-0)))
    (he (exp (gen) (mul (rec eA) eB e))) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l-0)) (he (exp (gen) e)) (l l) (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (defstrand participant 3 (self self) (peer peer) (hl hl) (l l-1)
    (e e))
  (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 2) (0 3)) ((4 2) (1 3)))
  (absent (e (exp (gen) l-1)) (e hl) (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 e))) key)))
  (neq ((exp (gen) e) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB e)) (gen)))
  (non-orig (privk A) (privk B) (privk C) (privk D) lA l)
  (uniq-gen eA eB l l-0 e)
  (operation nonce-test (added-strand participant 3) (exp (gen) e)
    (1 3))
  (label 13)
  (parent 4)
  (unrealized (0 0) (0 1) (0 3))
  (comment "3 in cohort - 3 not yet seen"))

Item 14, Parent: 4, Children: 44 45 46.

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

Item 15, Parent: 4, Children: 47 48 49.

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

Item 16, Parent: 4, Children: 50 51 52 53.

(defskeleton iadh-um
  (vars (key data) (A B C D self name) (lA eA eB l l-0 l-1 expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l-0)))
    (he (exp (gen) (mul (rec eA) eB l-1))) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l-0)) (he (exp (gen) l-1)) (l l) (e eB))
  (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 1)) ((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) lA))
    (eA (exp (gen) (mul (rec lA) l 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 eB l-1))) key)))
  (neq ((exp (gen) l-1) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l-1)) (gen)))
  (non-orig (privk A) (privk B) (privk C) (privk D) lA l)
  (uniq-gen eA eB l l-0 l-1)
  (operation nonce-test (added-strand ltx-gen 1) (exp (gen) l-1) (1 3))
  (label 16)
  (parent 4)
  (unrealized (0 0) (0 1) (0 3))
  (comment "4 in cohort - 4 not yet seen"))

Item 17, Parent: 4, Children: 54 55 56 57 58 59 60.

(defskeleton iadh-um
  (vars (key data) (A B C D name) (he base) (lA eA eB l l-0 expn)
    (w expr))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l-0))) (he he) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l-0)) (he (exp he (mul eA (rec eB)))) (l l) (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (exp he (mul eA (rec eB) (rec w))) w))
  (precedes ((0 2) (4 0)) ((1 2) (4 0)) ((2 0) (0 1)) ((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) 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 he eA)) key)))
  (neq ((exp he (mul eA (rec eB))) (gen)) (eA eB) (he (gen)))
  (non-orig (privk A) (privk B) (privk C) (privk D) lA l)
  (uniq-gen eA eB l l-0)
  (precur (4 0))
  (operation nonce-test
    (added-listener (cat (exp he (mul eA (rec eB) (rec w))) w))
    (exp he (mul eA (rec eB))) (1 3))
  (label 17)
  (parent 4)
  (unrealized (0 0) (0 1) (4 0))
  (comment "7 in cohort - 7 not yet seen"))

Item 18, Parent: 5, Child: 61.

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

Item 19, Parent: 5.

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

Item 20, Parent: 6, Child: 62.

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

Item 21, Parent: 6.

(defskeleton iadh-um
  (vars (key data) (A B C name) (eA l e l-0 expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul l l (rec l-0))))
    (he (exp (gen) (mul (rec eA) e e))) (l l-0) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) e)) (l l) (e e))
  (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 (e (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 e e))) key)))
  (neq ((exp (gen) e) (gen)) (eA e)
    ((exp (gen) (mul (rec eA) e e)) (gen)))
  (non-orig (privk A) (privk B) (privk C) l l-0)
  (uniq-gen eA l e l-0)
  (operation encryption-test (added-strand ltx-gen 1)
    (enc "cert" (exp (gen) l-0) A (privk A)) (0 0))
  (label 21)
  (parent 6)
  (unrealized (0 1) (0 3))
  (comment "empty cohort"))

Item 22, Parent: 7, Child: 63.

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

Item 23, Parent: 7.

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

Item 24, Parent: 8, Child: 64.

(defskeleton iadh-um
  (vars (key data) (B C name) (eA eB l expn))
  (defstrand participant 5 (key key) (self B) (peer C)
    (hl (exp (gen) l)) (he (exp (gen) (mul (rec eA) eB l))) (l l)
    (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) l)) (l l) (e eB))
  (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 eB l))) key)))
  (neq ((exp (gen) l) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l)) (gen)))
  (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 24)
  (parent 8)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 25, Parent: 8.

(defskeleton iadh-um
  (vars (key data) (A B C name) (eA eB l l-0 expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul l l (rec l-0))))
    (he (exp (gen) (mul (rec eA) eB l))) (l l-0) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) l)) (l l) (e eB))
  (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 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 l))) key)))
  (neq ((exp (gen) l) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l)) (gen)))
  (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 25)
  (parent 8)
  (unrealized (0 1) (0 3))
  (comment "empty cohort"))

Item 26, Parent: 9, Child: 65.

(defskeleton iadh-um
  (vars (key data) (B C self name) (eA eB l l-0 expn))
  (defstrand participant 5 (key key) (self B) (peer C)
    (hl (exp (gen) l-0)) (he (exp (gen) (mul (rec eA) eB l))) (l l-0)
    (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l-0)) (he (exp (gen) l)) (l l-0) (e eB))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self self) (l l))
  (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-0)) (eA (exp (gen) l-0)))
  (fn-of ("principal-of" (l-0 B) (l self))
    (foo ((hash (exp (gen) (mul l-0 l-0)) (exp (gen) (mul eB l))) key)))
  (neq ((exp (gen) l) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l)) (gen)))
  (non-orig (privk B) (privk C) 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 26)
  (parent 9)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 27, Parent: 9.

(defskeleton iadh-um
  (vars (key data) (B C self name) (eA eB l l-0 expn))
  (defstrand participant 5 (key key) (self self) (peer C)
    (hl (exp (gen) (mul l l (rec l-0))))
    (he (exp (gen) (mul (rec eA) eB l-0))) (l l-0) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) l-0)) (l l) (e eB))
  (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 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 self) (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eB l-0))) key)))
  (neq ((exp (gen) l-0) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l-0)) (gen)))
  (non-orig (privk B) (privk C) (privk self) 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 27)
  (parent 9)
  (unrealized (0 1) (0 3))
  (comment "empty cohort"))

Item 28, Parent: 9.

(defskeleton iadh-um
  (vars (key data) (A B C self name) (eA eB l l-0 l-1 expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul l l (rec l-1))))
    (he (exp (gen) (mul (rec eA) eB l-0))) (l l-1) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) l-0)) (l l) (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self self) (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) (0 3)) ((3 0) (1 3)) ((4 0) (0 0)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) l-1))
    (eA (exp (gen) (mul l l (rec l-1)))))
  (fn-of ("principal-of" (l-1 A) (l-0 self) (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eB l-0))) key)))
  (neq ((exp (gen) l-0) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l-0)) (gen)))
  (non-orig (privk A) (privk B) (privk C) 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 28)
  (parent 9)
  (unrealized (0 1) (0 3))
  (comment "empty cohort"))

Item 29, Parent: 10, Children: 66 67.

(defskeleton iadh-um
  (vars (key data) (A B C name) (lA eA eB l expn) (w expr))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l)))
    (he (exp (gen) (mul (rec eA) eB w))) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) w)) (l l) (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (gen) w))
  (precedes ((0 2) (3 0)) ((1 2) (0 3)) ((1 2) (3 0)) ((2 0) (0 1))
    ((2 0) (1 0)) ((3 1) (1 3)))
  (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 w))) key)))
  (neq ((exp (gen) w) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB w)) (gen)))
  (non-orig (privk A) (privk B) (privk C) lA l)
  (uniq-gen eA eB l)
  (precur (3 0))
  (operation nonce-test
    (contracted (he (exp (gen) (mul (rec eA) eB w)))) (gen) (3 0))
  (label 29)
  (parent 10)
  (unrealized (0 0) (0 1) (0 3))
  (comment "2 in cohort - 2 not yet seen"))

Item 30, Parent: 10, Children: 68 69.

(defskeleton iadh-um
  (vars (key data) (A B C name) (eB l expn) (w expr) (l-0 e expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul l l (rec l-0)))) (he (exp (gen) (mul eB w)))
    (l l-0) (e e))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) (mul w e))) (l l) (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) e) w))
  (precedes ((0 2) (3 0)) ((1 2) (0 3)) ((1 2) (3 0)) ((2 0) (0 1))
    ((2 0) (1 0)) ((3 1) (1 3)))
  (absent (e (exp (gen) l-0)) (e (exp (gen) (mul l l (rec l-0))))
    (eB (exp (gen) l)))
  (fn-of ("principal-of" (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eB w e))) key)))
  (neq ((exp (gen) (mul w e)) (gen)) (e eB)
    ((exp (gen) (mul eB w)) (gen)))
  (non-orig (privk A) (privk B) (privk C) l l-0)
  (precur (3 0))
  (uniq-gen eB l e)
  (operation nonce-test (displaced 4 0 participant 3) (exp (gen) e-0)
    (3 0))
  (label 30)
  (parent 10)
  (unrealized (0 0) (0 1))
  (comment "2 in cohort - 2 not yet seen"))

Item 31, Parent: 10, Children: 70 71.

(defskeleton iadh-um
  (vars (key data) (A B C name) (lA eA expn) (w expr) (l e expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l)))
    (he (exp (gen) (mul (rec eA) w e e))) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) (mul w e))) (l l) (e e))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) e) w))
  (precedes ((0 2) (3 0)) ((1 2) (0 3)) ((1 2) (3 0)) ((2 0) (0 1))
    ((2 0) (1 0)) ((3 1) (1 3)))
  (absent (e (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 w e e))) key)))
  (neq ((exp (gen) (mul w e)) (gen)) (eA e)
    ((exp (gen) (mul (rec eA) w e e)) (gen)))
  (non-orig (privk A) (privk B) (privk C) lA l)
  (precur (3 0))
  (uniq-gen eA l e)
  (operation nonce-test (displaced 4 1 participant 3) (exp (gen) e-0)
    (3 0))
  (label 31)
  (parent 10)
  (unrealized (0 0) (0 1) (0 3))
  (comment "2 in cohort - 2 not yet seen"))

Item 32, Parent: 10, Children: 72 73.

(defskeleton iadh-um
  (vars (key data) (A B C self peer name) (hl base) (lA eA eB l expn)
    (w expr) (l-0 e expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l)))
    (he (exp (gen) (mul (rec eA) eB w e))) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) (mul w e))) (l l) (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) e) w))
  (defstrand participant 3 (self self) (peer peer) (hl hl) (l l-0)
    (e e))
  (precedes ((0 2) (3 0)) ((1 2) (0 3)) ((1 2) (3 0)) ((2 0) (0 1))
    ((2 0) (1 0)) ((3 1) (1 3)) ((4 2) (0 3)) ((4 2) (3 0)))
  (absent (e (exp (gen) l-0)) (e hl) (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 w e))) key)))
  (neq ((exp (gen) (mul w e)) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB w e)) (gen)))
  (non-orig (privk A) (privk B) (privk C) lA l)
  (precur (3 0))
  (uniq-gen eA eB l e)
  (operation nonce-test (added-strand participant 3) (exp (gen) e)
    (3 0))
  (label 32)
  (parent 10)
  (unrealized (0 0) (0 1) (0 3))
  (comment "2 in cohort - 2 not yet seen"))

Item 33, Parent: 10, Children: 74 75.

(defskeleton iadh-um
  (vars (key data) (A B C name) (lA eA eB expn) (w expr) (l expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l)))
    (he (exp (gen) (mul (rec eA) eB w l))) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) (mul w l))) (l l) (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (deflistener (cat (exp (gen) l) w))
  (precedes ((0 2) (3 0)) ((1 2) (0 3)) ((1 2) (3 0)) ((2 0) (0 1))
    ((2 0) (1 0)) ((3 1) (1 3)))
  (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 w l))) key)))
  (neq ((exp (gen) (mul w l)) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB w l)) (gen)))
  (non-orig (privk A) (privk B) (privk C) lA 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 33)
  (parent 10)
  (unrealized (0 0) (0 1) (0 3))
  (comment "2 in cohort - 2 not yet seen"))

Item 34, Parent: 10, Children: 76 77 78.

(defskeleton iadh-um
  (vars (key data) (A B C self name) (lA eA eB l expn) (w expr)
    (l-0 expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l)))
    (he (exp (gen) (mul (rec eA) eB w l-0))) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer B)
    (hl (exp (gen) l)) (he (exp (gen) (mul w l-0))) (l l) (e eB))
  (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) (3 0)) ((1 2) (0 3)) ((1 2) (3 0)) ((2 0) (0 1))
    ((2 0) (1 0)) ((3 1) (1 3)) ((4 0) (0 3)) ((4 0) (3 0)))
  (absent (eB (exp (gen) l)) (eA (exp (gen) lA))
    (eA (exp (gen) (mul (rec lA) l l))))
  (fn-of ("principal-of" (l-0 self) (l B))
    (foo ((hash (exp (gen) (mul l l)) (exp (gen) (mul eB w l-0))) key)))
  (neq ((exp (gen) (mul w l-0)) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB w l-0)) (gen)))
  (non-orig (privk A) (privk B) (privk C) lA l)
  (precur (3 0))
  (uniq-gen eA eB l l-0)
  (operation nonce-test (added-strand ltx-gen 1) (exp (gen) l-0) (3 0))
  (label 34)
  (parent 10)
  (unrealized (0 0) (0 1) (0 3))
  (comment "3 in cohort - 3 not yet seen"))

Item 35, Parent: 11, Child: 79.

(defskeleton iadh-um
  (vars (key data) (B C D name) (eB l e l-0 expn))
  (defstrand participant 5 (key key) (self B) (peer C)
    (hl (exp (gen) l)) (he (exp (gen) eB)) (l l-0) (e e))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l)) (he (exp (gen) e)) (l l-0) (e eB))
  (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 (e (exp (gen) l-0)) (e (exp (gen) l)) (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 eB e))) key)))
  (neq ((exp (gen) e) (gen)) (e eB) ((exp (gen) eB) (gen)))
  (non-orig (privk B) (privk C) (privk D) l-0)
  (uniq-gen eB l e l-0)
  (operation encryption-test (displaced 4 2 ltx-gen 1)
    (enc "cert" (exp (gen) l-1) A (privk A)) (0 0))
  (label 35)
  (parent 11)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 36, Parent: 11, Child: 80.

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

Item 37, Parent: 11.

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

Item 38, Parent: 12, Child: 81.

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

Item 39, Parent: 12, Child: 82.

(defskeleton iadh-um
  (vars (key data) (B C D name) (eA l e l-0 expn))
  (defstrand participant 5 (key key) (self D) (peer C)
    (hl (exp (gen) l)) (he (exp (gen) (mul (rec eA) e e))) (l l-0)
    (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l-0)) (he (exp (gen) e)) (l l) (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 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-0 D) (l B))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul e e))) key)))
  (neq ((exp (gen) e) (gen)) (eA e)
    ((exp (gen) (mul (rec eA) e e)) (gen)))
  (non-orig (privk B) (privk C) (privk D) l l-0)
  (uniq-gen eA l e l-0)
  (operation encryption-test (displaced 4 3 ltx-gen 1)
    (enc "cert" (exp (gen) l-1) A (privk A)) (0 0))
  (label 39)
  (parent 12)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 40, Parent: 12.

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

Item 41, Parent: 13, Child: 83.

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

Item 42, Parent: 13, Child: 84.

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

Item 43, Parent: 13.

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

Item 44, Parent: 14, Child: 85.

(defskeleton iadh-um
  (vars (key data) (B C D name) (eA eB l l-0 expn))
  (defstrand participant 5 (key key) (self B) (peer C)
    (hl (exp (gen) l)) (he (exp (gen) (mul (rec eA) eB l-0))) (l l-0)
    (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l)) (he (exp (gen) l-0)) (l l-0) (e eB))
  (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 eB l-0))) key)))
  (neq ((exp (gen) l-0) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l-0)) (gen)))
  (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 44)
  (parent 14)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 45, Parent: 14, Child: 86.

(defskeleton iadh-um
  (vars (key data) (B C D name) (eA eB l l-0 expn))
  (defstrand participant 5 (key key) (self D) (peer C)
    (hl (exp (gen) l)) (he (exp (gen) (mul (rec eA) eB l))) (l l-0)
    (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l-0)) (he (exp (gen) l)) (l l) (e eB))
  (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 eB l))) key)))
  (neq ((exp (gen) l) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l)) (gen)))
  (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 45)
  (parent 14)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 46, Parent: 14.

(defskeleton iadh-um
  (vars (key data) (A B C D name) (eA eB l l-0 l-1 expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul l l-0 (rec l-1))))
    (he (exp (gen) (mul (rec eA) eB l-0))) (l l-1) (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l)) (he (exp (gen) l-0)) (l l-0) (e eB))
  (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) (0 1)) ((3 0) (1 1)) ((4 0) (0 0)))
  (absent (eB (exp (gen) l-0)) (eB (exp (gen) l)) (eA (exp (gen) l-1))
    (eA (exp (gen) (mul l l-0 (rec l-1)))))
  (fn-of ("principal-of" (l-1 A) (l-0 B) (l D))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eB l-0))) key)))
  (neq ((exp (gen) l-0) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l-0)) (gen)))
  (non-orig (privk A) (privk B) (privk C) (privk D) l-0 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 46)
  (parent 14)
  (unrealized (0 1) (0 3))
  (comment "empty cohort"))

Item 47, Parent: 15, Child: 87.

(defskeleton iadh-um
  (vars (key data) (B C D name) (eA eB l l-0 expn))
  (defstrand participant 5 (key key) (self B) (peer C)
    (hl (exp (gen) l)) (he (exp (gen) (mul (rec eA) eB l))) (l l-0)
    (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l)) (he (exp (gen) l)) (l l-0) (e eB))
  (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 eB l))) key)))
  (neq ((exp (gen) l) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l)) (gen)))
  (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 47)
  (parent 15)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 48, Parent: 15, Child: 88.

(defskeleton iadh-um
  (vars (key data) (B C D name) (eA eB l l-0 expn))
  (defstrand participant 5 (key key) (self D) (peer C)
    (hl (exp (gen) l)) (he (exp (gen) (mul (rec eA) eB l-0))) (l l-0)
    (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l-0)) (he (exp (gen) l-0)) (l l) (e eB))
  (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 eB l-0))) key)))
  (neq ((exp (gen) l-0) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l-0)) (gen)))
  (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 48)
  (parent 15)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

Item 49, Parent: 15.

(defskeleton iadh-um
  (vars (key data) (A B C D name) (eA eB l l-0 l-1 expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul l l-0 (rec l-1))))
    (he (exp (gen) (mul (rec eA) eB l-0))) (l l-1) (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l-0)) (he (exp (gen) l-0)) (l l) (e eB))
  (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) (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 l-0))) key)))
  (neq ((exp (gen) l-0) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l-0)) (gen)))
  (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 49)
  (parent 15)
  (unrealized (0 1) (0 3))
  (comment "empty cohort"))

Item 50, Parent: 16, Child: 89.

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

Item 51, Parent: 16, Child: 90.

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

Item 52, Parent: 16.

(defskeleton iadh-um
  (vars (key data) (B C D self name) (eA eB l l-0 l-1 expn))
  (defstrand participant 5 (key key) (self self) (peer C)
    (hl (exp (gen) (mul l l-0 (rec l-1))))
    (he (exp (gen) (mul (rec eA) eB l-1))) (l l-1) (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l-0)) (he (exp (gen) l-1)) (l l) (e eB))
  (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 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 self) (l-0 D) (l B))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul eB l-1))) key)))
  (neq ((exp (gen) l-1) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB l-1)) (gen)))
  (non-orig (privk B) (privk C) (privk D) (privk self) l l-1)
  (uniq-gen eA eB l l-0 l-1)
  (operation encryption-test (displaced 5 4 ltx-gen 1)
    (enc "cert" (exp (gen) l-2) A (privk A)) (0 0))
  (label 52)
  (parent 16)
  (unrealized (0 1) (0 3))
  (comment "empty cohort"))

Item 53, Parent: 16.

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

Item 54, Parent: 17, Children: 91 92 93.

(defskeleton iadh-um
  (vars (key data) (A B C D name) (lA eA eB l l-0 expn) (w expr))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l-0)))
    (he (exp (gen) (mul (rec eA) eB w))) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l-0)) (he (exp (gen) w)) (l l) (e eB))
  (defstrand ltx-gen 1 (self B) (l l))
  (defstrand ltx-gen 1 (self D) (l l-0))
  (deflistener (cat (gen) 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 1)) ((3 0) (1 1)) ((4 1) (1 3)))
  (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 w))) key)))
  (neq ((exp (gen) w) (gen)) (eA eB)
    ((exp (gen) (mul (rec eA) eB w)) (gen)))
  (non-orig (privk A) (privk B) (privk C) (privk D) lA l)
  (uniq-gen eA eB l l-0)
  (precur (4 0))
  (operation nonce-test
    (contracted (he (exp (gen) (mul (rec eA) eB w)))) (gen) (4 0))
  (label 54)
  (parent 17)
  (unrealized (0 0) (0 1) (0 3))
  (comment "3 in cohort - 3 not yet seen"))

Item 55, Parent: 17, Children: 94 95 96.

(defskeleton iadh-um
  (vars (key data) (A B C D name) (eB l l-0 expn) (w expr) (l-1 e expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul l l-0 (rec l-1)))) (he (exp (gen) (mul eB w)))
    (l l-1) (e e))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l-0)) (he (exp (gen) (mul w e))) (l l) (e eB))
  (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) (4 0)) ((1 2) (0 3)) ((1 2) (4 0)) ((2 0) (0 1))
    ((2 0) (1 0)) ((3 0) (0 1)) ((3 0) (1 1)) ((4 1) (1 3)))
  (absent (e (exp (gen) l-1)) (e (exp (gen) (mul l l-0 (rec l-1))))
    (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 eB w e))) key)))
  (neq ((exp (gen) (mul w e)) (gen)) (e eB)
    ((exp (gen) (mul eB w)) (gen)))
  (non-orig (privk A) (privk B) (privk C) (privk D) l l-1)
  (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 55)
  (parent 17)
  (unrealized (0 0) (0 1))
  (comment "3 in cohort - 3 not yet seen"))

Item 56, Parent: 17, Children: 97 98 99.

(defskeleton iadh-um
  (vars (key data) (A B C D name) (lA eA l expn) (w expr) (l-0 e expn))
  (defstrand participant 5 (key key) (self A) (peer C)
    (hl (exp (gen) (mul (rec lA) l l-0)))
    (he (exp (gen) (mul (rec eA) w e e))) (l lA) (e eA))
  (defstrand participant 5 (key key) (self B) (peer D)
    (hl (exp (gen) l)) (he (exp (gen) (mul w e))) (l l-0) (e e))
  (defstrand ltx-gen 1 (self B) (l l-0))
  (defstrand ltx-gen 1 (self D) (l l))
  (deflistener (cat (exp (gen) e) 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 1)) ((3 0) (1 1)) ((4 1) (1 3)))
  (absent (e (exp (gen) l-0)) (e (exp (gen) l)) (eA (exp (gen) lA))
    (eA (exp (gen) (mul (rec lA) l l-0))))
  (fn-of ("principal-of" (l D) (l-0 B))
    (foo ((hash (exp (gen) (mul l l-0)) (exp (gen) (mul w e e))) key)))
  (neq ((exp (gen) (mul w e)) (gen)) (eA e)
    ((exp (gen) (mul (rec eA) w e e)) (gen)))
  (non-orig (privk A) (privk B) (privk C) (privk D) lA l-0)
  (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 56)
  (parent 17)
  (unrealized (0 0) (0 1) (0 3))
  (comment "3 in cohort - 3 not yet seen"))

Item 57, Parent: 17, Children: 100 101 102.