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

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

(defprotocol dh_sig diffie-hellman
  (defrole group-init
    (vars (alpha rndx) (group text) (group-dist chan))
    (trace (send group-dist (cat "Group id" group (exp (gen) alpha))))
    (uniq-gen alpha)
    (conf group-dist))
  (defrole init
    (vars (x rndx) (y alpha expt) (group 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 (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))))
    (uniq-gen x)
    (absent (x alpha))
    (auth group-dist))
  (defrole resp
    (vars (y rndx) (x alpha expt) (group 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 (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))))
    (uniq-gen 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 text) (a b name) (group-dist chan) (x rndx)
    (y alpha expt))
  (defstrand init 4 (group group) (a a) (b b) (group-dist group-dist)
    (x x) (y y) (alpha alpha))
  (non-orig (privk a) (privk b))
  (uniq-gen 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 (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)))))
  (label 0)
  (unrealized (0 0) (0 2))
  (maps
    ((0)
      ((a a) (b b) (x x) (y y) (alpha alpha) (group group)
        (group-dist group-dist))))
  (origs)
  (ugens (x (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group text) (a b name) (group-dist chan) (x rndx) (y expt)
    (alpha rndx))
  (defstrand init 4 (group group) (a a) (b b) (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 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 (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha)))))
  (label 1)
  (parent 0)
  (unrealized (0 2))
  (maps
    ((0)
      ((a a) (b b) (x x) (y y) (alpha alpha) (group group)
        (group-dist group-dist))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (y x alpha rndx) (alpha-0 expt))
  (defstrand init 4 (group group) (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-0) (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 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 (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 (exp (gen) (mul y alpha-0)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" (exp (gen) (mul y alpha-0))
          (exp (gen) (mul x alpha)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul x alpha))
          (privk b)))))
  (label 2)
  (parent 1)
  (unrealized (2 0))
  (maps
    ((0)
      ((a a) (b b) (x x) (y (mul y (rec alpha) alpha-0)) (alpha alpha)
        (group group) (group-dist group-dist))))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig
  (vars (group text) (a b a-0 name) (group-dist chan) (y x alpha rndx))
  (defstrand init 4 (group group) (a a) (b b) (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-0) (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 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 (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))))
  (label 3)
  (parent 2)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (x x) (y y) (alpha alpha) (group group)
        (group-dist group-dist))))
  (origs)
  (ugens (alpha (1 0)) (y (2 2)) (x (0 1))))

(defskeleton dh_sig
  (vars (group group-0 text) (a b a-0 name)
    (group-dist group-dist-0 chan) (y x alpha alpha-0 rndx))
  (defstrand init 4 (group group) (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-0) (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 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 (exp (gen) (mul y alpha-0)) (exp (gen) (mul x alpha))
          (privk b)))
      (send
        (enc "final" (exp (gen) (mul y alpha-0))
          (exp (gen) (mul x alpha)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
      (send
        (enc (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)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (x x) (y (mul y (rec alpha) alpha-0)) (alpha alpha)
        (group group) (group-dist group-dist))))
  (origs)
  (ugens (alpha-0 (3 0)) (y (2 2)) (alpha (1 0)) (x (0 1))))

(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 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 (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))))
    (uniq-gen x)
    (absent (x alpha))
    (auth group-dist))
  (defrole resp
    (vars (y rndx) (x alpha expt) (group 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 (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))))
    (uniq-gen 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 text) (a b name) (group-dist chan) (y rndx)
    (x alpha expt))
  (defstrand resp 4 (group group) (a a) (b b) (group-dist group-dist)
    (y y) (x x) (alpha alpha))
  (non-orig (privk a) (privk b))
  (uniq-gen 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 (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)))))
  (label 5)
  (unrealized (0 0) (0 1) (0 3))
  (maps
    ((0)
      ((a a) (b b) (y y) (x x) (alpha alpha) (group group)
        (group-dist group-dist))))
  (origs)
  (ugens (y (0 2)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group text) (a b name) (group-dist chan) (y rndx) (x expt)
    (alpha rndx))
  (defstrand resp 4 (group group) (a a) (b b) (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 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 (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha)))))
  (label 6)
  (parent 5)
  (unrealized (0 1) (0 3))
  (maps
    ((0)
      ((a a) (b b) (y y) (x x) (alpha alpha) (group group)
        (group-dist group-dist))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group group-0 text) (a b name) (group-dist group-dist-0 chan)
    (y alpha x rndx) (alpha-0 expt))
  (defstrand resp 4 (group group) (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 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 (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha))
          (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a)))))
  (label 7)
  (parent 6)
  (unrealized (0 3) (2 0))
  (maps
    ((0)
      ((a a) (b b) (y y) (x (mul (rec alpha) x alpha-0)) (alpha alpha)
        (group group) (group-dist group-dist))))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dh_sig
  (vars (group text) (a b name) (group-dist chan) (y x alpha rndx))
  (defstrand resp 4 (group group) (a a) (b b) (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 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 (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul x alpha)) (privk a)))))
  (label 8)
  (parent 7)
  (unrealized (0 3))
  (maps
    ((0)
      ((a a) (b b) (y y) (x x) (alpha alpha) (group group)
        (group-dist group-dist))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group group-0 text) (a b name) (group-dist group-dist-0 chan)
    (y alpha x alpha-0 rndx))
  (defstrand resp 4 (group group) (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 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 (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha-0))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha))
          (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul x alpha-0)) (privk a))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))))
  (label 9)
  (parent 7)
  (unrealized (0 3))
  (maps
    ((0)
      ((a a) (b b) (y y) (x (mul (rec alpha) x alpha-0)) (alpha alpha)
        (group group) (group-dist group-dist))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dh_sig
  (vars (group text) (a b b-0 name) (group-dist chan) (y alpha x rndx))
  (defstrand resp 4 (group group) (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) (a a) (b b-0) (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 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" (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 (exp (gen) (mul y alpha)) (exp (gen) (mul alpha x))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul alpha x))
          (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((recv group-dist (cat "Group id" group (exp (gen) alpha)))
      (send (enc (exp (gen) (mul alpha x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul alpha x))
          (privk b-0)))
      (send
        (enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul alpha x))
          (privk a)))))
  (label 10)
  (parent 8)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (y y) (x x) (alpha alpha) (group group)
        (group-dist group-dist))))
  (origs)
  (ugens (x (2 1)) (alpha (1 0)) (y (0 2))))

(defskeleton dh_sig
  (vars (group group-0 text) (a b b-0 name)
    (group-dist group-dist-0 chan) (y alpha alpha-0 x rndx))
  (defstrand resp 4 (group group) (a a) (b b) (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) (a a) (b b-0)
    (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 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" (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 (exp (gen) (mul y alpha)) (exp (gen) (mul alpha-0 x))
          (privk b)))
      (recv
        (enc "final" (exp (gen) (mul y alpha))
          (exp (gen) (mul alpha-0 x)) (privk a))))
    ((send group-dist (cat "Group id" group (exp (gen) alpha))))
    ((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
    ((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
      (send (enc (exp (gen) (mul alpha-0 x)) (privk a)))
      (recv
        (enc (exp (gen) (mul y alpha)) (exp (gen) (mul alpha-0 x))
          (privk b-0)))
      (send
        (enc "final" (exp (gen) (mul y alpha))
          (exp (gen) (mul alpha-0 x)) (privk a)))))
  (label 11)
  (parent 9)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (y y) (x (mul (rec alpha) alpha-0 x)) (alpha alpha)
        (group group) (group-dist group-dist))))
  (origs)
  (ugens (x (3 1)) (alpha-0 (2 0)) (alpha (1 0)) (y (0 2))))

(comment "Nothing left to do")