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

(comment "CPSA 4.4.7")
(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) (group-dist chan))
    (trace (send group-dist (cat "Group id" group (exp (gen) alpha))))
    (uniq-gen alpha)
    (conf group-dist))
  (defrole init
    (vars (x rndx) (y alpha expt) (group na nb text) (a b name)
      (group-dist chan))
    (trace (recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc a (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" b na (exp (gen) (mul y alpha))
          (exp (gen) (mul x alpha)) (privk a)))
      (recv (enc na nb (exp (gen) (mul x y alpha)))) (send nb))
    (uniq-gen na x)
    (absent (x alpha))
    (auth group-dist))
  (defrole resp
    (vars (y rndx) (x alpha expt) (group na nb text) (a b name)
      (group-dist chan))
    (trace (recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc a (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (recv
        (enc "final" b na (exp (gen) (mul y alpha))
          (exp (gen) (mul x alpha)) (privk a)))
      (send (enc na nb (exp (gen) (mul y x alpha)))) (recv nb))
    (uniq-gen nb y)
    (absent (y (mul x alpha)) (y alpha))
    (auth group-dist))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton dh_sig
  (vars (group na nb text) (a b name) (group-dist chan) (x rndx)
    (y alpha expt))
  (defstrand init 6 (group group) (na na) (nb nb) (a a) (b b)
    (group-dist group-dist) (x x) (y y) (alpha alpha))
  (non-orig (privk a) (privk b))
  (uniq-gen na x)
  (absent (x alpha))
  (auth group-dist)
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc a (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" b na (exp (gen) (mul y alpha))
          (exp (gen) (mul x alpha)) (privk a)))
      (recv (enc na nb (exp (gen) (mul x y alpha)))) (send nb)))
  (label 0)
  (unrealized (0 0) (0 2))
  (maps
    ((0)
      ((a a) (b b) (x x) (y y) (alpha alpha) (group group) (na na)
        (nb nb) (group-dist group-dist))))
  (origs)
  (ugens (x (0 1)) (na (0 3)))
  (comment "1 in cohort - 1 not yet seen"))

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

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

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

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

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

(defskeleton dh_sig
  (vars (group na nb text) (a b name) (group-dist chan)
    (y x alpha rndx))
  (defstrand init 6 (group group) (na na) (nb nb) (a a) (b b)
    (group-dist group-dist) (x x) (y y) (alpha alpha))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a) (b b) (group-dist group-dist)
    (y y) (x x) (alpha alpha))
  (deflistener (exp (gen) (mul y x alpha)))
  (precedes ((0 1) (2 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2))
    ((2 2) (3 0)) ((3 1) (0 4)))
  (non-orig (privk a) (privk b))
  (uniq-gen na y x alpha)
  (absent (y (mul x alpha)) (y alpha) (x alpha))
  (conf group-dist)
  (auth group-dist)
  (operation encryption-test
    (added-listener (exp (gen) (mul y x alpha)))
    (enc na nb (exp (gen) (mul y x alpha))) (0 4))
  (strand-map 0 1 2)
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc a (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" b na (exp (gen) (mul y alpha))
          (exp (gen) (mul x alpha)) (privk a)))
      (recv (enc na nb (exp (gen) (mul y x alpha)))) (send nb))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc a (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 6)
  (parent 3)
  (unrealized (3 0))
  (maps
    ((0)
      ((a a) (b b) (x x) (y y) (alpha alpha) (group group) (na na)
        (nb nb) (group-dist group-dist))))
  (comment "3 in cohort - 3 not yet seen"))

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

(defskeleton dh_sig
  (vars (group na nb text) (a b name) (group-dist chan)
    (y x alpha rndx))
  (defstrand init 6 (group group) (na na) (nb nb) (a a) (b b)
    (group-dist group-dist) (x x) (y y) (alpha alpha))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a) (b b) (group-dist group-dist)
    (y y) (x x) (alpha alpha))
  (deflistener (exp (gen) (mul y x alpha)))
  (deflistener (cat (exp (gen) (mul y x)) alpha))
  (precedes ((0 1) (2 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2))
    ((2 2) (4 0)) ((3 1) (0 4)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen na y x alpha)
  (absent (y (mul x alpha)) (y alpha) (x alpha))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y x)) alpha))
    (exp (gen) (mul y x alpha)) (3 0))
  (strand-map 0 1 2 3)
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc a (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" b na (exp (gen) (mul y alpha))
          (exp (gen) (mul x alpha)) (privk a)))
      (recv (enc na nb (exp (gen) (mul y x alpha)))) (send nb))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc a (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 8)
  (parent 6)
  (unrealized (4 0))
  (dead)
  (maps
    ((0)
      ((a a) (b b) (x x) (y y) (alpha alpha) (group group) (na na)
        (nb nb) (group-dist group-dist))))
  (comment "empty cohort"))

(defskeleton dh_sig
  (vars (group na nb text) (a b name) (group-dist chan)
    (y x alpha rndx))
  (defstrand init 6 (group group) (na na) (nb nb) (a a) (b b)
    (group-dist group-dist) (x x) (y y) (alpha alpha))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a) (b b) (group-dist group-dist)
    (y y) (x x) (alpha alpha))
  (deflistener (exp (gen) (mul y x alpha)))
  (deflistener (cat (exp (gen) (mul y alpha)) x))
  (precedes ((0 1) (2 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2))
    ((2 2) (4 0)) ((3 1) (0 4)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen na y x alpha)
  (absent (y (mul x alpha)) (y alpha) (x alpha))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha)) x))
    (exp (gen) (mul y x alpha)) (3 0))
  (strand-map 0 1 2 3)
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc a (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" b na (exp (gen) (mul y alpha))
          (exp (gen) (mul x alpha)) (privk a)))
      (recv (enc na nb (exp (gen) (mul y x alpha)))) (send nb))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc a (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 9)
  (parent 6)
  (unrealized (4 0))
  (dead)
  (maps
    ((0)
      ((a a) (b b) (x x) (y y) (alpha alpha) (group group) (na na)
        (nb nb) (group-dist group-dist))))
  (comment "empty cohort"))

(defskeleton dh_sig
  (vars (group na nb text) (a b name) (group-dist chan)
    (y x alpha rndx))
  (defstrand init 6 (group group) (na na) (nb nb) (a a) (b b)
    (group-dist group-dist) (x x) (y y) (alpha alpha))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand resp 3 (group group) (a a) (b b) (group-dist group-dist)
    (y y) (x x) (alpha alpha))
  (deflistener (exp (gen) (mul y x alpha)))
  (deflistener (cat (exp (gen) (mul x alpha)) y))
  (precedes ((0 1) (2 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2))
    ((2 2) (4 0)) ((3 1) (0 4)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen na y x alpha)
  (absent (y (mul x alpha)) (y alpha) (x alpha))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul x alpha)) y))
    (exp (gen) (mul y x alpha)) (3 0))
  (strand-map 0 1 2 3)
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))
      (recv
        (enc a (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" b na (exp (gen) (mul y alpha))
          (exp (gen) (mul x alpha)) (privk a)))
      (recv (enc na nb (exp (gen) (mul y x alpha)))) (send nb))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a)))
      (send
        (enc a (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 10)
  (parent 6)
  (unrealized (4 0))
  (dead)
  (maps
    ((0)
      ((a a) (b b) (x x) (y y) (alpha alpha) (group group) (na na)
        (nb nb) (group-dist group-dist))))
  (comment "empty cohort"))

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

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

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

(comment "Nothing left to do")

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

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

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

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

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

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

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

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

(defskeleton dh_sig
  (vars (na nb group text) (a b name) (group-dist chan)
    (y alpha x rndx))
  (defstrand resp 6 (group group) (na na) (nb nb) (a a) (b b)
    (group-dist group-dist) (y y) (x x) (alpha alpha))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 6 (group group) (na na) (nb nb) (a a) (b b)
    (group-dist group-dist) (x x) (y y) (alpha alpha))
  (precedes ((0 2) (2 2)) ((0 4) (2 4)) ((1 0) (0 0)) ((1 0) (2 0))
    ((2 1) (0 1)) ((2 3) (0 3)) ((2 5) (0 5)))
  (non-orig (privk a) (privk b))
  (uniq-gen na nb y alpha x)
  (absent (y alpha) (y (mul alpha x)) (x alpha))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test (displaced 2 3 init 6) nb (0 5)
    (enc na nb (exp (gen) (mul y alpha-0 x-0))))
  (strand-map 0 1 2)
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a)))
      (send
        (enc a (exp (gen) (mul y alpha)) (exp (gen) (mul alpha x))
          (privk b)))
      (recv
        (enc "final" b na (exp (gen) (mul y alpha))
          (exp (gen) (mul alpha x)) (privk a)))
      (send (enc na nb (exp (gen) (mul y alpha x)))) (recv nb))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc a (exp (gen) (mul y alpha)) (exp (gen) (mul alpha x))
          (privk b)))
      (send
        (enc "final" b na (exp (gen) (mul y alpha))
          (exp (gen) (mul alpha x)) (privk a)))
      (recv (enc na nb (exp (gen) (mul y alpha x)))) (send nb)))
  (label 21)
  (parent 19)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (y y) (x x) (alpha alpha) (group group) (na na)
        (nb nb) (group-dist group-dist))))
  (origs)
  (ugens (na (2 3)) (x (2 1)) (alpha (1 0)) (y (0 2)) (nb (0 4))))

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

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

(defskeleton dh_sig
  (vars (na nb group text) (a b name) (group-dist chan)
    (y alpha x rndx))
  (defstrand resp 6 (group group) (na na) (nb nb) (a a) (b b)
    (group-dist group-dist) (y y) (x x) (alpha alpha))
  (defstrand group-init 1 (group group) (group-dist group-dist)
    (alpha alpha))
  (defstrand init 4 (group group) (na na) (a a) (b b)
    (group-dist group-dist) (x x) (y y) (alpha alpha))
  (deflistener (exp (gen) (mul y alpha x)))
  (deflistener (cat (exp (gen) (mul y alpha)) x))
  (precedes ((0 2) (2 2)) ((0 2) (4 0)) ((1 0) (0 0)) ((1 0) (2 0))
    ((2 1) (0 1)) ((2 3) (0 3)) ((3 1) (0 5)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-gen na nb y alpha x)
  (absent (y alpha) (y (mul alpha x)) (x alpha))
  (conf group-dist)
  (auth group-dist)
  (operation nonce-test
    (added-listener (cat (exp (gen) (mul y alpha)) x))
    (exp (gen) (mul y alpha x)) (3 0))
  (strand-map 0 1 2 3)
  (traces
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul alpha x)) (privk a)))
      (send
        (enc a (exp (gen) (mul y alpha)) (exp (gen) (mul alpha x))
          (privk b)))
      (recv
        (enc "final" b na (exp (gen) (mul y alpha))
          (exp (gen) (mul alpha x)) (privk a)))
      (send (enc na nb (exp (gen) (mul y alpha x)))) (recv nb))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc a (exp (gen) (mul y alpha)) (exp (gen) (mul alpha x))
          (privk b)))
      (send
        (enc "final" b na (exp (gen) (mul y alpha))
          (exp (gen) (mul alpha x)) (privk a))))
    ((recv (exp (gen) (mul y alpha x)))
      (send (exp (gen) (mul y alpha x))))
    ((recv (cat (exp (gen) (mul y alpha)) x))
      (send (cat (exp (gen) (mul y alpha)) x))))
  (label 24)
  (parent 22)
  (unrealized (4 0))
  (dead)
  (maps
    ((0)
      ((a a) (b b) (y y) (x x) (alpha alpha) (group group) (na na)
        (nb nb) (group-dist group-dist))))
  (comment "empty cohort"))

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

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

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

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

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

(comment "Nothing left to do")