(comment "CPSA 2.1.2")
(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)
  (seen 8)
  (unrealized (2 0))
  (comment "4 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)
  (seen 12)
  (unrealized (2 0))
  (comment "5 in cohort - 4 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)
  (seen 15 16)
  (unrealized (2 0) (4 0))
  (comment "5 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 m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (2 0)) ((2 1) (0 1))
    ((3 1) (2 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 4 1 resp 2) m (2 0)
    (enc (enc m (pubk a-1)) b (pubk a-1))
    (enc (enc m (pubk b)) a-1 (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)))))
  (label 11)
  (parent 7)
  (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 12)
  (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 13)
  (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 14)
  (parent 10)
  (seen 11)
  (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 (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 10)
  (seen 19 21)
  (unrealized (2 0))
  (comment "7 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 16)
  (parent 10)
  (unrealized (3 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 (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m m) (a b) (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 (2 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)))))
  (label 17)
  (parent 11)
  (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 18)
  (parent 15)
  (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 19)
  (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 20)
  (parent 15)
  (seen 31)
  (unrealized (5 0))
  (comment "6 in cohort - 5 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) (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 22)
  (parent 16)
  (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 23)
  (parent 16)
  (seen 36 37)
  (unrealized (5 0))
  (comment "5 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 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) (3 0))
    ((3 1) (1 0)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 5 2 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)))))
  (label 24)
  (parent 16)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (b name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (1 0)) ((1 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)))))
  (label 25)
  (parent 17)
  (seen 1)
  (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 26)
  (parent 18)
  (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 27)
  (parent 19)
  (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 28)
  (parent 20)
  (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 29)
  (parent 20)
  (seen 46)
  (unrealized (5 0))
  (comment "7 in cohort - 6 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)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (2 0)) ((4 1) (3 0)) ((4 1) (5 0)) ((5 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 6 4 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)))))
  (label 30)
  (parent 20)
  (seen 32 52)
  (unrealized (5 0))
  (comment "7 in cohort - 5 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 31)
  (parent 20)
  (seen 52)
  (unrealized (4 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton dy
  (vars (m text) (a a-0 a-1 a-2 a-3 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-3) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (5 0)) ((4 1) (3 0)) ((5 1) (2 0)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation nonce-test (displaced 6 3 resp 2) m (5 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (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-3 (pubk a)))
      (send (enc (enc m (pubk a-3)) a (pubk a-3)))))
  (label 32)
  (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 33)
  (parent 21)
  (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 34)
  (parent 22)
  (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 35)
  (parent 23)
  (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 36)
  (parent 23)
  (seen 61)
  (unrealized (4 0))
  (comment "5 in cohort - 4 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 37)
  (parent 23)
  (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) (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))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (2 0)) ((2 1) (0 1))
    ((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 (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 38)
  (parent 24)
  (seen 6)
  (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 (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 39)
  (parent 26)
  (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 40)
  (parent 27)
  (seen 25)
  (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 (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 41)
  (parent 28)
  (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 42)
  (parent 29)
  (seen 65 66)
  (unrealized (2 0))
  (comment "7 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 43)
  (parent 29)
  (unrealized (7 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 (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 a-2) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((0 0) (6 0)) ((1 1) (5 0))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (3 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 1 resp 2) m (5 0)
    (enc (enc m (pubk a-3)) b (pubk a-3))
    (enc (enc m (pubk b)) a-3 (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)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 44)
  (parent 29)
  (unrealized)
  (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 (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) (5 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 (displaced 7 3 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)))))
  (label 45)
  (parent 29)
  (unrealized)
  (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 46)
  (parent 29)
  (unrealized (4 0))
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a a-0 a-1 a-2 a-3 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-3) (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) (5 0)) ((4 1) (3 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation nonce-test (displaced 7 3 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 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-3 (pubk a)))
      (send (enc (enc m (pubk a-3)) a (pubk a-3))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a)))))
  (label 47)
  (parent 29)
  (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 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))
  (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)) ((4 1) (5 0)) ((5 1) (2 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)))))
  (label 48)
  (parent 30)
  (unrealized (2 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 (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 (cat (enc m (pubk a)) b)) (a a-4) (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)) ((4 1) (5 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 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 (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 49)
  (parent 30)
  (unrealized (6 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 (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 a-2) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (2 0)) ((4 1) (3 0)) ((4 1) (5 0)) ((5 1) (2 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 6 1 resp 2) m (5 0)
    (enc (enc m (pubk a-3)) b (pubk a-3))
    (enc (enc m (pubk b)) a-3 (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)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2)))))
  (label 50)
  (parent 30)
  (unrealized)
  (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 (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)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (5 0)) ((4 1) (3 0)) ((5 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 6 3 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)))))
  (label 51)
  (parent 30)
  (unrealized)
  (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 (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)) ((3 1) (4 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 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 (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 52)
  (parent 30)
  (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 53)
  (parent 31)
  (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 54)
  (parent 31)
  (unrealized (6 0))
  (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 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-2) (b a))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (4 0)) ((3 1) (2 0))
    ((4 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 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-2 (pubk a)))
      (send (enc (enc m (pubk a-2)) a (pubk a-2)))))
  (label 55)
  (parent 32)
  (unrealized)
  (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 56)
  (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 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 57)
  (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 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 58)
  (parent 36)
  (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 59)
  (parent 36)
  (unrealized (4 0) (6 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 (cat (enc m (pubk b)) b)) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (4 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 6 3 resp 2) m (4 0)
    (enc (enc m (pubk a-3)) b (pubk a-3))
    (enc (enc m (pubk b)) a-3 (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 (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)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 60)
  (parent 36)
  (unrealized)
  (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 61)
  (parent 36)
  (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 62)
  (parent 37)
  (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 63)
  (parent 41)
  (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 64)
  (parent 42)
  (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 65)
  (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 66)
  (parent 42)
  (unrealized)
  (comment "aborted"))