packages feed

cpsa-4.4.4: tst/dh_group_sig_auth_failure.tst

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

(comment "CPSA 4.4.4")
(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))
  (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))
  (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))
  (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))
  (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))
  (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))
  (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))
  (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))
  (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")