(herald "Signed group DH exchange (version with auth failure)"
  (algebra diffie-hellman) (limit 100))

(comment "CPSA 4.4.3")
(comment "All input read from tst/dh_group_sig_auth_failure.scm")
(comment "Step count limited to 100")

(defprotocol dh_sig diffie-hellman
  (defrole group-init
    (vars (alpha rndx) (group text) (group-dist chan))
    (trace (send group-dist (cat "Group id" group (exp (gen) alpha))))
    (uniq-gen alpha)
    (conf group-dist))
  (defrole init
    (vars (x rndx) (y expt) (g base) (group text) (a b name)
      (group-dist chan))
    (trace (recv group-dist (cat "Group id" group g))
      (send (enc (exp g x) (privk a)))
      (recv (enc (exp g y) (exp g x) (privk b)))
      (send (enc "final" (exp g y) (exp g x) (privk a))))
    (uniq-gen x)
    (auth group-dist))
  (defrole resp
    (vars (y rndx) (x expt) (g base) (group text) (a b name)
      (group-dist chan))
    (trace (recv group-dist (cat "Group id" group g))
      (recv (enc (exp g x) (privk a)))
      (send (enc (exp g y) (exp g x) (privk b)))
      (recv (enc "final" (exp g y) (exp g x) (privk a))))
    (uniq-gen y)
    (absent (y x))
    (auth group-dist))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton dh_sig
  (vars (group text) (a b name) (g base) (group-dist chan) (x rndx)
    (y expt))
  (defstrand init 4 (group group) (a a) (b b) (g g)
    (group-dist group-dist) (x x) (y y))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (auth group-dist)
  (traces
    ((recv group-dist (cat "Group id" group g))
      (send (enc (exp g x) (privk a)))
      (recv (enc (exp g y) (exp g x) (privk b)))
      (send (enc "final" (exp g y) (exp g x) (privk a)))))
  (label 0)
  (unrealized (0 0) (0 2))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group text) (a b name) (group-dist chan) (x rndx) (y expt)
    (alpha rndx))
  (defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (precedes ((1 0) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen x alpha)
  (conf group-dist)
  (auth group-dist)
  (operation channel-test (added-strand group-init 1)
    (ch-msg group-dist (cat "Group id" group (exp (gen) alpha))) (0 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha)))))
  (label 1)
  (parent 0)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (alpha x y rndx) (x-0 expt))
  (defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (x x) (y (mul x y (rec x-0))))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) (mul alpha x (rec x-0)))) (group-dist group-dist-0)
    (y y) (x x-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen alpha x y)
  (absent (y x-0))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation encryption-test (added-strand resp 3)
    (enc (exp (gen) (mul alpha x y (rec x-0))) (exp (gen) (mul alpha x))
      (privk b)) (0 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul alpha x y (rec x-0)))
          (exp (gen) (mul alpha x)) (privk b)))
      (send
        (enc "final" (exp (gen) (mul alpha x y (rec x-0)))
          (exp (gen) (mul alpha x)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0
       (cat "Group id" group-0 (exp (gen) (mul alpha x (rec x-0)))))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul alpha x y (rec x-0)))
          (exp (gen) (mul alpha x)) (privk b)))))
  (label 2)
  (parent 1)
  (unrealized (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig
  (vars (group text) (a b a-0 name) (group-dist chan) (y x alpha rndx))
  (defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation channel-test (displaced 3 1 group-init 1)
    (ch-msg group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
    (2 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))))
  (label 3)
  (parent 2)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (y alpha x alpha-0 rndx))
  (defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (x x) (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (y y)
    (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((3 0) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0)
  (absent (y (mul alpha x (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation channel-test (added-strand group-init 1)
    (ch-msg group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
    (2 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b)))
      (send
        (enc "final" (exp (gen) (mul y alpha-0))
          (exp (gen) (mul alpha x)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 4)
  (parent 2)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group text) (a b a-0 name) (group-dist chan) (y x alpha rndx))
  (defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (precedes ((0 1) (2 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation generalization weakened ((0 1) (2 0)))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))))
  (label 5)
  (parent 3)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (x x) (y y) (g (exp (gen) alpha)) (group group)
        (group-dist group-dist))))
  (origs))

(defskeleton dh_sig
  (vars (group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (y alpha x alpha-0 rndx))
  (defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (x x) (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (y y)
    (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (precedes ((0 1) (2 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2))
    ((3 0) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0)
  (absent (y (mul alpha x (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation generalization weakened ((0 1) (2 0)))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b)))
      (send
        (enc "final" (exp (gen) (mul y alpha-0))
          (exp (gen) (mul alpha x)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 6)
  (parent 4)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (y alpha x alpha-0 rndx))
  (defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (x x) (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (y y)
    (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (precedes ((0 1) (2 1)) ((1 0) (0 0)) ((2 2) (0 2)) ((3 0) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0)
  (absent (y (mul alpha x (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation generalization weakened ((1 0) (2 0)))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b)))
      (send
        (enc "final" (exp (gen) (mul y alpha-0))
          (exp (gen) (mul alpha x)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 7)
  (parent 6)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (x x) (y (mul y (rec alpha) alpha-0))
        (g (exp (gen) alpha)) (group group) (group-dist group-dist))))
  (origs))

(comment "Nothing left to do")

(defprotocol dh_sig diffie-hellman
  (defrole group-init
    (vars (alpha rndx) (group text) (group-dist chan))
    (trace (send group-dist (cat "Group id" group (exp (gen) alpha))))
    (uniq-gen alpha)
    (conf group-dist))
  (defrole init
    (vars (x rndx) (y expt) (g base) (group text) (a b name)
      (group-dist chan))
    (trace (recv group-dist (cat "Group id" group g))
      (send (enc (exp g x) (privk a)))
      (recv (enc (exp g y) (exp g x) (privk b)))
      (send (enc "final" (exp g y) (exp g x) (privk a))))
    (uniq-gen x)
    (auth group-dist))
  (defrole resp
    (vars (y rndx) (x expt) (g base) (group text) (a b name)
      (group-dist chan))
    (trace (recv group-dist (cat "Group id" group g))
      (recv (enc (exp g x) (privk a)))
      (send (enc (exp g y) (exp g x) (privk b)))
      (recv (enc "final" (exp g y) (exp g x) (privk a))))
    (uniq-gen y)
    (absent (y x))
    (auth group-dist))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton dh_sig
  (vars (group text) (a b name) (g base) (group-dist chan) (y rndx)
    (x expt))
  (defstrand resp 4 (group group) (a a) (b b) (g g)
    (group-dist group-dist) (y y) (x x))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (absent (y x))
  (auth group-dist)
  (traces
    ((recv group-dist (cat "Group id" group g))
      (recv (enc (exp g x) (privk a)))
      (send (enc (exp g y) (exp g x) (privk b)))
      (recv (enc "final" (exp g y) (exp g x) (privk a)))))
  (label 8)
  (unrealized (0 0) (0 1) (0 3))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group text) (a b name) (group-dist chan) (y rndx) (x expt)
    (alpha rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (precedes ((1 0) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation channel-test (added-strand group-init 1)
    (ch-msg group-dist (cat "Group id" group (exp (gen) alpha))) (0 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha)))))
  (label 9)
  (parent 8)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group group-0 text) (a b name) (group-dist group-dist-0 chan)
    (y rndx) (x expt) (alpha x-0 rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a)
    (g (exp (gen) (mul x alpha (rec x-0)))) (group-dist group-dist-0)
    (x x-0))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x-0)
  (absent (y x))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation encryption-test (added-strand init 2)
    (enc (exp (gen) (mul x alpha)) (privk a)) (0 1))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0
       (cat "Group id" group-0 (exp (gen) (mul x alpha (rec x-0)))))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))))
  (label 10)
  (parent 9)
  (unrealized (0 3) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig
  (vars (group text) (a b name) (group-dist chan) (y x alpha rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation channel-test (displaced 3 1 group-init 1)
    (ch-msg group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
    (2 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))))
  (label 11)
  (parent 10)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig
  (vars (group group-0 text) (a b name) (group-dist group-dist-0 chan)
    (y alpha x alpha-0 rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1)) ((3 0) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation channel-test (added-strand group-init 1)
    (ch-msg group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
    (2 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha))
          (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 12)
  (parent 10)
  (unrealized (0 3))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig
  (vars (group text) (a b b-0 name) (group-dist chan) (alpha y x rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 4 (group group) (a a) (b b-0) (g (exp (gen) alpha))
    (group-dist group-dist) (x x) (y y))
  (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((2 3) (0 3)))
  (non-orig (privk a) (privk b))
  (uniq-gen alpha y x)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation encryption-test (displaced 2 3 init 4)
    (enc "final" (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x-0))
      (privk a)) (0 3))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk b-0)))
      (send
        (enc "final" (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk a)))))
  (label 13)
  (parent 11)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (y y) (x x) (g (exp (gen) alpha)) (group group)
        (group-dist group-dist))))
  (origs))

(defskeleton dh_sig
  (vars (group group-0 text) (a b b-0 name)
    (group-dist group-dist-0 chan) (alpha y x x-0 rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (group group-0) (a a) (b b-0)
    (g (exp (gen) (mul alpha x (rec x-0)))) (group-dist group-dist-0)
    (x x-0) (y (mul y (rec x) x-0)))
  (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((2 1) (3 0)) ((3 3) (0 3)))
  (non-orig (privk a) (privk b))
  (uniq-gen alpha y x x-0)
  (absent (y x))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation encryption-test (added-strand init 4)
    (enc "final" (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
      (privk a)) (0 3))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a))))
    ((recv group-dist-0
       (cat "Group id" group-0 (exp (gen) (mul alpha x (rec x-0)))))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk b-0)))
      (send
        (enc "final" (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk a)))))
  (label 14)
  (parent 11)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig
  (vars (group group-0 text) (a b b-0 name)
    (group-dist group-dist-0 chan) (y alpha alpha-0 x rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x (mul (rec alpha) alpha-0 x)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (group group-0) (a a) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x)
    (y (mul y alpha (rec alpha-0))))
  (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (3 0))
    ((3 1) (0 1)) ((3 3) (0 3)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha alpha-0 x)
  (absent (y (mul (rec alpha) alpha-0 x)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation encryption-test (displaced 2 4 init 4)
    (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x-0 alpha-0))
      (privk a)) (0 3))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul alpha-0 x))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha))
          (exp (gen) (mul alpha-0 x)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul alpha-0 x))
          (privk b-0)))
      (send
        (enc "final" (exp (gen) (mul y alpha))
          (exp (gen) (mul alpha-0 x)) (privk a)))))
  (label 15)
  (parent 12)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group group-0 group-1 text) (a b b-0 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (y alpha x alpha-0 x-0 rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (group group-1) (a a) (b b-0)
    (g (exp (gen) (mul x alpha-0 (rec x-0)))) (group-dist group-dist-1)
    (x x-0) (y (mul y alpha (rec x) (rec alpha-0) x-0)))
  (precedes ((0 2) (4 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((2 1) (4 0)) ((3 0) (2 0)) ((4 3) (0 3)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0 x-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation encryption-test (added-strand init 4)
    (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
      (privk a)) (0 3))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha))
          (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-1
       (cat "Group id" group-1 (exp (gen) (mul x alpha-0 (rec x-0)))))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b-0)))
      (send
        (enc "final" (exp (gen) (mul y alpha))
          (exp (gen) (mul x alpha-0)) (privk a)))))
  (label 16)
  (parent 12)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig
  (vars (group group-0 text) (a b b-0 name)
    (group-dist group-dist-0 chan) (y alpha alpha-0 x rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x (mul (rec alpha) alpha-0 x)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (group group-0) (a a) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x)
    (y (mul y alpha (rec alpha-0))))
  (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (3 0)) ((3 1) (0 1))
    ((3 3) (0 3)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha alpha-0 x)
  (absent (y (mul (rec alpha) alpha-0 x)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation generalization weakened ((1 0) (3 0)))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul alpha-0 x))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha))
          (exp (gen) (mul alpha-0 x)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul alpha-0 x))
          (privk b-0)))
      (send
        (enc "final" (exp (gen) (mul y alpha))
          (exp (gen) (mul alpha-0 x)) (privk a)))))
  (label 17)
  (parent 15)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (y y) (x (mul (rec alpha) alpha-0 x))
        (g (exp (gen) alpha)) (group group) (group-dist group-dist))))
  (origs))

(comment "Nothing left to do")

(defprotocol dh_sig2 diffie-hellman
  (defrole group-init
    (vars (alpha rndx) (group text) (group-dist chan))
    (trace (send group-dist (cat "Group id" group (exp (gen) alpha))))
    (uniq-gen alpha)
    (conf group-dist))
  (defrole init
    (vars (x rndx) (y expt) (g base) (n group text) (a b name)
      (group-dist chan))
    (trace (recv group-dist (cat "Group id" group g))
      (send (enc (exp g x) (privk a)))
      (recv (enc (exp g y) (exp g x) (privk b)))
      (send (enc n (exp g (mul x y)))) (recv n))
    (uniq-gen n x)
    (auth group-dist))
  (defrole resp
    (vars (y rndx) (x expt) (g base) (n group text) (a b name)
      (group-dist chan))
    (trace (recv group-dist (cat "Group id" group g))
      (recv (enc (exp g x) (privk a)))
      (send (enc (exp g y) (exp g x) (privk b)))
      (recv (enc n (exp g (mul y x)))) (send n))
    (uniq-gen y)
    (absent (y x))
    (auth group-dist))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (g base) (group-dist chan) (x rndx)
    (y expt))
  (defstrand init 5 (n n) (group group) (a a) (b b) (g g)
    (group-dist group-dist) (x x) (y y))
  (non-orig (privk a) (privk b))
  (uniq-gen n x)
  (auth group-dist)
  (traces
    ((recv group-dist (cat "Group id" group g))
      (send (enc (exp g x) (privk a)))
      (recv (enc (exp g y) (exp g x) (privk b)))
      (send (enc n (exp g (mul x y)))) (recv n)))
  (label 18)
  (unrealized (0 0) (0 2))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (group-dist chan) (x rndx) (y expt)
    (alpha rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (precedes ((1 0) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n x alpha)
  (conf group-dist)
  (auth group-dist)
  (operation channel-test (added-strand group-init 1)
    (ch-msg group-dist (cat "Group id" group (exp (gen) alpha))) (0 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (send (enc n (exp (gen) (mul x y alpha))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha)))))
  (label 19)
  (parent 18)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (alpha x y rndx) (x-0 expt))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x)
    (y (mul x y (rec x-0))))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) (mul alpha x (rec x-0)))) (group-dist group-dist-0)
    (y y) (x x-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y)
  (absent (y x-0))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation encryption-test (added-strand resp 3)
    (enc (exp (gen) (mul alpha x y (rec x-0))) (exp (gen) (mul alpha x))
      (privk b)) (0 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul alpha x y (rec x-0)))
          (exp (gen) (mul alpha x)) (privk b)))
      (send (enc n (exp (gen) (mul alpha x x y (rec x-0))))) (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0
       (cat "Group id" group-0 (exp (gen) (mul alpha x (rec x-0)))))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul alpha x y (rec x-0)))
          (exp (gen) (mul alpha x)) (privk b)))))
  (label 20)
  (parent 19)
  (unrealized (0 4) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 name) (group-dist chan)
    (y x alpha rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation channel-test (displaced 3 1 group-init 1)
    (ch-msg group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
    (2 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))))
  (label 21)
  (parent 20)
  (unrealized (0 4))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (y alpha x alpha-0 rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x)
    (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (y y)
    (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((3 0) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0)
  (absent (y (mul alpha x (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation channel-test (added-strand group-init 1)
    (ch-msg group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
    (2 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha-0))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 22)
  (parent 20)
  (unrealized (0 4))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a a-0 b name) (group-dist chan)
    (alpha x y rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 5 (n n) (group group) (a a-0) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (precedes ((0 1) (2 0)) ((0 3) (2 3)) ((1 0) (0 0)) ((2 2) (0 2))
    ((2 4) (0 4)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test (displaced 2 3 resp 5) n (0 4)
    (enc n (exp (gen) (mul y-0 x-0 alpha))))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk b))) (send (enc n (exp (gen) (mul alpha x y))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk b))) (recv (enc n (exp (gen) (mul alpha x y))))
      (send n)))
  (label 23)
  (parent 21)
  (realized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 a-1 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha y-0 rndx) (x-0 expt))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (defstrand resp 5 (n n) (group group-0) (a a-1) (b b-0)
    (g (exp (gen) (mul y x alpha (rec y-0) (rec x-0))))
    (group-dist group-dist-0) (y y-0) (x x-0))
  (precedes ((0 1) (2 0)) ((0 3) (3 3)) ((1 0) (0 0)) ((2 2) (0 2))
    ((2 2) (3 0)) ((3 4) (0 4)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha y-0)
  (absent (y x) (y-0 x-0))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation nonce-test (added-strand resp 5) n (0 4)
    (enc n (exp (gen) (mul y x alpha))))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))))
    ((recv group-dist-0
       (cat "Group id" group-0
         (exp (gen) (mul y x alpha (rec y-0) (rec x-0)))))
      (recv (enc (exp (gen) (mul y x alpha (rec y-0))) (privk a-1)))
      (send
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul y x alpha (rec y-0))) (privk b-0)))
      (recv (enc n (exp (gen) (mul y x alpha)))) (send n)))
  (label 24)
  (parent 21)
  (unrealized (3 0) (3 1))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 name) (group-dist chan)
    (y x alpha rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((2 2) (3 0))
    ((3 1) (0 4)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test (added-listener (exp (gen) (mul y x alpha))) n
    (0 4) (enc n (exp (gen) (mul y x alpha))))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))))
    ((recv (exp (gen) (mul y x alpha)))
      (send (exp (gen) (mul y x alpha)))))
  (label 25)
  (parent 21)
  (unrealized (3 0))
  (comment "5 in cohort - 5 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 a-1 b-0 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (y alpha x alpha-0 y-0 rndx) (x-0 expt))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x)
    (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (y y)
    (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand resp 5 (n n) (group group-1) (a a-1) (b b-0)
    (g (exp (gen) (mul y x alpha-0 (rec y-0) (rec x-0))))
    (group-dist group-dist-1) (y y-0) (x x-0))
  (precedes ((0 1) (2 0)) ((0 3) (4 3)) ((1 0) (0 0)) ((2 2) (0 2))
    ((2 2) (4 0)) ((3 0) (2 0)) ((4 4) (0 4)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0 y-0)
  (absent (y (mul alpha x (rec alpha-0))) (y-0 x-0))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand resp 5) n (0 4)
    (enc n (exp (gen) (mul y x alpha-0))))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha-0))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-1
       (cat "Group id" group-1
         (exp (gen) (mul y x alpha-0 (rec y-0) (rec x-0)))))
      (recv (enc (exp (gen) (mul y x alpha-0 (rec y-0))) (privk a-1)))
      (send
        (enc (exp (gen) (mul y x alpha-0 (rec x-0)))
          (exp (gen) (mul y x alpha-0 (rec y-0))) (privk b-0)))
      (recv (enc n (exp (gen) (mul y x alpha-0)))) (send n)))
  (label 26)
  (parent 22)
  (unrealized (4 0) (4 1))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (y alpha x alpha-0 rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x)
    (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (y y)
    (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (exp (gen) (mul y x alpha-0)))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((2 2) (4 0))
    ((3 0) (2 0)) ((4 1) (0 4)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0)
  (absent (y (mul alpha x (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test (added-listener (exp (gen) (mul y x alpha-0))) n
    (0 4) (enc n (exp (gen) (mul y x alpha-0))))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha-0))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (exp (gen) (mul y x alpha-0)))
      (send (exp (gen) (mul y x alpha-0)))))
  (label 27)
  (parent 22)
  (unrealized (4 0))
  (comment "5 in cohort - 5 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a a-0 b name) (group-dist chan)
    (alpha x y rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 5 (n n) (group group) (a a-0) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (precedes ((0 1) (2 1)) ((0 3) (2 3)) ((1 0) (0 0)) ((1 0) (2 0))
    ((2 2) (0 2)) ((2 4) (0 4)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation generalization weakened ((0 1) (2 0)))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk b))) (send (enc n (exp (gen) (mul alpha x y))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk b))) (recv (enc n (exp (gen) (mul alpha x y))))
      (send n)))
  (label 28)
  (parent 23)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (x x) (y y) (g (exp (gen) alpha)) (n n) (group group)
        (group-dist group-dist))))
  (origs))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 a-1 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha y-0 rndx) (x-0 expt))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (defstrand resp 3 (group group-0) (a a-1) (b b-0)
    (g (exp (gen) (mul y x alpha (rec y-0)))) (group-dist group-dist-0)
    (y y-0) (x x-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((2 2) (4 0))
    ((3 1) (0 4)) ((4 2) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha y-0)
  (absent (y x) (y-0 x-0))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation nonce-test (added-strand resp 3)
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))))
    ((recv (exp (gen) (mul y x alpha)))
      (send (exp (gen) (mul y x alpha))))
    ((recv group-dist-0
       (cat "Group id" group-0 (exp (gen) (mul y x alpha (rec y-0)))))
      (recv (enc (exp (gen) (mul y x alpha (rec y-0) x-0)) (privk a-1)))
      (send
        (enc (exp (gen) (mul y x alpha))
          (exp (gen) (mul y x alpha (rec y-0) x-0)) (privk b-0)))))
  (label 29)
  (parent 25)
  (unrealized (4 0) (4 1))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 a-1 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (defstrand init 2 (group group-0) (a a-1)
    (g (exp (gen) (mul y x alpha (rec x-0)))) (group-dist group-dist-0)
    (x x-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((2 2) (4 0))
    ((3 1) (0 4)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0)
  (absent (y x))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation nonce-test (added-strand init 2)
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))))
    ((recv (exp (gen) (mul y x alpha)))
      (send (exp (gen) (mul y x alpha))))
    ((recv group-dist-0
       (cat "Group id" group-0 (exp (gen) (mul y x alpha (rec x-0)))))
      (send (enc (exp (gen) (mul y x alpha)) (privk a-1)))))
  (label 30)
  (parent 25)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 name) (group-dist chan)
    (y x alpha rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (deflistener (cat (exp (gen) (mul y x)) alpha))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((2 2) (4 0))
    ((3 1) (0 4)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x)) alpha))
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))))
    ((recv (exp (gen) (mul y x alpha)))
      (send (exp (gen) (mul y x alpha))))
    ((recv (cat (exp (gen) (mul y x)) alpha))
      (send (cat (exp (gen) (mul y x)) alpha))))
  (label 31)
  (parent 25)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 name) (group-dist chan)
    (y x alpha rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (deflistener (cat (exp (gen) (mul y alpha)) x))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((2 2) (4 0))
    ((3 1) (0 4)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha)) x))
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))))
    ((recv (exp (gen) (mul y x alpha)))
      (send (exp (gen) (mul y x alpha))))
    ((recv (cat (exp (gen) (mul y alpha)) x))
      (send (cat (exp (gen) (mul y alpha)) x))))
  (label 32)
  (parent 25)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 name) (group-dist chan)
    (y x alpha rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (group-dist group-dist) (y y) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (deflistener (cat (exp (gen) (mul x alpha)) y))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((2 2) (4 0))
    ((3 1) (0 4)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x alpha)) y))
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))))
    ((recv (exp (gen) (mul y x alpha)))
      (send (exp (gen) (mul y x alpha))))
    ((recv (cat (exp (gen) (mul x alpha)) y))
      (send (cat (exp (gen) (mul x alpha)) y))))
  (label 33)
  (parent 25)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 a-1 b-0 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (y alpha x alpha-0 y-0 rndx) (x-0 expt))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x)
    (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (y y)
    (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (exp (gen) (mul y x alpha-0)))
  (defstrand resp 3 (group group-1) (a a-1) (b b-0)
    (g (exp (gen) (mul y x alpha-0 (rec y-0))))
    (group-dist group-dist-1) (y y-0) (x x-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((2 2) (5 0))
    ((3 0) (2 0)) ((4 1) (0 4)) ((5 2) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0 y-0)
  (absent (y (mul alpha x (rec alpha-0))) (y-0 x-0))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand resp 3)
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha-0))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (exp (gen) (mul y x alpha-0)))
      (send (exp (gen) (mul y x alpha-0))))
    ((recv group-dist-1
       (cat "Group id" group-1 (exp (gen) (mul y x alpha-0 (rec y-0)))))
      (recv
        (enc (exp (gen) (mul y x alpha-0 (rec y-0) x-0)) (privk a-1)))
      (send
        (enc (exp (gen) (mul y x alpha-0))
          (exp (gen) (mul y x alpha-0 (rec y-0) x-0)) (privk b-0)))))
  (label 34)
  (parent 27)
  (unrealized (5 0) (5 1))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 a-1 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (y alpha x alpha-0 x-0 rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x)
    (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (y y)
    (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (exp (gen) (mul y x alpha-0)))
  (defstrand init 2 (group group-1) (a a-1)
    (g (exp (gen) (mul y x alpha-0 (rec x-0))))
    (group-dist group-dist-1) (x x-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((2 2) (5 0))
    ((3 0) (2 0)) ((4 1) (0 4)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0 x-0)
  (absent (y (mul alpha x (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand init 2)
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha-0))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (exp (gen) (mul y x alpha-0)))
      (send (exp (gen) (mul y x alpha-0))))
    ((recv group-dist-1
       (cat "Group id" group-1 (exp (gen) (mul y x alpha-0 (rec x-0)))))
      (send (enc (exp (gen) (mul y x alpha-0)) (privk a-1)))))
  (label 35)
  (parent 27)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (y alpha x alpha-0 rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x)
    (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (y y)
    (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (exp (gen) (mul y x alpha-0)))
  (deflistener (cat (exp (gen) (mul y x)) alpha-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((2 2) (5 0))
    ((3 0) (2 0)) ((4 1) (0 4)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0)
  (absent (y (mul alpha x (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x)) alpha-0))
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha-0))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (exp (gen) (mul y x alpha-0)))
      (send (exp (gen) (mul y x alpha-0))))
    ((recv (cat (exp (gen) (mul y x)) alpha-0))
      (send (cat (exp (gen) (mul y x)) alpha-0))))
  (label 36)
  (parent 27)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (y alpha x alpha-0 rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x)
    (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (y y)
    (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (exp (gen) (mul y x alpha-0)))
  (deflistener (cat (exp (gen) (mul y alpha-0)) x))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((2 2) (5 0))
    ((3 0) (2 0)) ((4 1) (0 4)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0)
  (absent (y (mul alpha x (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha-0)) x))
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha-0))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (exp (gen) (mul y x alpha-0)))
      (send (exp (gen) (mul y x alpha-0))))
    ((recv (cat (exp (gen) (mul y alpha-0)) x))
      (send (cat (exp (gen) (mul y alpha-0)) x))))
  (label 37)
  (parent 27)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (y alpha x alpha-0 rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x)
    (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (y y)
    (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (exp (gen) (mul y x alpha-0)))
  (deflistener (cat (exp (gen) (mul x alpha-0)) y))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((2 2) (5 0))
    ((3 0) (2 0)) ((4 1) (0 4)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0)
  (absent (y (mul alpha x (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x alpha-0)) y))
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))) (send (enc n (exp (gen) (mul y x alpha-0))))
      (recv n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
          (privk b))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (exp (gen) (mul y x alpha-0)))
      (send (exp (gen) (mul y x alpha-0))))
    ((recv (cat (exp (gen) (mul x alpha-0)) y))
      (send (cat (exp (gen) (mul x alpha-0)) y))))
  (label 38)
  (parent 27)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol dh_sig2 diffie-hellman
  (defrole group-init
    (vars (alpha rndx) (group text) (group-dist chan))
    (trace (send group-dist (cat "Group id" group (exp (gen) alpha))))
    (uniq-gen alpha)
    (conf group-dist))
  (defrole init
    (vars (x rndx) (y expt) (g base) (n group text) (a b name)
      (group-dist chan))
    (trace (recv group-dist (cat "Group id" group g))
      (send (enc (exp g x) (privk a)))
      (recv (enc (exp g y) (exp g x) (privk b)))
      (send (enc n (exp g (mul x y)))) (recv n))
    (uniq-gen n x)
    (auth group-dist))
  (defrole resp
    (vars (y rndx) (x expt) (g base) (n group text) (a b name)
      (group-dist chan))
    (trace (recv group-dist (cat "Group id" group g))
      (recv (enc (exp g x) (privk a)))
      (send (enc (exp g y) (exp g x) (privk b)))
      (recv (enc n (exp g (mul y x)))) (send n))
    (uniq-gen y)
    (absent (y x))
    (auth group-dist))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (g base) (group-dist chan) (y rndx)
    (x expt))
  (defstrand resp 5 (n n) (group group) (a a) (b b) (g g)
    (group-dist group-dist) (y y) (x x))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (absent (y x))
  (auth group-dist)
  (traces
    ((recv group-dist (cat "Group id" group g))
      (recv (enc (exp g x) (privk a)))
      (send (enc (exp g y) (exp g x) (privk b)))
      (recv (enc n (exp g (mul y x)))) (send n)))
  (label 39)
  (unrealized (0 0) (0 1))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (group-dist chan) (y rndx) (x expt)
    (alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (precedes ((1 0) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation channel-test (added-strand group-init 1)
    (ch-msg group-dist (cat "Group id" group (exp (gen) alpha))) (0 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha)))))
  (label 40)
  (parent 39)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b name) (group-dist group-dist-0 chan)
    (y rndx) (x expt) (alpha x-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a)
    (g (exp (gen) (mul x alpha (rec x-0)))) (group-dist group-dist-0)
    (x x-0))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x-0)
  (absent (y x))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation encryption-test (added-strand init 2)
    (enc (exp (gen) (mul x alpha)) (privk a)) (0 1))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0
       (cat "Group id" group-0 (exp (gen) (mul x alpha (rec x-0)))))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))))
  (label 41)
  (parent 40)
  (unrealized (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (group-dist chan) (y x alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation channel-test (displaced 3 1 group-init 1)
    (ch-msg group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
    (2 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))))
  (label 42)
  (parent 41)
  (unrealized (0 3))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b name) (group-dist group-dist-0 chan)
    (y alpha x alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1)) ((3 0) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation channel-test (added-strand group-init 1)
    (ch-msg group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
    (2 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 43)
  (parent 41)
  (unrealized (0 3))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (b a b-0 name) (group-dist chan)
    (alpha y x rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 4 (n n) (group group) (a a) (b b-0)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
  (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((2 3) (0 3)))
  (non-orig (privk b) (privk a))
  (uniq-gen n alpha y x)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation encryption-test (displaced 2 3 init 4)
    (enc n (exp (gen) (mul y-0 x-0 alpha))) (0 3))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk b))) (recv (enc n (exp (gen) (mul alpha y x))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
          (privk b-0))) (send (enc n (exp (gen) (mul alpha y x))))))
  (label 44)
  (parent 42)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (y y) (x x) (g (exp (gen) alpha)) (n n) (group group)
        (group-dist group-dist))))
  (origs))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 rndx) (y-0 expt))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) (mul y x alpha (rec x-0) (rec y-0))))
    (group-dist group-dist-0) (x x-0) (y y-0))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 3) (0 3)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0)
  (absent (y x))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation encryption-test (added-strand init 4)
    (enc n (exp (gen) (mul y x alpha))) (0 3))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist-0
       (cat "Group id" group-0
         (exp (gen) (mul y x alpha (rec x-0) (rec y-0)))))
      (send (enc (exp (gen) (mul y x alpha (rec y-0))) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul y x alpha (rec y-0))) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha))))))
  (label 45)
  (parent 42)
  (unrealized (3 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (group-dist chan) (y x alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (0 3)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation encryption-test
    (added-listener (exp (gen) (mul y x alpha)))
    (enc n (exp (gen) (mul y x alpha))) (0 3))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv (exp (gen) (mul y x alpha)))
      (send (exp (gen) (mul y x alpha)))))
  (label 46)
  (parent 42)
  (unrealized (3 0))
  (comment "5 in cohort - 5 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (b a b-0 name)
    (group-dist group-dist-0 chan) (alpha alpha-0 y x rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) alpha-0 x)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x) (y y))
  (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (3 0))
    ((3 1) (0 1)) ((3 3) (0 3)))
  (non-orig (privk b) (privk a))
  (uniq-gen n alpha alpha-0 y x)
  (absent (y (mul (rec alpha) alpha-0 x)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation encryption-test (displaced 2 4 init 4)
    (enc n (exp (gen) (mul y-0 x-0 alpha-0))) (0 3))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha-0 x))
          (privk b))) (recv (enc n (exp (gen) (mul alpha-0 y x))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (recv
        (enc (exp (gen) (mul alpha-0 y)) (exp (gen) (mul alpha-0 x))
          (privk b-0))) (send (enc n (exp (gen) (mul alpha-0 y x))))))
  (label 47)
  (parent 43)
  (unrealized (3 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (y alpha x alpha-0 x-0 rndx) (y-0 expt))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) (mul y x alpha-0 (rec x-0) (rec y-0))))
    (group-dist group-dist-1) (x x-0) (y y-0))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 3) (0 3)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0 x-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation encryption-test (added-strand init 4)
    (enc n (exp (gen) (mul y x alpha-0))) (0 3))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-1
       (cat "Group id" group-1
         (exp (gen) (mul y x alpha-0 (rec x-0) (rec y-0)))))
      (send (enc (exp (gen) (mul y x alpha-0 (rec y-0))) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha-0 (rec x-0)))
          (exp (gen) (mul y x alpha-0 (rec y-0))) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0))))))
  (label 48)
  (parent 43)
  (unrealized (4 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b name) (group-dist group-dist-0 chan)
    (y alpha x alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (exp (gen) (mul y x alpha-0)))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (0 3)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation encryption-test
    (added-listener (exp (gen) (mul y x alpha-0)))
    (enc n (exp (gen) (mul y x alpha-0))) (0 3))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (exp (gen) (mul y x alpha-0)))
      (send (exp (gen) (mul y x alpha-0)))))
  (label 49)
  (parent 43)
  (unrealized (4 0))
  (comment "5 in cohort - 5 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 b-0 name) (group-dist chan)
    (y x x-0 alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x-0)
    (y (mul y x (rec x-0))))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 3) (0 3)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x x-0 alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation channel-test (displaced 4 1 group-init 1)
    (ch-msg group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
    (3 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x-0 alpha)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha))
          (exp (gen) (mul x-0 alpha)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha))))))
  (label 50)
  (parent 45)
  (unrealized (3 2))
  (comment "6 in cohort - 6 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 3) (0 3)) ((4 0) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0)
  (absent (y x))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation channel-test (added-strand group-init 1)
    (ch-msg group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
    (3 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 51)
  (parent 45)
  (unrealized (3 2))
  (comment "6 in cohort - 6 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha y-0 rndx) (x-0 expt))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (defstrand resp 3 (group group-0) (a a-0) (b b-0)
    (g (exp (gen) (mul y x alpha (rec y-0)))) (group-dist group-dist-0)
    (y y-0) (x x-0))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (0 3)) ((4 2) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha y-0)
  (absent (y x) (y-0 x-0))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation nonce-test (added-strand resp 3)
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv (exp (gen) (mul y x alpha)))
      (send (exp (gen) (mul y x alpha))))
    ((recv group-dist-0
       (cat "Group id" group-0 (exp (gen) (mul y x alpha (rec y-0)))))
      (recv (enc (exp (gen) (mul y x alpha (rec y-0) x-0)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y x alpha))
          (exp (gen) (mul y x alpha (rec y-0) x-0)) (privk b-0)))))
  (label 52)
  (parent 46)
  (unrealized (4 0) (4 1))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (defstrand init 2 (group group-0) (a a-0)
    (g (exp (gen) (mul y x alpha (rec x-0)))) (group-dist group-dist-0)
    (x x-0))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (0 3)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha x-0)
  (absent (y x))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation nonce-test (added-strand init 2)
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv (exp (gen) (mul y x alpha)))
      (send (exp (gen) (mul y x alpha))))
    ((recv group-dist-0
       (cat "Group id" group-0 (exp (gen) (mul y x alpha (rec x-0)))))
      (send (enc (exp (gen) (mul y x alpha)) (privk a-0)))))
  (label 53)
  (parent 46)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (group-dist chan) (y x alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (deflistener (cat (exp (gen) (mul y x)) alpha))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (0 3)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x)) alpha))
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv (exp (gen) (mul y x alpha)))
      (send (exp (gen) (mul y x alpha))))
    ((recv (cat (exp (gen) (mul y x)) alpha))
      (send (cat (exp (gen) (mul y x)) alpha))))
  (label 54)
  (parent 46)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (group-dist chan) (y x alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (deflistener (cat (exp (gen) (mul y alpha)) x))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (0 3)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha)) x))
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv (exp (gen) (mul y x alpha)))
      (send (exp (gen) (mul y x alpha))))
    ((recv (cat (exp (gen) (mul y alpha)) x))
      (send (cat (exp (gen) (mul y alpha)) x))))
  (label 55)
  (parent 46)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (group-dist chan) (y x alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (deflistener (cat (exp (gen) (mul x alpha)) y))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (0 3)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x alpha)) y))
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv (exp (gen) (mul y x alpha)))
      (send (exp (gen) (mul y x alpha))))
    ((recv (cat (exp (gen) (mul x alpha)) y))
      (send (cat (exp (gen) (mul x alpha)) y))))
  (label 56)
  (parent 46)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (b a b-0 a-0 b-1 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (alpha alpha-0 y x y-0 rndx) (x-0 expt))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) alpha-0 x)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x) (y y))
  (defstrand resp 3 (group group-1) (a a-0) (b b-1)
    (g (exp (gen) (mul alpha-0 y (rec y-0)))) (group-dist group-dist-1)
    (y y-0) (x x-0))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (3 0))
    ((3 1) (0 1)) ((3 3) (0 3)) ((4 2) (3 2)))
  (non-orig (privk b) (privk a))
  (uniq-gen n alpha alpha-0 y x y-0)
  (absent (y (mul (rec alpha) alpha-0 x)) (y-0 x-0))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand resp 3)
    (exp (gen) (mul alpha-0 y)) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha-0 x))
          (privk b))) (recv (enc n (exp (gen) (mul alpha-0 y x))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (recv
        (enc (exp (gen) (mul alpha-0 y)) (exp (gen) (mul alpha-0 x))
          (privk b-0))) (send (enc n (exp (gen) (mul alpha-0 y x)))))
    ((recv group-dist-1
       (cat "Group id" group-1 (exp (gen) (mul alpha-0 y (rec y-0)))))
      (recv (enc (exp (gen) (mul alpha-0 y (rec y-0) x-0)) (privk a-0)))
      (send
        (enc (exp (gen) (mul alpha-0 y))
          (exp (gen) (mul alpha-0 y (rec y-0) x-0)) (privk b-1)))))
  (label 57)
  (parent 47)
  (unrealized (4 0) (4 1))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (b a b-0 a-0 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (alpha alpha-0 y x x-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) alpha-0 x)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x) (y y))
  (defstrand init 2 (group group-1) (a a-0)
    (g (exp (gen) (mul alpha-0 y (rec x-0)))) (group-dist group-dist-1)
    (x x-0))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (3 0))
    ((3 1) (0 1)) ((3 3) (0 3)) ((4 1) (3 2)))
  (non-orig (privk b) (privk a))
  (uniq-gen n alpha alpha-0 y x x-0)
  (absent (y (mul (rec alpha) alpha-0 x)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand init 2)
    (exp (gen) (mul alpha-0 y)) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha-0 x))
          (privk b))) (recv (enc n (exp (gen) (mul alpha-0 y x))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (recv
        (enc (exp (gen) (mul alpha-0 y)) (exp (gen) (mul alpha-0 x))
          (privk b-0))) (send (enc n (exp (gen) (mul alpha-0 y x)))))
    ((recv group-dist-1
       (cat "Group id" group-1 (exp (gen) (mul alpha-0 y (rec x-0)))))
      (send (enc (exp (gen) (mul alpha-0 y)) (privk a-0)))))
  (label 58)
  (parent 47)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (b a b-0 name)
    (group-dist group-dist-0 chan) (alpha alpha-0 y x rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) alpha-0 x)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x) (y y))
  (deflistener (cat (exp (gen) alpha-0) y))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (3 0))
    ((3 1) (0 1)) ((3 3) (0 3)) ((4 1) (3 2)))
  (non-orig (privk b) (privk a))
  (uniq-gen n alpha alpha-0 y x)
  (absent (y (mul (rec alpha) alpha-0 x)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test (added-listener (cat (exp (gen) alpha-0) y))
    (exp (gen) (mul alpha-0 y)) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha-0 x))
          (privk b))) (recv (enc n (exp (gen) (mul alpha-0 y x))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (recv
        (enc (exp (gen) (mul alpha-0 y)) (exp (gen) (mul alpha-0 x))
          (privk b-0))) (send (enc n (exp (gen) (mul alpha-0 y x)))))
    ((recv (cat (exp (gen) alpha-0) y))
      (send (cat (exp (gen) alpha-0) y))))
  (label 59)
  (parent 47)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (b a b-0 name)
    (group-dist group-dist-0 chan) (alpha alpha-0 y x rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) alpha-0 x)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x) (y y))
  (deflistener (cat (exp (gen) y) alpha-0))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (3 0))
    ((3 1) (0 1)) ((3 3) (0 3)) ((4 1) (3 2)))
  (non-orig (privk b) (privk a))
  (uniq-gen n alpha alpha-0 y x)
  (absent (y (mul (rec alpha) alpha-0 x)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test (added-listener (cat (exp (gen) y) alpha-0))
    (exp (gen) (mul alpha-0 y)) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha-0 x))
          (privk b))) (recv (enc n (exp (gen) (mul alpha-0 y x))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (recv
        (enc (exp (gen) (mul alpha-0 y)) (exp (gen) (mul alpha-0 x))
          (privk b-0))) (send (enc n (exp (gen) (mul alpha-0 y x)))))
    ((recv (cat (exp (gen) y) alpha-0))
      (send (cat (exp (gen) y) alpha-0))))
  (label 60)
  (parent 47)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (y y)
    (x (mul x alpha (rec alpha-0))))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha-0))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 3) (0 3)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0)
  (absent (y (mul x alpha (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation channel-test (displaced 5 1 group-init 1)
    (ch-msg group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1)))
    (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha))))))
  (label 61)
  (parent 48)
  (unrealized (4 2))
  (comment "6 in cohort - 6 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (alpha y x x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x (rec x-0))))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 3) (0 3)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x x-0 alpha-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation channel-test (displaced 5 3 group-init 1)
    (ch-msg group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1)))
    (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha-0))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0))))))
  (label 62)
  (parent 48)
  (unrealized (4 2))
  (comment "6 in cohort - 6 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (alpha y x alpha-0 x-0 alpha-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) alpha-1)) (group-dist group-dist-1) (x x-0)
    (y (mul y x alpha-0 (rec x-0) (rec alpha-1))))
  (defstrand group-init 1 (group group-1) (group-dist group-dist-1)
    (alpha alpha-1))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 3) (0 3)) ((5 0) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x alpha-0 x-0 alpha-1)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0 group-dist-1)
  (auth group-dist group-dist-0 group-dist-1)
  (operation channel-test (added-strand group-init 1)
    (ch-msg group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1)))
    (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1)))
      (send (enc (exp (gen) (mul x-0 alpha-1)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha-0 (rec x-0)))
          (exp (gen) (mul x-0 alpha-1)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((send group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1)))))
  (label 63)
  (parent 48)
  (unrealized (4 2))
  (comment "6 in cohort - 6 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (y alpha x alpha-0 y-0 rndx) (x-0 expt))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (exp (gen) (mul y x alpha-0)))
  (defstrand resp 3 (group group-1) (a a-0) (b b-0)
    (g (exp (gen) (mul y x alpha-0 (rec y-0))))
    (group-dist group-dist-1) (y y-0) (x x-0))
  (precedes ((0 2) (5 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (0 3)) ((5 2) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0 y-0)
  (absent (y (mul (rec alpha) x alpha-0)) (y-0 x-0))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand resp 3)
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (exp (gen) (mul y x alpha-0)))
      (send (exp (gen) (mul y x alpha-0))))
    ((recv group-dist-1
       (cat "Group id" group-1 (exp (gen) (mul y x alpha-0 (rec y-0)))))
      (recv
        (enc (exp (gen) (mul y x alpha-0 (rec y-0) x-0)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y x alpha-0))
          (exp (gen) (mul y x alpha-0 (rec y-0) x-0)) (privk b-0)))))
  (label 64)
  (parent 49)
  (unrealized (5 0) (5 1))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (y alpha x alpha-0 x-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (exp (gen) (mul y x alpha-0)))
  (defstrand init 2 (group group-1) (a a-0)
    (g (exp (gen) (mul y x alpha-0 (rec x-0))))
    (group-dist group-dist-1) (x x-0))
  (precedes ((0 2) (5 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (0 3)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0 x-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand init 2)
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (exp (gen) (mul y x alpha-0)))
      (send (exp (gen) (mul y x alpha-0))))
    ((recv group-dist-1
       (cat "Group id" group-1 (exp (gen) (mul y x alpha-0 (rec x-0)))))
      (send (enc (exp (gen) (mul y x alpha-0)) (privk a-0)))))
  (label 65)
  (parent 49)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b name) (group-dist group-dist-0 chan)
    (y alpha x alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (exp (gen) (mul y x alpha-0)))
  (deflistener (cat (exp (gen) (mul y x)) alpha-0))
  (precedes ((0 2) (5 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (0 3)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x)) alpha-0))
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (exp (gen) (mul y x alpha-0)))
      (send (exp (gen) (mul y x alpha-0))))
    ((recv (cat (exp (gen) (mul y x)) alpha-0))
      (send (cat (exp (gen) (mul y x)) alpha-0))))
  (label 66)
  (parent 49)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b name) (group-dist group-dist-0 chan)
    (y alpha x alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (exp (gen) (mul y x alpha-0)))
  (deflistener (cat (exp (gen) (mul y alpha-0)) x))
  (precedes ((0 2) (5 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (0 3)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha-0)) x))
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (exp (gen) (mul y x alpha-0)))
      (send (exp (gen) (mul y x alpha-0))))
    ((recv (cat (exp (gen) (mul y alpha-0)) x))
      (send (cat (exp (gen) (mul y alpha-0)) x))))
  (label 67)
  (parent 49)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b name) (group-dist group-dist-0 chan)
    (y alpha x alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (exp (gen) (mul y x alpha-0)))
  (deflistener (cat (exp (gen) (mul x alpha-0)) y))
  (precedes ((0 2) (5 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (0 3)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x alpha-0)) y))
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (exp (gen) (mul y x alpha-0)))
      (send (exp (gen) (mul y x alpha-0))))
    ((recv (cat (exp (gen) (mul x alpha-0)) y))
      (send (cat (exp (gen) (mul x alpha-0)) y))))
  (label 68)
  (parent 49)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 b-0 name) (group-dist chan)
    (y x x-0 alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x-0)
    (y (mul y x (rec x-0))))
  (deflistener (cat (exp (gen) (mul y x (rec x-0))) alpha))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 3) (0 3)) ((4 1) (3 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x x-0 alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x (rec x-0))) alpha))
    (exp (gen) (mul y x (rec x-0) alpha)) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x-0 alpha)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha))
          (exp (gen) (mul x-0 alpha)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((recv (cat (exp (gen) (mul y x (rec x-0))) alpha))
      (send (cat (exp (gen) (mul y x (rec x-0))) alpha))))
  (label 69)
  (parent 50)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 a-1 b-1 name)
    (group-dist group-dist-0 chan) (y x x-0 alpha y-0 rndx) (x-1 expt))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x-0)
    (y (mul y x (rec x-0))))
  (defstrand resp 3 (group group-0) (a a-1) (b b-1)
    (g (exp (gen) (mul y x (rec x-0) alpha (rec y-0))))
    (group-dist group-dist-0) (y y-0) (x x-1))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 3) (0 3)) ((4 2) (3 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x x-0 alpha y-0)
  (absent (y x) (y-0 x-1))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation nonce-test (added-strand resp 3)
    (exp (gen) (mul y x (rec x-0) alpha)) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x-0 alpha)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha))
          (exp (gen) (mul x-0 alpha)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((recv group-dist-0
       (cat "Group id" group-0
         (exp (gen) (mul y x (rec x-0) alpha (rec y-0)))))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha (rec y-0) x-1))
          (privk a-1)))
      (send
        (enc (exp (gen) (mul y x (rec x-0) alpha))
          (exp (gen) (mul y x (rec x-0) alpha (rec y-0) x-1))
          (privk b-1)))))
  (label 70)
  (parent 50)
  (unrealized (4 0) (4 1))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 a-1 name)
    (group-dist group-dist-0 chan) (y x x-0 alpha x-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x-0)
    (y (mul y x (rec x-0))))
  (defstrand init 2 (group group-0) (a a-1)
    (g (exp (gen) (mul y x (rec x-0) alpha (rec x-1))))
    (group-dist group-dist-0) (x x-1))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 3) (0 3)) ((4 1) (3 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x x-0 alpha x-1)
  (absent (y x))
  (conf group-dist)
  (auth group-dist group-dist-0)
  (operation nonce-test (added-strand init 2)
    (exp (gen) (mul y x (rec x-0) alpha)) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x-0 alpha)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha))
          (exp (gen) (mul x-0 alpha)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((recv group-dist-0
       (cat "Group id" group-0
         (exp (gen) (mul y x (rec x-0) alpha (rec x-1)))))
      (send (enc (exp (gen) (mul y x (rec x-0) alpha)) (privk a-1)))))
  (label 71)
  (parent 50)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 b-0 name) (group-dist chan)
    (y x x-0 alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x-0)
    (y (mul y x (rec x-0))))
  (deflistener (cat (exp (gen) (mul y x alpha)) x-0))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 3) (0 3)) ((4 1) (3 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x x-0 alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x alpha)) x-0))
    (exp (gen) (mul y x (rec x-0) alpha)) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x-0 alpha)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha))
          (exp (gen) (mul x-0 alpha)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((recv (cat (exp (gen) (mul y x alpha)) x-0))
      (send (cat (exp (gen) (mul y x alpha)) x-0))))
  (label 72)
  (parent 50)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 b-0 name) (group-dist chan)
    (y x x-0 alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x-0)
    (y (mul y x (rec x-0))))
  (deflistener (cat (exp (gen) (mul y (rec x-0) alpha)) x))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 3) (0 3)) ((4 1) (3 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x x-0 alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y (rec x-0) alpha)) x))
    (exp (gen) (mul y x (rec x-0) alpha)) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x-0 alpha)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha))
          (exp (gen) (mul x-0 alpha)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((recv (cat (exp (gen) (mul y (rec x-0) alpha)) x))
      (send (cat (exp (gen) (mul y (rec x-0) alpha)) x))))
  (label 73)
  (parent 50)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 b-0 name) (group-dist chan)
    (y x x-0 alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha)) (group-dist group-dist) (x x-0)
    (y (mul y x (rec x-0))))
  (deflistener (cat (exp (gen) (mul x (rec x-0) alpha)) y))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 3) (0 3)) ((4 1) (3 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x x-0 alpha)
  (absent (y x))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x (rec x-0) alpha)) y))
    (exp (gen) (mul y x (rec x-0) alpha)) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x-0 alpha)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha))
          (exp (gen) (mul x-0 alpha)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((recv (cat (exp (gen) (mul x (rec x-0) alpha)) y))
      (send (cat (exp (gen) (mul x (rec x-0) alpha)) y))))
  (label 74)
  (parent 50)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (cat (exp (gen) (mul y x alpha)) x-0))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (5 0)) ((3 3) (0 3)) ((4 0) (3 0)) ((5 1) (3 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0)
  (absent (y x))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x alpha)) x-0))
    (exp (gen) (mul y x alpha (rec x-0))) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (cat (exp (gen) (mul y x alpha)) x-0))
      (send (cat (exp (gen) (mul y x alpha)) x-0))))
  (label 75)
  (parent 51)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 a-1 b-1 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (y x alpha x-0 alpha-0 y-0 rndx) (x-1 expt))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand resp 3 (group group-1) (a a-1) (b b-1)
    (g (exp (gen) (mul y x alpha (rec x-0) (rec y-0))))
    (group-dist group-dist-1) (y y-0) (x x-1))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (5 0)) ((3 3) (0 3)) ((4 0) (3 0)) ((5 2) (3 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0 y-0)
  (absent (y x) (y-0 x-1))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand resp 3)
    (exp (gen) (mul y x alpha (rec x-0))) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-1
       (cat "Group id" group-1
         (exp (gen) (mul y x alpha (rec x-0) (rec y-0)))))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0) (rec y-0) x-1))
          (privk a-1)))
      (send
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul y x alpha (rec x-0) (rec y-0) x-1))
          (privk b-1)))))
  (label 76)
  (parent 51)
  (unrealized (5 0) (5 1))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 a-1 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (y x alpha x-0 alpha-0 x-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 2 (group group-1) (a a-1)
    (g (exp (gen) (mul y x alpha (rec x-0) (rec x-1))))
    (group-dist group-dist-1) (x x-1))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (5 0)) ((3 3) (0 3)) ((4 0) (3 0)) ((5 1) (3 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0 x-1)
  (absent (y x))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand init 2)
    (exp (gen) (mul y x alpha (rec x-0))) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-1
       (cat "Group id" group-1
         (exp (gen) (mul y x alpha (rec x-0) (rec x-1)))))
      (send (enc (exp (gen) (mul y x alpha (rec x-0))) (privk a-1)))))
  (label 77)
  (parent 51)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (cat (exp (gen) (mul y x (rec x-0))) alpha))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (5 0)) ((3 3) (0 3)) ((4 0) (3 0)) ((5 1) (3 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0)
  (absent (y x))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x (rec x-0))) alpha))
    (exp (gen) (mul y x alpha (rec x-0))) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (cat (exp (gen) (mul y x (rec x-0))) alpha))
      (send (cat (exp (gen) (mul y x (rec x-0))) alpha))))
  (label 78)
  (parent 51)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (cat (exp (gen) (mul y alpha (rec x-0))) x))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (5 0)) ((3 3) (0 3)) ((4 0) (3 0)) ((5 1) (3 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0)
  (absent (y x))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha (rec x-0))) x))
    (exp (gen) (mul y x alpha (rec x-0))) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (cat (exp (gen) (mul y alpha (rec x-0))) x))
      (send (cat (exp (gen) (mul y alpha (rec x-0))) x))))
  (label 79)
  (parent 51)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha))
    (group-dist group-dist) (x x))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (deflistener (cat (exp (gen) (mul x alpha (rec x-0))) y))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 1) (5 0)) ((3 3) (0 3)) ((4 0) (3 0)) ((5 1) (3 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0)
  (absent (y x))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x alpha (rec x-0))) y))
    (exp (gen) (mul y x alpha (rec x-0))) (3 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (cat (exp (gen) (mul x alpha (rec x-0))) y))
      (send (cat (exp (gen) (mul x alpha (rec x-0))) y))))
  (label 80)
  (parent 51)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (y y)
    (x (mul x alpha (rec alpha-0))))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha-0))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (deflistener (cat (exp (gen) (mul y x alpha)) x-0))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (5 0)) ((4 3) (0 3)) ((5 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0)
  (absent (y (mul x alpha (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x alpha)) x-0))
    (exp (gen) (mul y x alpha (rec x-0))) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((recv (cat (exp (gen) (mul y x alpha)) x-0))
      (send (cat (exp (gen) (mul y x alpha)) x-0))))
  (label 81)
  (parent 61)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 a-1 b-1 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (y x alpha x-0 alpha-0 y-0 rndx) (x-1 expt))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (y y)
    (x (mul x alpha (rec alpha-0))))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha-0))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (defstrand resp 3 (group group-1) (a a-1) (b b-1)
    (g (exp (gen) (mul y x alpha (rec x-0) (rec y-0))))
    (group-dist group-dist-1) (y y-0) (x x-1))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (5 0)) ((4 3) (0 3)) ((5 2) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0 y-0)
  (absent (y (mul x alpha (rec alpha-0))) (y-0 x-1))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand resp 3)
    (exp (gen) (mul y x alpha (rec x-0))) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((recv group-dist-1
       (cat "Group id" group-1
         (exp (gen) (mul y x alpha (rec x-0) (rec y-0)))))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0) (rec y-0) x-1))
          (privk a-1)))
      (send
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul y x alpha (rec x-0) (rec y-0) x-1))
          (privk b-1)))))
  (label 82)
  (parent 61)
  (unrealized (5 0) (5 1))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 a-1 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (y x alpha x-0 alpha-0 x-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (y y)
    (x (mul x alpha (rec alpha-0))))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha-0))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (defstrand init 2 (group group-1) (a a-1)
    (g (exp (gen) (mul y x alpha (rec x-0) (rec x-1))))
    (group-dist group-dist-1) (x x-1))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (5 0)) ((4 3) (0 3)) ((5 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0 x-1)
  (absent (y (mul x alpha (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand init 2)
    (exp (gen) (mul y x alpha (rec x-0))) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((recv group-dist-1
       (cat "Group id" group-1
         (exp (gen) (mul y x alpha (rec x-0) (rec x-1)))))
      (send (enc (exp (gen) (mul y x alpha (rec x-0))) (privk a-1)))))
  (label 83)
  (parent 61)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (y y)
    (x (mul x alpha (rec alpha-0))))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha-0))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (deflistener (cat (exp (gen) (mul y x (rec x-0))) alpha))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (5 0)) ((4 3) (0 3)) ((5 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0)
  (absent (y (mul x alpha (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x (rec x-0))) alpha))
    (exp (gen) (mul y x alpha (rec x-0))) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((recv (cat (exp (gen) (mul y x (rec x-0))) alpha))
      (send (cat (exp (gen) (mul y x (rec x-0))) alpha))))
  (label 84)
  (parent 61)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (y y)
    (x (mul x alpha (rec alpha-0))))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha-0))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (deflistener (cat (exp (gen) (mul y alpha (rec x-0))) x))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (5 0)) ((4 3) (0 3)) ((5 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0)
  (absent (y (mul x alpha (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha (rec x-0))) x))
    (exp (gen) (mul y x alpha (rec x-0))) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((recv (cat (exp (gen) (mul y alpha (rec x-0))) x))
      (send (cat (exp (gen) (mul y alpha (rec x-0))) x))))
  (label 85)
  (parent 61)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (y x alpha x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (y y)
    (x (mul x alpha (rec alpha-0))))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha-0))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha))
  (defstrand init 4 (n n) (group group) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist) (x x-0)
    (y (mul y x alpha (rec x-0) (rec alpha-0))))
  (deflistener (cat (exp (gen) (mul x alpha (rec x-0))) y))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (5 0)) ((4 3) (0 3)) ((5 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0 alpha-0)
  (absent (y (mul x alpha (rec alpha-0))))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x alpha (rec x-0))) y))
    (exp (gen) (mul y x alpha (rec x-0))) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul x alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha)))))
    ((recv (cat (exp (gen) (mul x alpha (rec x-0))) y))
      (send (cat (exp (gen) (mul x alpha (rec x-0))) y))))
  (label 86)
  (parent 61)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (alpha y x x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x (rec x-0))))
  (deflistener (cat (exp (gen) (mul y x (rec x-0))) alpha-0))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (5 0)) ((4 3) (0 3)) ((5 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x x-0 alpha-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x (rec x-0))) alpha-0))
    (exp (gen) (mul y x (rec x-0) alpha-0)) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha-0))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((recv (cat (exp (gen) (mul y x (rec x-0))) alpha-0))
      (send (cat (exp (gen) (mul y x (rec x-0))) alpha-0))))
  (label 87)
  (parent 62)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 a-1 b-1 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (alpha y x x-0 alpha-0 y-0 rndx) (x-1 expt))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x (rec x-0))))
  (defstrand resp 3 (group group-1) (a a-1) (b b-1)
    (g (exp (gen) (mul y x (rec x-0) alpha-0 (rec y-0))))
    (group-dist group-dist-1) (y y-0) (x x-1))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (5 0)) ((4 3) (0 3)) ((5 2) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x x-0 alpha-0 y-0)
  (absent (y (mul (rec alpha) x alpha-0)) (y-0 x-1))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand resp 3)
    (exp (gen) (mul y x (rec x-0) alpha-0)) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha-0))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((recv group-dist-1
       (cat "Group id" group-1
         (exp (gen) (mul y x (rec x-0) alpha-0 (rec y-0)))))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha-0 (rec y-0) x-1))
          (privk a-1)))
      (send
        (enc (exp (gen) (mul y x (rec x-0) alpha-0))
          (exp (gen) (mul y x (rec x-0) alpha-0 (rec y-0) x-1))
          (privk b-1)))))
  (label 88)
  (parent 62)
  (unrealized (5 0) (5 1))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 a-1 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (alpha y x x-0 alpha-0 x-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x (rec x-0))))
  (defstrand init 2 (group group-1) (a a-1)
    (g (exp (gen) (mul y x (rec x-0) alpha-0 (rec x-1))))
    (group-dist group-dist-1) (x x-1))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (5 0)) ((4 3) (0 3)) ((5 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x x-0 alpha-0 x-1)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test (added-strand init 2)
    (exp (gen) (mul y x (rec x-0) alpha-0)) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha-0))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((recv group-dist-1
       (cat "Group id" group-1
         (exp (gen) (mul y x (rec x-0) alpha-0 (rec x-1)))))
      (send (enc (exp (gen) (mul y x (rec x-0) alpha-0)) (privk a-1)))))
  (label 89)
  (parent 62)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (alpha y x x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x (rec x-0))))
  (deflistener (cat (exp (gen) (mul y x alpha-0)) x-0))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (5 0)) ((4 3) (0 3)) ((5 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x x-0 alpha-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x alpha-0)) x-0))
    (exp (gen) (mul y x (rec x-0) alpha-0)) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha-0))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((recv (cat (exp (gen) (mul y x alpha-0)) x-0))
      (send (cat (exp (gen) (mul y x alpha-0)) x-0))))
  (label 90)
  (parent 62)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (alpha y x x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x (rec x-0))))
  (deflistener (cat (exp (gen) (mul y (rec x-0) alpha-0)) x))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (5 0)) ((4 3) (0 3)) ((5 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x x-0 alpha-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y (rec x-0) alpha-0)) x))
    (exp (gen) (mul y x (rec x-0) alpha-0)) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha-0))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((recv (cat (exp (gen) (mul y (rec x-0) alpha-0)) x))
      (send (cat (exp (gen) (mul y (rec x-0) alpha-0)) x))))
  (label 91)
  (parent 62)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 chan) (alpha y x x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x-0)
    (y (mul y x (rec x-0))))
  (deflistener (cat (exp (gen) (mul x (rec x-0) alpha-0)) y))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (5 0)) ((4 3) (0 3)) ((5 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x x-0 alpha-0)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0)
  (auth group-dist group-dist-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x (rec x-0) alpha-0)) y))
    (exp (gen) (mul y x (rec x-0) alpha-0)) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x (rec x-0) alpha-0))
          (exp (gen) (mul x-0 alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((recv (cat (exp (gen) (mul x (rec x-0) alpha-0)) y))
      (send (cat (exp (gen) (mul x (rec x-0) alpha-0)) y))))
  (label 92)
  (parent 62)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (alpha y x alpha-0 x-0 alpha-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) alpha-1)) (group-dist group-dist-1) (x x-0)
    (y (mul y x alpha-0 (rec x-0) (rec alpha-1))))
  (defstrand group-init 1 (group group-1) (group-dist group-dist-1)
    (alpha alpha-1))
  (deflistener (cat (exp (gen) (mul y x alpha-0)) x-0))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (6 0)) ((4 3) (0 3)) ((5 0) (4 0))
    ((6 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x alpha-0 x-0 alpha-1)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0 group-dist-1)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x alpha-0)) x-0))
    (exp (gen) (mul y x alpha-0 (rec x-0))) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1)))
      (send (enc (exp (gen) (mul x-0 alpha-1)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha-0 (rec x-0)))
          (exp (gen) (mul x-0 alpha-1)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((send group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1))))
    ((recv (cat (exp (gen) (mul y x alpha-0)) x-0))
      (send (cat (exp (gen) (mul y x alpha-0)) x-0))))
  (label 93)
  (parent 63)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 group-2 text)
    (a b a-0 b-0 a-1 b-1 name)
    (group-dist group-dist-0 group-dist-1 group-dist-2 chan)
    (alpha y x alpha-0 x-0 alpha-1 y-0 rndx) (x-1 expt))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) alpha-1)) (group-dist group-dist-1) (x x-0)
    (y (mul y x alpha-0 (rec x-0) (rec alpha-1))))
  (defstrand group-init 1 (group group-1) (group-dist group-dist-1)
    (alpha alpha-1))
  (defstrand resp 3 (group group-2) (a a-1) (b b-1)
    (g (exp (gen) (mul y x alpha-0 (rec x-0) (rec y-0))))
    (group-dist group-dist-2) (y y-0) (x x-1))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (6 0)) ((4 3) (0 3)) ((5 0) (4 0))
    ((6 2) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x alpha-0 x-0 alpha-1 y-0)
  (absent (y (mul (rec alpha) x alpha-0)) (y-0 x-1))
  (conf group-dist group-dist-0 group-dist-1)
  (auth group-dist group-dist-0 group-dist-1 group-dist-2)
  (operation nonce-test (added-strand resp 3)
    (exp (gen) (mul y x alpha-0 (rec x-0))) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1)))
      (send (enc (exp (gen) (mul x-0 alpha-1)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha-0 (rec x-0)))
          (exp (gen) (mul x-0 alpha-1)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((send group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1))))
    ((recv group-dist-2
       (cat "Group id" group-2
         (exp (gen) (mul y x alpha-0 (rec x-0) (rec y-0)))))
      (recv
        (enc (exp (gen) (mul y x alpha-0 (rec x-0) (rec y-0) x-1))
          (privk a-1)))
      (send
        (enc (exp (gen) (mul y x alpha-0 (rec x-0)))
          (exp (gen) (mul y x alpha-0 (rec x-0) (rec y-0) x-1))
          (privk b-1)))))
  (label 94)
  (parent 63)
  (unrealized (6 0) (6 1))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 group-2 text) (a b a-0 b-0 a-1 name)
    (group-dist group-dist-0 group-dist-1 group-dist-2 chan)
    (alpha y x alpha-0 x-0 alpha-1 x-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) alpha-1)) (group-dist group-dist-1) (x x-0)
    (y (mul y x alpha-0 (rec x-0) (rec alpha-1))))
  (defstrand group-init 1 (group group-1) (group-dist group-dist-1)
    (alpha alpha-1))
  (defstrand init 2 (group group-2) (a a-1)
    (g (exp (gen) (mul y x alpha-0 (rec x-0) (rec x-1))))
    (group-dist group-dist-2) (x x-1))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (6 0)) ((4 3) (0 3)) ((5 0) (4 0))
    ((6 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x alpha-0 x-0 alpha-1 x-1)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0 group-dist-1)
  (auth group-dist group-dist-0 group-dist-1 group-dist-2)
  (operation nonce-test (added-strand init 2)
    (exp (gen) (mul y x alpha-0 (rec x-0))) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1)))
      (send (enc (exp (gen) (mul x-0 alpha-1)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha-0 (rec x-0)))
          (exp (gen) (mul x-0 alpha-1)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((send group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1))))
    ((recv group-dist-2
       (cat "Group id" group-2
         (exp (gen) (mul y x alpha-0 (rec x-0) (rec x-1)))))
      (send (enc (exp (gen) (mul y x alpha-0 (rec x-0))) (privk a-1)))))
  (label 95)
  (parent 63)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (alpha y x alpha-0 x-0 alpha-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) alpha-1)) (group-dist group-dist-1) (x x-0)
    (y (mul y x alpha-0 (rec x-0) (rec alpha-1))))
  (defstrand group-init 1 (group group-1) (group-dist group-dist-1)
    (alpha alpha-1))
  (deflistener (cat (exp (gen) (mul y x (rec x-0))) alpha-0))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (6 0)) ((4 3) (0 3)) ((5 0) (4 0))
    ((6 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x alpha-0 x-0 alpha-1)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0 group-dist-1)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x (rec x-0))) alpha-0))
    (exp (gen) (mul y x alpha-0 (rec x-0))) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1)))
      (send (enc (exp (gen) (mul x-0 alpha-1)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha-0 (rec x-0)))
          (exp (gen) (mul x-0 alpha-1)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((send group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1))))
    ((recv (cat (exp (gen) (mul y x (rec x-0))) alpha-0))
      (send (cat (exp (gen) (mul y x (rec x-0))) alpha-0))))
  (label 96)
  (parent 63)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (alpha y x alpha-0 x-0 alpha-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) alpha-1)) (group-dist group-dist-1) (x x-0)
    (y (mul y x alpha-0 (rec x-0) (rec alpha-1))))
  (defstrand group-init 1 (group group-1) (group-dist group-dist-1)
    (alpha alpha-1))
  (deflistener (cat (exp (gen) (mul y alpha-0 (rec x-0))) x))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (6 0)) ((4 3) (0 3)) ((5 0) (4 0))
    ((6 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x alpha-0 x-0 alpha-1)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0 group-dist-1)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha-0 (rec x-0))) x))
    (exp (gen) (mul y x alpha-0 (rec x-0))) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1)))
      (send (enc (exp (gen) (mul x-0 alpha-1)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha-0 (rec x-0)))
          (exp (gen) (mul x-0 alpha-1)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((send group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1))))
    ((recv (cat (exp (gen) (mul y alpha-0 (rec x-0))) x))
      (send (cat (exp (gen) (mul y alpha-0 (rec x-0))) x))))
  (label 97)
  (parent 63)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 name)
    (group-dist group-dist-0 group-dist-1 chan)
    (alpha y x alpha-0 x-0 alpha-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (group-dist group-dist) (y y)
    (x (mul (rec alpha) x alpha-0)))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (group-dist group-dist-0) (x x))
  (defstrand group-init 1 (group group-0) (group-dist group-dist-0)
    (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) alpha-1)) (group-dist group-dist-1) (x x-0)
    (y (mul y x alpha-0 (rec x-0) (rec alpha-1))))
  (defstrand group-init 1 (group group-1) (group-dist group-dist-1)
    (alpha alpha-1))
  (deflistener (cat (exp (gen) (mul x alpha-0 (rec x-0))) y))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((4 1) (6 0)) ((4 3) (0 3)) ((5 0) (4 0))
    ((6 1) (4 2)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha y x alpha-0 x-0 alpha-1)
  (absent (y (mul (rec alpha) x alpha-0)))
  (conf group-dist group-dist-0 group-dist-1)
  (auth group-dist group-dist-0 group-dist-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x alpha-0 (rec x-0))) y))
    (exp (gen) (mul y x alpha-0 (rec x-0))) (4 2))
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x alpha-0))))
      (send n))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1)))
      (send (enc (exp (gen) (mul x-0 alpha-1)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha-0 (rec x-0)))
          (exp (gen) (mul x-0 alpha-1)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0)))))
    ((send group-dist-1 (cat "Group id" group-1 (exp (gen) alpha-1))))
    ((recv (cat (exp (gen) (mul x alpha-0 (rec x-0))) y))
      (send (cat (exp (gen) (mul x alpha-0 (rec x-0))) y))))
  (label 98)
  (parent 63)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")