(comment "CPSA 2.0.4")
(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 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 2)
  (parent 0)
  (unrealized (0 1))
  (comment "2 in cohort - 2 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))
  (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 3)
  (parent 0)
  (unrealized)
  (shape))

(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 2)
  (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 2)
  (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 3)
  (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 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 7)
  (parent 5)
  (unrealized)
  (shape))

(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 8)
  (parent 5)
  (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))
  (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 8)
  (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 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 10)
  (parent 8)
  (seen 6)
  (unrealized)
  (comment "1 in cohort - 0 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 11)
  (parent 8)
  (unrealized (2 0) (4 0))
  (comment "3 in cohort - 3 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 3)
  (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 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 nonce-test (contracted (a-1 b) (a-2 a-0)) 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 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 13)
  (parent 11)
  (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))
  (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 14)
  (parent 11)
  (unrealized (3 0))
  (comment "2 in cohort - 2 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 15)
  (parent 11)
  (unrealized (2 0))
  (comment "4 in cohort - 4 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 16)
  (parent 13)
  (seen 4)
  (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 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 17)
  (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 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 18)
  (parent 14)
  (unrealized (5 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 (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 19)
  (parent 15)
  (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 nonce-test (contracted (b a) (a-2 a-1)) 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 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 20)
  (parent 15)
  (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 (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 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 (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 22)
  (parent 15)
  (seen 20)
  (unrealized (5 0))
  (comment "3 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 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 23)
  (parent 17)
  (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 (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) (3 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (2 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 (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 24)
  (parent 18)
  (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 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 25)
  (parent 18)
  (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 26)
  (parent 18)
  (unrealized (4 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 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 27)
  (parent 19)
  (unrealized)
  (comment "1 in cohort - 1 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 28)
  (parent 20)
  (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 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 21)
  (seen 6)
  (unrealized)
  (comment "1 in cohort - 0 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 30)
  (parent 22)
  (unrealized (4 0))
  (comment "2 in cohort - 2 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 31)
  (parent 22)
  (unrealized (5 0))
  (comment "3 in cohort - 3 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 (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 32)
  (parent 23)
  (seen 4)
  (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 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) (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 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 (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 33)
  (parent 24)
  (seen 6)
  (unrealized)
  (comment "1 in cohort - 0 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) (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 34)
  (parent 25)
  (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 (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 35)
  (parent 26)
  (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 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 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 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 37)
  (parent 26)
  (unrealized (4 0) (6 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 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 38)
  (parent 27)
  (seen 3)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(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 39)
  (parent 28)
  (seen 1)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(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 30)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(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 30)
  (seen 43)
  (unrealized (6 0))
  (comment "3 in cohort - 2 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 42)
  (parent 31)
  (unrealized (2 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 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 43)
  (parent 31)
  (seen 58)
  (unrealized (4 0))
  (comment "4 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 44)
  (parent 31)
  (unrealized (7 0))
  (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 (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) (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 (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 45)
  (parent 34)
  (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 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))
  (defstrand resp 2 (m m) (a a) (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 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 (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))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 46)
  (parent 35)
  (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 (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 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) (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 (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 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 47)
  (parent 36)
  (unrealized)
  (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 a-1) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-2) (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 b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-3 b) (a-4 a-2)) m (6 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 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)) a-1 (pubk b)))
      (send (enc (enc m (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 (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 48)
  (parent 37)
  (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-2) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-3) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-4) (b b))
  (precedes ((0 0) (4 0)) ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (3 0)) ((5 1) (3 0)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (6 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-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 a)) b (pubk a)) a-3 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-3)) a (pubk a-3))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-4 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-4)) b (pubk a-4)))))
  (label 49)
  (parent 37)
  (unrealized (5 0))
  (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 (cat (enc m (pubk a)) b)) (a a-4) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (3 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) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (6 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 (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))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 50)
  (parent 37)
  (unrealized (4 0))
  (comment "aborted"))

(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 b) (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))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 1) (3 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 m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((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)))))
  (label 51)
  (parent 40)
  (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 m) (a a-3) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-4) (b b))
  (precedes ((0 0) (3 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) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (6 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 m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3))))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-4 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-4)) b (pubk a-4)))))
  (label 52)
  (parent 41)
  (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))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (7 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)) ((7 1) (6 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (6 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))))
    ((recv (enc (enc m (pubk b)) a-4 (pubk b)))
      (send (enc (enc m (pubk a-4)) b (pubk a-4))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 53)
  (parent 41)
  (unrealized (6 0))
  (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 54)
  (parent 42)
  (unrealized)
  (comment "aborted"))

(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))
  (defstrand resp 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (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))
  (uniq-orig m)
  (operation nonce-test (contracted (b a) (a-2 a-1)) 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 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))))
    ((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 55)
  (parent 42)
  (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 56)
  (parent 42)
  (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) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-3 b)) m (4 0) (enc m (pubk b))
    (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 57)
  (parent 43)
  (unrealized)
  (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 m) (a b) (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)) ((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 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 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-2 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-2)) b (pubk a-2)))))
  (label 58)
  (parent 43)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-3) (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)) ((0 0) (7 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)) ((7 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 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))))
    ((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 59)
  (parent 43)
  (unrealized (7 0))
  (comment "aborted"))