(herald "Signed group DH exchange" (algebra diffie-hellman) (limit 100))

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

(defprotocol dh_sig diffie-hellman
  (defrole group-init
    (vars (alpha rndx) (group text))
    (trace (init (cat "Group id" group (exp (gen) alpha))))
    (uniq-gen alpha))
  (defrole init
    (vars (x rndx) (y expt) (g base) (group text) (a b name))
    (trace (obsv (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)
    (absent (x g)))
  (defrole resp
    (vars (y rndx) (x expt) (g base) (group text) (a b name))
    (trace (obsv (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 g) (y (exp g x)))))

(defskeleton dh_sig
  (vars (group text) (a b name) (g base) (x rndx) (y expt))
  (defstrand init 4 (group group) (a a) (b b) (g g) (x x) (y y))
  (absent (x g))
  (non-orig (privk a) (privk b))
  (uniq-gen x)
  (traces
    ((obsv (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) (x rndx) (y expt) (alpha rndx))
  (defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (x x) (y y))
  (defstrand group-init 1 (group group) (alpha alpha))
  (precedes ((1 0) (0 0)))
  (leadsto ((1 0) (0 0)))
  (absent (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen x alpha)
  (operation state-passing-test (added-strand group-init 1)
    (cat "Group id" group (exp (gen) alpha)) (0 0))
  (traces
    ((obsv (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))))
    ((init (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) (alpha x y rndx) (x-0 expt))
  (defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (x x) (y (mul x y (rec x-0))))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) (mul alpha x (rec x-0)))) (y y) (x x-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)))
  (leadsto ((1 0) (0 0)))
  (absent (y (exp (gen) (mul alpha x (rec x-0))))
    (y (exp (gen) (mul alpha x))) (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen alpha x y)
  (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
    ((obsv (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))))
    ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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) (y x alpha rndx))
  (defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (x x) (y y))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (y y) (x x))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (y (exp (gen) alpha)) (y (exp (gen) (mul x alpha)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (operation state-passing-test (displaced 3 1 group-init 1)
    (cat "Group id" group-0 (exp (gen) alpha-0)) (2 0))
  (traces
    ((obsv (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)))) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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)
  (unrealized)
  (shape)
  (maps
    ((0) ((a a) (b b) (x x) (y y) (g (exp (gen) alpha)) (group group))))
  (origs))

(defskeleton dh_sig
  (vars (group group-0 text) (a b a-0 name) (y alpha x alpha-0 rndx))
  (defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (x x) (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (y y) (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((3 0) (2 0)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (y (exp (gen) alpha-0)) (y (exp (gen) (mul alpha x)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha x alpha-0)
  (operation state-passing-test (added-strand group-init 1)
    (cat "Group id" group-0 (exp (gen) alpha-0)) (2 0))
  (traces
    ((obsv (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))))
    ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 4)
  (parent 2)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (x x) (y (mul y (rec alpha) alpha-0))
        (g (exp (gen) alpha)) (group group))))
  (origs))

(comment "Nothing left to do")

(defprotocol dh_sig diffie-hellman
  (defrole group-init
    (vars (alpha rndx) (group text))
    (trace (init (cat "Group id" group (exp (gen) alpha))))
    (uniq-gen alpha))
  (defrole init
    (vars (x rndx) (y expt) (g base) (group text) (a b name))
    (trace (obsv (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)
    (absent (x g)))
  (defrole resp
    (vars (y rndx) (x expt) (g base) (group text) (a b name))
    (trace (obsv (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 g) (y (exp g x)))))

(defskeleton dh_sig
  (vars (group text) (a b name) (g base) (y rndx) (x expt))
  (defstrand resp 4 (group group) (a a) (b b) (g g) (y y) (x x))
  (absent (y g) (y (exp g x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (traces
    ((obsv (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 5)
  (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) (y rndx) (x expt) (alpha rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (y y) (x x))
  (defstrand group-init 1 (group group) (alpha alpha))
  (precedes ((1 0) (0 0)))
  (leadsto ((1 0) (0 0)))
  (absent (y (exp (gen) alpha)) (y (exp (gen) (mul x alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha)
  (operation state-passing-test (added-strand group-init 1)
    (cat "Group id" group (exp (gen) alpha)) (0 0))
  (traces
    ((obsv (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))))
    ((init (cat "Group id" group (exp (gen) alpha)))))
  (label 6)
  (parent 5)
  (unrealized (0 1) (0 3))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton dh_sig
  (vars (group text) (a b name) (y x alpha rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (y y) (x x))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha)) (x x))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (x (exp (gen) alpha)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (operation state-passing-test (displaced 3 1 group-init 1)
    (cat "Group id" group-0 (exp (gen) alpha-0)) (2 0))
  (traces
    ((obsv (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)))) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))))
  (label 8)
  (parent 7)
  (unrealized (0 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group group-0 text) (a b name) (y x alpha alpha-0 rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (y y) (x (mul x (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0)) (x x))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1)) ((3 0) (2 0)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (x (exp (gen) alpha-0)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha alpha-0)
  (operation state-passing-test (added-strand group-init 1)
    (cat "Group id" group-0 (exp (gen) alpha-0)) (2 0))
  (traces
    ((obsv (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))))
    ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 9)
  (parent 7)
  (unrealized (0 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group text) (a b b-0 name) (alpha y x rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (y y) (x x))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 4 (group group) (a a) (b b-0) (g (exp (gen) alpha))
    (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)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (x (exp (gen) alpha)) (y (exp (gen) alpha))
    (y (exp (gen) (mul alpha x))))
  (non-orig (privk a) (privk b))
  (uniq-gen alpha y x)
  (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
    ((obsv (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)))) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 10)
  (parent 8)
  (unrealized)
  (shape)
  (maps
    ((0) ((a a) (b b) (y y) (x x) (g (exp (gen) alpha)) (group group))))
  (origs))

(defskeleton dh_sig
  (vars (group group-0 text) (a b b-0 name) (y alpha alpha-0 x rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (y y) (x (mul (rec alpha) alpha-0 x)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (group group-0) (a a) (b b-0)
    (g (exp (gen) alpha-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)))
  (leadsto ((1 0) (0 0)) ((2 0) (3 0)))
  (absent (x (exp (gen) alpha-0)) (y (exp (gen) alpha))
    (y (exp (gen) (mul alpha-0 x))))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha alpha-0 x)
  (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
    ((obsv (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))))
    ((init (cat "Group id" group (exp (gen) alpha))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (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 11)
  (parent 9)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group group-0 text) (a b b-0 name) (y alpha alpha-0 x rndx))
  (defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
    (y y) (x (mul (rec alpha) alpha-0 x)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (group group-0) (a a) (b b-0)
    (g (exp (gen) alpha-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)))
  (leadsto ((1 0) (0 0)) ((2 0) (3 0)))
  (absent (x (exp (gen) alpha-0)) (y (exp (gen) alpha))
    (y (exp (gen) (mul alpha-0 x))))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha alpha-0 x)
  (operation generalization weakened ((1 0) (3 0)))
  (traces
    ((obsv (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))))
    ((init (cat "Group id" group (exp (gen) alpha))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (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 12)
  (parent 11)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (y y) (x (mul (rec alpha) alpha-0 x))
        (g (exp (gen) alpha)) (group group))))
  (origs))

(comment "Nothing left to do")

(defprotocol dh_sig2 diffie-hellman
  (defrole group-init
    (vars (alpha rndx) (group text))
    (trace (init (cat "Group id" group (exp (gen) alpha))))
    (uniq-gen alpha))
  (defrole init
    (vars (x rndx) (y expt) (g base) (n group text) (a b name))
    (trace (obsv (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)
    (absent (x g)))
  (defrole resp
    (vars (y rndx) (x expt) (g base) (n group text) (a b name))
    (trace (obsv (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 g) (y (exp g x)))))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (g base) (x rndx) (y expt))
  (defstrand init 5 (n n) (group group) (a a) (b b) (g g) (x x) (y y))
  (absent (x g))
  (non-orig (privk a) (privk b))
  (uniq-gen n x)
  (traces
    ((obsv (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 13)
  (unrealized (0 0) (0 2))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (x rndx) (y expt) (alpha rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y y))
  (defstrand group-init 1 (group group) (alpha alpha))
  (precedes ((1 0) (0 0)))
  (leadsto ((1 0) (0 0)))
  (absent (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n x alpha)
  (operation state-passing-test (added-strand group-init 1)
    (cat "Group id" group (exp (gen) alpha)) (0 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha)))))
  (label 14)
  (parent 13)
  (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) (alpha x y rndx)
    (x-0 expt))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y (mul x y (rec x-0))))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) (mul alpha x (rec x-0)))) (y y) (x x-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)))
  (leadsto ((1 0) (0 0)))
  (absent (y (exp (gen) (mul alpha x (rec x-0))))
    (y (exp (gen) (mul alpha x))) (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y)
  (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
    ((obsv (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))
    ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 15)
  (parent 14)
  (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) (y x alpha rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y y))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (y y) (x x))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (y (exp (gen) alpha)) (y (exp (gen) (mul x alpha)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha)
  (operation state-passing-test (displaced 3 1 group-init 1)
    (cat "Group id" group-0 (exp (gen) alpha-0)) (2 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 16)
  (parent 15)
  (unrealized (0 4))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 name) (y alpha x alpha-0 rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (y y) (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)) ((3 0) (2 0)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (y (exp (gen) alpha-0)) (y (exp (gen) (mul alpha x)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0)
  (operation state-passing-test (added-strand group-init 1)
    (cat "Group id" group-0 (exp (gen) alpha-0)) (2 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 17)
  (parent 15)
  (unrealized (0 4))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a a-0 b name) (alpha x y rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y y))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 5 (n n) (group group) (a a-0) (b b)
    (g (exp (gen) alpha)) (y y) (x x))
  (precedes ((0 1) (2 0)) ((0 3) (2 3)) ((1 0) (0 0)) ((1 0) (2 0))
    ((2 2) (0 2)) ((2 4) (0 4)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (y (exp (gen) alpha)) (y (exp (gen) (mul alpha x)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y)
  (operation nonce-test (displaced 2 3 resp 5) n (0 4)
    (enc n (exp (gen) (mul y-0 x-0 alpha))))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 18)
  (parent 16)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (x x) (y y) (g (exp (gen) alpha)) (n n)
        (group group))))
  (origs))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 name) (y x alpha rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y y))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (y y) (x x))
  (deflistener (exp (gen) (mul y x alpha)))
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2))
    ((2 2) (3 0)) ((3 1) (0 4)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (y (exp (gen) alpha)) (y (exp (gen) (mul x alpha)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha)
  (operation nonce-test (added-listener (exp (gen) (mul y x alpha))) n
    (0 4) (enc n (exp (gen) (mul y x alpha))))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 19)
  (parent 16)
  (unrealized (3 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 name) (y alpha x alpha-0 rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (y y) (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-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)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (y (exp (gen) alpha-0)) (y (exp (gen) (mul alpha x)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-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
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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))))
    ((init (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 20)
  (parent 17)
  (unrealized (4 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 name) (y x alpha rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y y))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (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)) ((1 0) (2 0)) ((2 2) (0 2))
    ((2 2) (4 0)) ((3 1) (0 4)) ((4 1) (3 0)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (y (exp (gen) alpha)) (y (exp (gen) (mul x alpha)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x)) alpha))
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 21)
  (parent 19)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 name) (y x alpha rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y y))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (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)) ((1 0) (2 0)) ((2 2) (0 2))
    ((2 2) (4 0)) ((3 1) (0 4)) ((4 1) (3 0)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (y (exp (gen) alpha)) (y (exp (gen) (mul x alpha)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha)) x))
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 22)
  (parent 19)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b a-0 name) (y x alpha rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y y))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
    (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)) ((1 0) (2 0)) ((2 2) (0 2))
    ((2 2) (4 0)) ((3 1) (0 4)) ((4 1) (3 0)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (y (exp (gen) alpha)) (y (exp (gen) (mul x alpha)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x alpha)) y))
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 23)
  (parent 19)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 name) (y alpha x alpha-0 rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (y y) (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-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)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (y (exp (gen) alpha-0)) (y (exp (gen) (mul alpha x)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x)) alpha-0))
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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))))
    ((init (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 24)
  (parent 20)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 name) (y alpha x alpha-0 rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (y y) (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-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)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (y (exp (gen) alpha-0)) (y (exp (gen) (mul alpha x)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha-0)) x))
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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))))
    ((init (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 25)
  (parent 20)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 name) (y alpha x alpha-0 rndx))
  (defstrand init 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (x x) (y (mul y (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand resp 3 (group group-0) (a a-0) (b b)
    (g (exp (gen) alpha-0)) (y y) (x (mul alpha x (rec alpha-0))))
  (defstrand group-init 1 (group group-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)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (y (exp (gen) alpha-0)) (y (exp (gen) (mul alpha x)))
    (x (exp (gen) alpha)))
  (non-orig (privk a) (privk b))
  (uniq-gen n y alpha x alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x alpha-0)) y))
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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))))
    ((init (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 26)
  (parent 20)
  (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))
    (trace (init (cat "Group id" group (exp (gen) alpha))))
    (uniq-gen alpha))
  (defrole init
    (vars (x rndx) (y expt) (g base) (n group text) (a b name))
    (trace (obsv (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)
    (absent (x g)))
  (defrole resp
    (vars (y rndx) (x expt) (g base) (n group text) (a b name))
    (trace (obsv (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 g) (y (exp g x)))))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (g base) (y rndx) (x expt))
  (defstrand resp 5 (n n) (group group) (a a) (b b) (g g) (y y) (x x))
  (absent (y g) (y (exp g x)))
  (non-orig (privk a) (privk b))
  (uniq-gen y)
  (traces
    ((obsv (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 27)
  (unrealized (0 0) (0 1))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (y rndx) (x expt) (alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x))
  (defstrand group-init 1 (group group) (alpha alpha))
  (precedes ((1 0) (0 0)))
  (leadsto ((1 0) (0 0)))
  (absent (y (exp (gen) alpha)) (y (exp (gen) (mul x alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen y alpha)
  (operation state-passing-test (added-strand group-init 1)
    (cat "Group id" group (exp (gen) alpha)) (0 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha)))))
  (label 28)
  (parent 27)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton dh_sig2
  (vars (n group text) (a b name) (y x alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha)) (x x))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (x (exp (gen) alpha)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (operation state-passing-test (displaced 3 1 group-init 1)
    (cat "Group id" group-0 (exp (gen) alpha-0)) (2 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))))
  (label 30)
  (parent 29)
  (unrealized (0 3))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b name) (y x alpha alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul x (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0)) (x x))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1)) ((3 0) (2 0)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (x (exp (gen) alpha-0)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha alpha-0)
  (operation state-passing-test (added-strand group-init 1)
    (cat "Group id" group-0 (exp (gen) alpha-0)) (2 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 31)
  (parent 29)
  (unrealized (0 3))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (b a b-0 name) (alpha y x rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 4 (n n) (group group) (a a) (b b-0)
    (g (exp (gen) alpha)) (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)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (x (exp (gen) alpha)) (y (exp (gen) alpha))
    (y (exp (gen) (mul alpha x))))
  (non-orig (privk b) (privk a))
  (uniq-gen n alpha y x)
  (operation encryption-test (displaced 2 3 init 4)
    (enc n (exp (gen) (mul y-0 x-0 alpha))) (0 3))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 32)
  (parent 30)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (y y) (x x) (g (exp (gen) alpha)) (n n)
        (group group))))
  (origs))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name) (y x alpha rndx)
    (y-0 expt) (x-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha)) (x x))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) (mul y x alpha (rec y-0)))) (x x-0)
    (y (mul y-0 (rec x-0))))
  (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 3) (0 3)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (x-0 (exp (gen) (mul y x alpha (rec y-0))))
    (x (exp (gen) alpha)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha x-0)
  (operation encryption-test (added-strand init 4)
    (enc n (exp (gen) (mul y x alpha))) (0 3))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a))))
    ((obsv
       (cat "Group id" group-0 (exp (gen) (mul y x alpha (rec y-0)))))
      (send (enc (exp (gen) (mul y x alpha (rec y-0) x-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul y x alpha (rec x-0)))
          (exp (gen) (mul y x alpha (rec y-0) x-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha))))))
  (label 33)
  (parent 30)
  (unrealized (3 0) (3 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (y x alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha)) (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)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (x (exp (gen) alpha)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (operation encryption-test
    (added-listener (exp (gen) (mul y x alpha)))
    (enc n (exp (gen) (mul y x alpha))) (0 3))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 34)
  (parent 30)
  (unrealized (3 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (b a b-0 name) (alpha alpha-0 y x rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) alpha-0 x)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a) (b b-0)
    (g (exp (gen) alpha-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)))
  (leadsto ((1 0) (0 0)) ((2 0) (3 0)))
  (absent (x (exp (gen) alpha-0)) (y (exp (gen) alpha))
    (y (exp (gen) (mul alpha-0 x))))
  (non-orig (privk b) (privk a))
  (uniq-gen n alpha alpha-0 y x)
  (operation encryption-test (displaced 2 4 init 4)
    (enc n (exp (gen) (mul y-0 x-0 alpha-0))) (0 3))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (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 35)
  (parent 31)
  (unrealized (3 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 group-1 text) (a b a-0 b-0 name)
    (y x alpha alpha-0 rndx) (y-0 expt) (x-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul x (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0)) (x x))
  (defstrand group-init 1 (group group-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 y-0)))) (x x-0)
    (y (mul y-0 (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)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (x-0 (exp (gen) (mul y x alpha-0 (rec y-0))))
    (x (exp (gen) alpha-0)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen n y x alpha alpha-0 x-0)
  (operation encryption-test (added-strand init 4)
    (enc n (exp (gen) (mul y x alpha-0))) (0 3))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv
       (cat "Group id" group-1 (exp (gen) (mul y x alpha-0 (rec y-0)))))
      (send
        (enc (exp (gen) (mul y x alpha-0 (rec y-0) x-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) x-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x alpha-0))))))
  (label 36)
  (parent 31)
  (unrealized (4 0) (4 2))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b name) (y x alpha alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul x (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0)) (x x))
  (defstrand group-init 1 (group group-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)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (x (exp (gen) alpha-0)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha alpha-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
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((init (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 37)
  (parent 31)
  (unrealized (4 0))
  (comment "3 in cohort - 3 not yet seen"))

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

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (x y x-0 alpha alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x-0))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha)) (x x-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (x x)
    (y (mul (rec x) y x-0 alpha (rec alpha-0))))
  (defstrand group-init 1 (group group-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)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)) ((4 0) (3 0)))
  (absent (x (exp (gen) alpha-0)) (x-0 (exp (gen) alpha))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen n x y x-0 alpha alpha-0)
  (operation state-passing-test (added-strand group-init 1)
    (cat "Group id" group-0 (exp (gen) alpha-0)) (3 0))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x-0 alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x-0 alpha)) (privk a))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha))
          (exp (gen) (mul x alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha)))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 39)
  (parent 33)
  (unrealized (3 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (y x alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha)) (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)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (x (exp (gen) alpha)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x)) alpha))
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 40)
  (parent 34)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (y x alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha)) (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)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (x (exp (gen) alpha)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha)) x))
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 41)
  (parent 34)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group text) (a b name) (y x alpha rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha)) (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)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)))
  (absent (x (exp (gen) alpha)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x alpha)) y))
    (exp (gen) (mul y x alpha)) (3 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (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 42)
  (parent 34)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (b a b-0 name) (alpha alpha-0 y x rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) alpha-0 x)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a) (b b-0)
    (g (exp (gen) alpha-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)))
  (leadsto ((1 0) (0 0)) ((2 0) (3 0)))
  (absent (x (exp (gen) alpha-0)) (y (exp (gen) alpha))
    (y (exp (gen) (mul alpha-0 x))))
  (non-orig (privk b) (privk a))
  (uniq-gen n alpha alpha-0 y x)
  (operation nonce-test (added-listener (cat (exp (gen) alpha-0) y))
    (exp (gen) (mul alpha-0 y)) (3 2))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (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 43)
  (parent 35)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (b a b-0 name) (alpha alpha-0 y x rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) alpha-0 x)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a) (b b-0)
    (g (exp (gen) alpha-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)))
  (leadsto ((1 0) (0 0)) ((2 0) (3 0)))
  (absent (x (exp (gen) alpha-0)) (y (exp (gen) alpha))
    (y (exp (gen) (mul alpha-0 x))))
  (non-orig (privk b) (privk a))
  (uniq-gen n alpha alpha-0 y x)
  (operation nonce-test (added-listener (cat (exp (gen) y) alpha-0))
    (exp (gen) (mul alpha-0 y)) (3 2))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (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 44)
  (parent 35)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

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

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (alpha x y x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) x-0 alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (x x-0))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (x x) (y (mul (rec x) y x-0)))
  (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
    ((3 0) (2 0)) ((3 0) (4 0)) ((4 3) (0 3)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)) ((3 0) (4 0)))
  (absent (x (exp (gen) alpha-0)) (x-0 (exp (gen) alpha-0))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y x-0 alpha-0)
  (operation state-passing-test (displaced 5 3 group-init 1)
    (cat "Group id" group-1 (exp (gen) alpha-1)) (4 0))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x-0 alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha-0))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha-0))
          (exp (gen) (mul x alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha-0))))))
  (label 46)
  (parent 36)
  (unrealized (4 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)
    (alpha x y x-0 alpha-0 alpha-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) x-0 alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (x x-0))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) alpha-1)) (x x)
    (y (mul (rec x) y x-0 alpha-0 (rec alpha-1))))
  (defstrand group-init 1 (group group-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)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)) ((5 0) (4 0)))
  (absent (x (exp (gen) alpha-1)) (x-0 (exp (gen) alpha-0))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y x-0 alpha-0 alpha-1)
  (operation state-passing-test (added-strand group-init 1)
    (cat "Group id" group-1 (exp (gen) alpha-1)) (4 0))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x-0 alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha-0))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (cat "Group id" group-1 (exp (gen) alpha-1)))
      (send (enc (exp (gen) (mul x alpha-1)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha-0))
          (exp (gen) (mul x alpha-1)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha-0)))))
    ((init (cat "Group id" group-1 (exp (gen) alpha-1)))))
  (label 47)
  (parent 36)
  (unrealized (4 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b name) (y x alpha alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul x (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0)) (x x))
  (defstrand group-init 1 (group group-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)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (x (exp (gen) alpha-0)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x)) alpha-0))
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((init (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 48)
  (parent 37)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b name) (y x alpha alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul x (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0)) (x x))
  (defstrand group-init 1 (group group-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)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (x (exp (gen) alpha-0)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha-0)) x))
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((init (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 49)
  (parent 37)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b name) (y x alpha alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul x (rec alpha) alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0)) (x x))
  (defstrand group-init 1 (group group-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)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)))
  (absent (x (exp (gen) alpha-0)) (y (exp (gen) alpha))
    (y (exp (gen) (mul x alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen y x alpha alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x alpha-0)) y))
    (exp (gen) (mul y x alpha-0)) (4 0))
  (traces
    ((obsv (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)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((init (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 50)
  (parent 37)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

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

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

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

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

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (x y x-0 alpha alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x-0))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha)) (x x-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (x x)
    (y (mul (rec x) y x-0 alpha (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (deflistener (cat (exp (gen) (mul (rec x) y 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)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)) ((4 0) (3 0)))
  (absent (x (exp (gen) alpha-0)) (x-0 (exp (gen) alpha))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen n x y x-0 alpha alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) y x-0)) alpha))
    (exp (gen) (mul (rec x) y x-0 alpha)) (3 2))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x-0 alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x-0 alpha)) (privk a))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha))
          (exp (gen) (mul x alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha)))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (cat (exp (gen) (mul (rec x) y x-0)) alpha))
      (send (cat (exp (gen) (mul (rec x) y x-0)) alpha))))
  (label 55)
  (parent 39)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (x y x-0 alpha alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x-0))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha)) (x x-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (x x)
    (y (mul (rec x) y x-0 alpha (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (deflistener (cat (exp (gen) (mul (rec x) y 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)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)) ((4 0) (3 0)))
  (absent (x (exp (gen) alpha-0)) (x-0 (exp (gen) alpha))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen n x y x-0 alpha alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) y alpha)) x-0))
    (exp (gen) (mul (rec x) y x-0 alpha)) (3 2))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x-0 alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x-0 alpha)) (privk a))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha))
          (exp (gen) (mul x alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha)))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (cat (exp (gen) (mul (rec x) y alpha)) x-0))
      (send (cat (exp (gen) (mul (rec x) y alpha)) x-0))))
  (label 56)
  (parent 39)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (x y x-0 alpha alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x-0))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha)) (x x-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (x x)
    (y (mul (rec x) y x-0 alpha (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (deflistener (cat (exp (gen) (mul (rec x) x-0 alpha)) 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)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)) ((4 0) (3 0)))
  (absent (x (exp (gen) alpha-0)) (x-0 (exp (gen) alpha))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen n x y x-0 alpha alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) x-0 alpha)) y))
    (exp (gen) (mul (rec x) y x-0 alpha)) (3 2))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x-0 alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x-0 alpha)) (privk a))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha))
          (exp (gen) (mul x alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha)))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (cat (exp (gen) (mul (rec x) x-0 alpha)) y))
      (send (cat (exp (gen) (mul (rec x) x-0 alpha)) y))))
  (label 57)
  (parent 39)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (x y x-0 alpha alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x x-0))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group) (a a) (g (exp (gen) alpha)) (x x-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (x x)
    (y (mul (rec x) y x-0 alpha (rec alpha-0))))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (deflistener (cat (exp (gen) (mul y x-0 alpha)) 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)))
  (leadsto ((1 0) (0 0)) ((1 0) (2 0)) ((4 0) (3 0)))
  (absent (x (exp (gen) alpha-0)) (x-0 (exp (gen) alpha))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha))))
  (non-orig (privk a) (privk b))
  (uniq-gen n x y x-0 alpha alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x-0 alpha)) x))
    (exp (gen) (mul (rec x) y x-0 alpha)) (3 2))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha)) (privk a)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x-0 alpha))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x-0 alpha)) (privk a))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha))
          (exp (gen) (mul x alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha)))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv (cat (exp (gen) (mul y x-0 alpha)) x))
      (send (cat (exp (gen) (mul y x-0 alpha)) x))))
  (label 58)
  (parent 39)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

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

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

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

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

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (alpha x y x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) x-0 alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (x x-0))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (x x) (y (mul (rec x) y x-0)))
  (deflistener (cat (exp (gen) (mul (rec x) y 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)) ((3 0) (4 0)) ((4 1) (5 0)) ((4 3) (0 3))
    ((5 1) (4 2)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)) ((3 0) (4 0)))
  (absent (x (exp (gen) alpha-0)) (x-0 (exp (gen) alpha-0))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y x-0 alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) y x-0)) alpha-0))
    (exp (gen) (mul (rec x) y x-0 alpha-0)) (4 2))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x-0 alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha-0))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha-0))
          (exp (gen) (mul x alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha-0)))))
    ((recv (cat (exp (gen) (mul (rec x) y x-0)) alpha-0))
      (send (cat (exp (gen) (mul (rec x) y x-0)) alpha-0))))
  (label 63)
  (parent 46)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (alpha x y x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) x-0 alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (x x-0))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (x x) (y (mul (rec x) y x-0)))
  (deflistener (cat (exp (gen) (mul (rec x) y 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)) ((3 0) (4 0)) ((4 1) (5 0)) ((4 3) (0 3))
    ((5 1) (4 2)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)) ((3 0) (4 0)))
  (absent (x (exp (gen) alpha-0)) (x-0 (exp (gen) alpha-0))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y x-0 alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) y alpha-0)) x-0))
    (exp (gen) (mul (rec x) y x-0 alpha-0)) (4 2))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x-0 alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha-0))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha-0))
          (exp (gen) (mul x alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha-0)))))
    ((recv (cat (exp (gen) (mul (rec x) y alpha-0)) x-0))
      (send (cat (exp (gen) (mul (rec x) y alpha-0)) x-0))))
  (label 64)
  (parent 46)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (alpha x y x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) x-0 alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (x x-0))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (x x) (y (mul (rec x) y x-0)))
  (deflistener (cat (exp (gen) (mul (rec x) 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)) ((3 0) (4 0)) ((4 1) (5 0)) ((4 3) (0 3))
    ((5 1) (4 2)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)) ((3 0) (4 0)))
  (absent (x (exp (gen) alpha-0)) (x-0 (exp (gen) alpha-0))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y x-0 alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) x-0 alpha-0)) y))
    (exp (gen) (mul (rec x) y x-0 alpha-0)) (4 2))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x-0 alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha-0))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha-0))
          (exp (gen) (mul x alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha-0)))))
    ((recv (cat (exp (gen) (mul (rec x) x-0 alpha-0)) y))
      (send (cat (exp (gen) (mul (rec x) x-0 alpha-0)) y))))
  (label 65)
  (parent 46)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton dh_sig2
  (vars (n group group-0 text) (a b a-0 b-0 name)
    (alpha x y x-0 alpha-0 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) x-0 alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (x x-0))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-0) (a a-0) (b b-0)
    (g (exp (gen) alpha-0)) (x x) (y (mul (rec x) y x-0)))
  (deflistener (cat (exp (gen) (mul y 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)) ((3 0) (4 0)) ((4 1) (5 0)) ((4 3) (0 3))
    ((5 1) (4 2)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)) ((3 0) (4 0)))
  (absent (x (exp (gen) alpha-0)) (x-0 (exp (gen) alpha-0))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y x-0 alpha-0)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x-0 alpha-0)) x))
    (exp (gen) (mul (rec x) y x-0 alpha-0)) (4 2))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x-0 alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha-0))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha-0))
          (exp (gen) (mul x alpha-0)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha-0)))))
    ((recv (cat (exp (gen) (mul y x-0 alpha-0)) x))
      (send (cat (exp (gen) (mul y x-0 alpha-0)) x))))
  (label 66)
  (parent 46)
  (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)
    (alpha x y x-0 alpha-0 alpha-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) x-0 alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (x x-0))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) alpha-1)) (x x)
    (y (mul (rec x) y x-0 alpha-0 (rec alpha-1))))
  (defstrand group-init 1 (group group-1) (alpha alpha-1))
  (deflistener (cat (exp (gen) (mul (rec x) y 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)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)) ((5 0) (4 0)))
  (absent (x (exp (gen) alpha-1)) (x-0 (exp (gen) alpha-0))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y x-0 alpha-0 alpha-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) y x-0)) alpha-0))
    (exp (gen) (mul (rec x) y x-0 alpha-0)) (4 2))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x-0 alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha-0))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (cat "Group id" group-1 (exp (gen) alpha-1)))
      (send (enc (exp (gen) (mul x alpha-1)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha-0))
          (exp (gen) (mul x alpha-1)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha-0)))))
    ((init (cat "Group id" group-1 (exp (gen) alpha-1))))
    ((recv (cat (exp (gen) (mul (rec x) y x-0)) alpha-0))
      (send (cat (exp (gen) (mul (rec x) y x-0)) alpha-0))))
  (label 67)
  (parent 47)
  (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)
    (alpha x y x-0 alpha-0 alpha-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) x-0 alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (x x-0))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) alpha-1)) (x x)
    (y (mul (rec x) y x-0 alpha-0 (rec alpha-1))))
  (defstrand group-init 1 (group group-1) (alpha alpha-1))
  (deflistener (cat (exp (gen) (mul (rec x) y 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)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)) ((5 0) (4 0)))
  (absent (x (exp (gen) alpha-1)) (x-0 (exp (gen) alpha-0))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y x-0 alpha-0 alpha-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) y alpha-0)) x-0))
    (exp (gen) (mul (rec x) y x-0 alpha-0)) (4 2))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x-0 alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha-0))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (cat "Group id" group-1 (exp (gen) alpha-1)))
      (send (enc (exp (gen) (mul x alpha-1)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha-0))
          (exp (gen) (mul x alpha-1)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha-0)))))
    ((init (cat "Group id" group-1 (exp (gen) alpha-1))))
    ((recv (cat (exp (gen) (mul (rec x) y alpha-0)) x-0))
      (send (cat (exp (gen) (mul (rec x) y alpha-0)) x-0))))
  (label 68)
  (parent 47)
  (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)
    (alpha x y x-0 alpha-0 alpha-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) x-0 alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (x x-0))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) alpha-1)) (x x)
    (y (mul (rec x) y x-0 alpha-0 (rec alpha-1))))
  (defstrand group-init 1 (group group-1) (alpha alpha-1))
  (deflistener (cat (exp (gen) (mul (rec x) 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) (6 0)) ((4 3) (0 3)) ((5 0) (4 0))
    ((6 1) (4 2)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)) ((5 0) (4 0)))
  (absent (x (exp (gen) alpha-1)) (x-0 (exp (gen) alpha-0))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y x-0 alpha-0 alpha-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul (rec x) x-0 alpha-0)) y))
    (exp (gen) (mul (rec x) y x-0 alpha-0)) (4 2))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x-0 alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha-0))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (cat "Group id" group-1 (exp (gen) alpha-1)))
      (send (enc (exp (gen) (mul x alpha-1)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha-0))
          (exp (gen) (mul x alpha-1)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha-0)))))
    ((init (cat "Group id" group-1 (exp (gen) alpha-1))))
    ((recv (cat (exp (gen) (mul (rec x) x-0 alpha-0)) y))
      (send (cat (exp (gen) (mul (rec x) x-0 alpha-0)) y))))
  (label 69)
  (parent 47)
  (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)
    (alpha x y x-0 alpha-0 alpha-1 rndx))
  (defstrand resp 5 (n n) (group group) (a a) (b b)
    (g (exp (gen) alpha)) (y y) (x (mul (rec alpha) x-0 alpha-0)))
  (defstrand group-init 1 (group group) (alpha alpha))
  (defstrand init 2 (group group-0) (a a) (g (exp (gen) alpha-0))
    (x x-0))
  (defstrand group-init 1 (group group-0) (alpha alpha-0))
  (defstrand init 4 (n n) (group group-1) (a a-0) (b b-0)
    (g (exp (gen) alpha-1)) (x x)
    (y (mul (rec x) y x-0 alpha-0 (rec alpha-1))))
  (defstrand group-init 1 (group group-1) (alpha alpha-1))
  (deflistener (cat (exp (gen) (mul y 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) (6 0)) ((4 3) (0 3)) ((5 0) (4 0))
    ((6 1) (4 2)))
  (leadsto ((1 0) (0 0)) ((3 0) (2 0)) ((5 0) (4 0)))
  (absent (x (exp (gen) alpha-1)) (x-0 (exp (gen) alpha-0))
    (y (exp (gen) alpha)) (y (exp (gen) (mul x-0 alpha-0))))
  (non-orig (privk a) (privk b))
  (uniq-gen n alpha x y x-0 alpha-0 alpha-1)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x-0 alpha-0)) x))
    (exp (gen) (mul (rec x) y x-0 alpha-0)) (4 2))
  (traces
    ((obsv (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x-0 alpha-0)) (privk a)))
      (send
        (enc (exp (gen) (mul alpha y)) (exp (gen) (mul x-0 alpha-0))
          (privk b))) (recv (enc n (exp (gen) (mul y x-0 alpha-0))))
      (send n)) ((init (cat "Group id" group (exp (gen) alpha))))
    ((obsv (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x-0 alpha-0)) (privk a))))
    ((init (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((obsv (cat "Group id" group-1 (exp (gen) alpha-1)))
      (send (enc (exp (gen) (mul x alpha-1)) (privk a-0)))
      (recv
        (enc (exp (gen) (mul (rec x) y x-0 alpha-0))
          (exp (gen) (mul x alpha-1)) (privk b-0)))
      (send (enc n (exp (gen) (mul y x-0 alpha-0)))))
    ((init (cat "Group id" group-1 (exp (gen) alpha-1))))
    ((recv (cat (exp (gen) (mul y x-0 alpha-0)) x))
      (send (cat (exp (gen) (mul y x-0 alpha-0)) x))))
  (label 70)
  (parent 47)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")