(comment "CPSA 2.1.1")
(comment "All input read")

(defprotocol dy basic
  (defrole init
    (vars (a b name) (m text))
    (trace (send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a)))))
  (defrole resp
    (vars (a b name) (m mesg))
    (trace (recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))))

(defskeleton dy
  (vars (m text) (a b name))
  (defstrand init 2 (m m) (a a) (b b))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a)))))
  (label 0)
  (unrealized (0 1))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dy
  (vars (m text) (b name))
  (defstrand init 2 (m m) (a b) (b b))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a b)) m (0 1)
    (enc (enc m (pubk b)) b (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b)))))
  (label 1)
  (parent 0)
  (unrealized)
  (shape))

(defskeleton dy
  (vars (m text) (a b name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (0 1)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 2)
  (parent 0)
  (unrealized)
  (shape))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (0 1)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0)))))
  (label 3)
  (parent 0)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dy
  (vars (m text) (b a name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-0 b)) m (0 1) (enc m (pubk b))
    (enc (enc m (pubk b)) b (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a)))))
  (label 4)
  (parent 3)
  (seen 1)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (0 1) (enc m (pubk b))
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1)))))
  (label 5)
  (parent 3)
  (unrealized (2 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-1 a)) m (2 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 6)
  (parent 5)
  (seen 2)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (2 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 7)
  (parent 5)
  (unrealized (2 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-1) (b b))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (2 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-1)) b (pubk a-1)))))
  (label 8)
  (parent 5)
  (unrealized)
  (shape))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-1 a)) m (2 0)
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 9)
  (parent 7)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (2 0)
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-2 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-2)) a (pubk a-2)))))
  (label 10)
  (parent 7)
  (unrealized (2 0) (4 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-1) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (2 0)
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-1)) b (pubk a-1)))))
  (label 11)
  (parent 7)
  (seen 6)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dy
  (vars (m text) (a b name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 12)
  (parent 9)
  (seen 2)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dy
  (vars (m text) (b a a-0 a-1 name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-1) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-2 b)) m (4 0)
    (enc (enc m (pubk b)) b (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-1)) b (pubk a-1)))))
  (label 13)
  (parent 10)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (4 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-2 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 14)
  (parent 10)
  (unrealized (2 0))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-2) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (1 0)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (4 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-2 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-2)) b (pubk a-2)))))
  (label 15)
  (parent 10)
  (unrealized (3 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dy
  (vars (m text) (b a a-0 name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-0) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0)))))
  (label 16)
  (parent 13)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-2 a)) m (2 0) (enc m (pubk a))
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 17)
  (parent 14)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a-1) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation nonce-test (contracted (b a)) m (2 0) (enc m (pubk a))
    (enc (enc m (pubk a)) a (pubk a)))
  (traces
    ((send (enc (enc m (pubk a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-0 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk a)) a-1 (pubk a)))
      (send (enc (enc m (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-2 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a)))))
  (label 18)
  (parent 14)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (3 0)) ((5 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (2 0) (enc m (pubk a))
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-2 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk a)) a-3 (pubk a)))
      (send (enc (enc m (pubk a-3)) a (pubk a-3)))))
  (label 19)
  (parent 14)
  (unrealized (5 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-2) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (2 0) (enc m (pubk a))
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-2 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-2)) b (pubk a-2)))))
  (label 20)
  (parent 14)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (b a a-0 a-1 name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-1) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (1 0)) ((4 1) (3 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-2 b)) m (3 0) (enc m (pubk b))
    (enc (enc m (pubk b)) b (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-1)) b (pubk a-1)))))
  (label 21)
  (parent 15)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-2) (b b))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (3 0)) ((5 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (3 0) (enc m (pubk b))
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-2 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-2)) b (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3)))))
  (label 22)
  (parent 15)
  (unrealized (5 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dy
  (vars (m text) (b a name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a)))))
  (label 23)
  (parent 16)
  (seen 4)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-0 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 24)
  (parent 17)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a a-0 a-1 name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a-0) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a-0 (pubk a)))
      (send (enc (enc m (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a)))))
  (label 25)
  (parent 18)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (b a a-0 a-1 name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-1) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (3 0)) ((5 1) (2 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-2 b) (a-3 b)) m (5 0)
    (enc (enc m (pubk b)) b (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 26)
  (parent 19)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((0 0) (6 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (3 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (5 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-2 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk a)) a-3 (pubk a)))
      (send (enc (enc m (pubk a-3)) a (pubk a-3))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 27)
  (parent 19)
  (unrealized (5 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-2) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-3) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (1 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (5 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk a)) a-2 (pubk a)))
      (send (enc (enc m (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-3 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-3)) b (pubk a-3)))))
  (label 28)
  (parent 19)
  (unrealized (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-1) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-0 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-1)) b (pubk a-1)))))
  (label 29)
  (parent 20)
  (seen 6)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dy
  (vars (m text) (b a a-0 name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-0) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0)))))
  (label 30)
  (parent 21)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-2) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (3 0)) ((5 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-3 a)) m (5 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-2 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-2)) b (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 31)
  (parent 22)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-2) (b b))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (5 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-2 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-2)) b (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 32)
  (parent 22)
  (unrealized (4 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-3) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (1 0)) ((4 1) (3 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (5 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-3 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-3)) b (pubk a-3)))))
  (label 33)
  (parent 22)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-0 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 34)
  (parent 24)
  (seen 2)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dy
  (vars (m text) (a a-0 name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-0 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a)))))
  (label 35)
  (parent 25)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (b a a-0 name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (1 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 36)
  (parent 26)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a b) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((0 0) (6 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (3 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-3 b)) m (5 0)
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-2 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 37)
  (parent 27)
  (unrealized (2 0))
  (comment "3 in cohort - 3 not yet seen"))

(comment "Strand bound exceeded--aborting run")

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 a-4 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-4) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((0 0) (6 0)) ((0 0) (7 0))
    ((1 1) (0 1)) ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (2 0)) ((6 1) (5 0)) ((7 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (5 0)
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-2 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk a)) a-3 (pubk a)))
      (send (enc (enc m (pubk a-3)) a (pubk a-3))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-4 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-4)) a (pubk a-4)))))
  (label 38)
  (parent 27)
  (unrealized (7 0))
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-3) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (6 0)) ((1 1) (0 1))
    ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (1 0)) ((5 1) (4 0))
    ((6 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (5 0)
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk a)) a-2 (pubk a)))
      (send (enc (enc m (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-3 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-3)) b (pubk a-3)))))
  (label 39)
  (parent 27)
  (unrealized (4 0))
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (b a a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-2) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (1 0)) ((5 1) (4 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-3 b)) m (4 0) (enc m (pubk b))
    (enc (enc m (pubk b)) b (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-2 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-2)) b (pubk a-2)))))
  (label 40)
  (parent 28)
  (unrealized)
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 a-4 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-2) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-3) (b b))
  (defstrand resp 2 (m m) (a a-4) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (6 0)) ((1 1) (0 1))
    ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (1 0)) ((5 1) (4 0))
    ((6 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (4 0) (enc m (pubk b))
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk a)) a-2 (pubk a)))
      (send (enc (enc m (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-3 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-3)) b (pubk a-3))))
    ((recv (enc (enc m (pubk b)) a-4 (pubk b)))
      (send (enc (enc m (pubk a-4)) b (pubk a-4)))))
  (label 41)
  (parent 28)
  (unrealized (6 0))
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (b a a-0 name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-0) (b b))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0)))))
  (label 42)
  (parent 30)
  (unrealized)
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-0 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 43)
  (parent 31)
  (unrealized)
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-2) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-3 a)) m (4 0)
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-2 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-2)) b (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 44)
  (parent 32)
  (unrealized)
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 a-4 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-2) (b b))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-4) (b a))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (6 0)) ((1 1) (0 1))
    ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (2 0)) ((5 1) (4 0))
    ((6 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (4 0)
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-2 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-2)) b (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-4 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-4)) a (pubk a-4)))))
  (label 45)
  (parent 32)
  (unrealized (4 0) (6 0))
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-3) (b b))
  (precedes ((0 0) (4 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (3 0)) ((5 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (4 0)
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-3 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-3)) b (pubk a-3)))))
  (label 46)
  (parent 32)
  (unrealized)
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-2) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-0 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-2 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-2)) b (pubk a-2)))))
  (label 47)
  (parent 33)
  (unrealized)
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a)))))
  (label 48)
  (parent 35)
  (unrealized)
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (b a name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (0 1)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 49)
  (parent 36)
  (unrealized)
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a b) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((0 0) (6 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (3 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-2 a)) m (2 0) (enc m (pubk a))
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 50)
  (parent 37)
  (unrealized)
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a-1) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((0 0) (6 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (3 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation nonce-test (contracted (b a)) m (2 0) (enc m (pubk a))
    (enc (enc m (pubk a)) a (pubk a)))
  (traces
    ((send (enc (enc m (pubk a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-0 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk a)) a-1 (pubk a)))
      (send (enc (enc m (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-2 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a)))))
  (label 51)
  (parent 37)
  (unrealized)
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a b) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-2) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (6 0)) ((1 1) (0 1))
    ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (1 0)) ((5 1) (4 0))
    ((6 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (2 0) (enc m (pubk a))
    (enc (enc m (pubk a)) b (pubk a)) (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-2 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-2)) b (pubk a-2)))))
  (label 52)
  (parent 37)
  (unrealized)
  (comment "aborted"))