(herald "Example 1.3 from 1983 Dolev-Yao Paper")

(comment "CPSA 2.3.1")
(comment "All input read from dy.lsp")

(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))
  (origs (m (0 0)))
  (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)
  (maps ((0) ((a b) (b b) (m m))))
  (origs (m (0 0))))

(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)
  (maps ((0) ((a a) (b b) (m m))))
  (origs (m (0 0))))

(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)
  (maps ((0) ((a a) (b b) (m m))))
  (origs (m (0 0))))

(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 "3 in cohort - 3 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (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 "3 in cohort - 3 not yet seen"))

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

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m 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 19)
  (parent 14)
  (seen 18)
  (unrealized (5 0))
  (comment "2 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 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)
  (unrealized (5 0))
  (comment "4 in cohort - 4 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 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 24)
  (parent 18)
  (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 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 19)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m 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 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 27)
  (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 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))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-1 b) (a-2 a-0) (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 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)))))
  (label 28)
  (parent 22)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m 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 29)
  (parent 22)
  (unrealized (4 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (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 22)
  (seen 37)
  (unrealized (5 0))
  (comment "4 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 (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)
  (seen 40)
  (unrealized (5 0))
  (comment "4 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 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 33)
  (parent 25)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-0 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 34)
  (parent 26)
  (seen 3)
  (unrealized)
  (comment "1 in cohort - 0 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) (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 m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 35)
  (parent 28)
  (unrealized)
  (comment "1 in cohort - 1 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 36)
  (parent 29)
  (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) (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 (displaced 6 3 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)))))
  (label 37)
  (parent 29)
  (unrealized (4 0))
  (comment "4 in cohort - 4 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 38)
  (parent 29)
  (seen 43)
  (unrealized (6 0))
  (comment "4 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 (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 39)
  (parent 30)
  (unrealized (2 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))
  (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 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 (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 41)
  (parent 30)
  (seen 40 50)
  (unrealized (6 0))
  (comment "4 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 "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 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 49)
  (unrealized (4 0))
  (comment "4 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 (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 33)
  (seen 7)
  (unrealized)
  (comment "1 in cohort - 0 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 46)
  (parent 35)
  (seen 1)
  (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 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 47)
  (parent 36)
  (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 m) (a b) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (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)) ((3 1) (4 0)) ((4 1) (1 0)) ((5 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 (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 48)
  (parent 37)
  (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) (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) (4 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 (displaced 6 2 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 (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 49)
  (parent 37)
  (unrealized)
  (comment "1 in cohort - 1 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)) ((3 1) (4 0)) ((4 1) (1 0)) ((5 1) (4 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 6 5 resp 2) m (4 0) (enc m (pubk b))
    (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 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 50)
  (parent 37)
  (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 (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)) ((3 1) (4 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 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))))
    ((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 51)
  (parent 37)
  (seen 49 50 58)
  (unrealized (6 0))
  (comment "4 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 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 38)
  (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)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (6 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 (displaced 7 3 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)))))
  (label 53)
  (parent 38)
  (unrealized (6 0))
  (comment "4 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 (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))
  (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-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)))))
  (label 55)
  (parent 39)
  (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 m) (a b) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (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)) ((3 1) (4 0)) ((4 1) (1 0)) ((5 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 (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 39)
  (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 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) (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-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)))))
  (label 57)
  (parent 40)
  (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 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) (3 0)) ((0 0) (6 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))
    ((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 (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 58)
  (parent 41)
  (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))
  (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 60)
  (parent 42)
  (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 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 61)
  (parent 42)
  (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 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 62)
  (parent 43)
  (unrealized)
  (comment "1 in cohort - 1 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 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 (displaced 7 6 resp 2) m (4 0) (enc m (pubk b))
    (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 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 63)
  (parent 43)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (b a a-0 name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a 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))
  (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 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)))))
  (label 65)
  (parent 47)
  (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 m) (a b) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-1) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((2 1) (3 0)) ((3 1) (0 1)) ((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 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 (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 66)
  (parent 48)
  (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 a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (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) (3 0)) ((2 1) (1 0))
    ((3 1) (0 1)) ((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 m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((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 b)) a (pubk b)) a-2 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-2)) b (pubk a-2)))))
  (label 67)
  (parent 49)
  (seen 27)
  (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 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))
    ((2 1) (3 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 68)
  (parent 50)
  (seen 13)
  (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 (cat (enc m (pubk a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (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) (0 1)) ((4 1) (3 0)) ((5 1) (4 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))))
    ((recv (enc (enc m (pubk a)) a-1 (pubk a)))
      (send (enc (enc m (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 70)
  (parent 52)
  (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) (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) (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) (6 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-4 a)) m (6 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))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 71)
  (parent 53)
  (unrealized (4 0))
  (comment "4 in cohort - 4 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 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)) ((3 1) (5 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 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-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 72)
  (parent 53)
  (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)) ((1 1) (0 1)) ((2 1) (6 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 (displaced 7 2 resp 2) m (6 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))))
    ((recv (enc (enc m (pubk b)) a-4 (pubk b)))
      (send (enc (enc m (pubk a-4)) b (pubk a-4)))))
  (label 73)
  (parent 53)
  (unrealized (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 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 m) (a b) (b a))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0))
    ((3 1) (4 0)) ((4 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 (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 m (pubk a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b)))))
  (label 75)
  (parent 55)
  (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 m) (a b) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-1) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((2 1) (3 0)) ((3 1) (0 1)) ((4 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 m (pubk a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b))))
    ((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 76)
  (parent 56)
  (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 m) (a a-1) (b a))
  (precedes ((0 0) (2 0)) ((1 1) (3 0)) ((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 m (pubk a)) a-1 (pubk a)))
      (send (enc (enc m (pubk a-1)) a (pubk a-1)))))
  (label 77)
  (parent 57)
  (seen 34)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dy
  (vars (m text) (b a a-0 a-1 a-2 a-3 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))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-3) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (6 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))
    ((6 1) (5 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-4 b)) m (5 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))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-3 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-3)) b (pubk a-3)))))
  (label 78)
  (parent 58)
  (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 m) (a a-1) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (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) (4 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 (displaced 7 3 resp 2) m (5 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 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)) 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 (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 79)
  (parent 58)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m 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 m) (a b) (b a))
  (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) (1 0)) ((5 1) (4 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))))
    ((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 81)
  (parent 60)
  (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 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-1) (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) (0 1)) ((4 1) (3 0)) ((5 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 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-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-1)) b (pubk a-1)))))
  (label 82)
  (parent 61)
  (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 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-1) (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) (0 1)) ((4 1) (3 0)) ((5 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 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-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-1)) b (pubk a-1)))))
  (label 83)
  (parent 62)
  (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 b) (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) (2 0)) ((0 0) (4 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (1 0)) ((3 1) (0 1)) ((4 1) (3 0)) ((5 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 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 84)
  (parent 63)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (b a a-0 name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-0) (b b))
  (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 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)))))
  (label 85)
  (parent 65)
  (seen 4)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a b) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (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 m (pubk a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b))))
    ((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 86)
  (parent 66)
  (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 m) (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 m (pubk a)) a-0 (pubk a)))
      (send (enc (enc m (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 87)
  (parent 70)
  (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 m) (a b) (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) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((3 1) (6 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 (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 88)
  (parent 71)
  (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) (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) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (4 0))
    ((3 1) (2 0)) ((3 1) (6 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 (displaced 7 2 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 (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 (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 89)
  (parent 71)
  (unrealized)
  (comment "1 in cohort - 1 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))
  (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) (2 0)) ((3 1) (6 0)) ((4 1) (1 0)) ((5 1) (4 0))
    ((6 1) (4 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 5 resp 2) m (4 0) (enc m (pubk b))
    (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 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))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 90)
  (parent 71)
  (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 a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (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))
    ((2 1) (4 0)) ((3 1) (0 1)) ((4 1) (3 0)) ((5 1) (4 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))))
    ((recv (enc (enc m (pubk a)) a-1 (pubk a)))
      (send (enc (enc m (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 92)
  (parent 72)
  (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) (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) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (6 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-4 a)) m (6 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)) 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 (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 93)
  (parent 73)
  (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 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) (5 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 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)) 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 94)
  (parent 73)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a b) (b a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((2 1) (3 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 m (pubk a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b)))))
  (label 96)
  (parent 75)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a b) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (2 0)) ((2 1) (0 1))
    ((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 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 (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 97)
  (parent 76)
  (seen 6)
  (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 (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))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-2) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((2 1) (3 0)) ((3 1) (0 1)) ((4 1) (3 0)) ((5 1) (4 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))))
    ((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 98)
  (parent 78)
  (seen 17)
  (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 m) (a a-0) (b a))
  (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) (1 0)) ((0 0) (4 0)) ((1 1) (3 0)) ((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 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)) 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 99)
  (parent 79)
  (seen 24)
  (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))
  (defstrand resp 2 (m m) (a b) (b a))
  (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) (0 1)) ((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 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 100)
  (parent 81)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m 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-0) (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) (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 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-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0)))))
  (label 101)
  (parent 82)
  (seen 97)
  (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 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-0) (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 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-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0)))))
  (label 102)
  (parent 83)
  (seen 86)
  (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 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) (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 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 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 103)
  (parent 84)
  (seen 13)
  (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-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 m (pubk a)) a-0 (pubk a)))
      (send (enc (enc m (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 104)
  (parent 87)
  (seen 7)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m m) (a b) (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) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((2 1) (5 0)) ((3 1) (0 1)) ((4 1) (3 0)) ((5 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 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 (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 105)
  (parent 88)
  (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 a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (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)) ((1 1) (3 0)) ((2 1) (1 0))
    ((2 1) (5 0)) ((3 1) (0 1)) ((4 1) (3 0)) ((5 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 m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((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 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 106)
  (parent 89)
  (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 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))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((2 1) (5 0)) ((3 1) (0 1)) ((4 1) (3 0)) ((5 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))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 107)
  (parent 90)
  (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) (b b))
  (defstrand resp 2 (m m) (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) (3 0)) ((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 m (pubk a)) a-0 (pubk a)))
      (send (enc (enc m (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 108)
  (parent 92)
  (seen 104)
  (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 a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (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)) ((1 1) (5 0)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 1) (3 0)) ((5 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 m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((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 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 109)
  (parent 93)
  (seen 20)
  (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 (cat (enc m (pubk a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (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) (4 0)) ((2 1) (1 0))
    ((3 1) (0 1)) ((4 1) (3 0)) ((5 1) (4 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))))
    ((recv (enc (enc m (pubk a)) a-1 (pubk a)))
      (send (enc (enc m (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 110)
  (parent 94)
  (seen 108)
  (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 b) (b a))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 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 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 111)
  (parent 96)
  (seen 3)
  (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 b) (b a))
  (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 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 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 112)
  (parent 100)
  (seen 111)
  (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 m) (a b) (b a))
  (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) (3 0)) ((1 1) (4 0)) ((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 m (pubk a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b))))
    ((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 113)
  (parent 105)
  (seen 86)
  (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 m) (a a) (b b))
  (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))
    ((2 1) (4 0)) ((3 1) (0 1)) ((4 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (3 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))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 114)
  (parent 106)
  (seen 9)
  (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 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))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (4 0)) ((2 1) (0 1))
    ((3 1) (2 0)) ((4 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 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)))))
  (label 115)
  (parent 107)
  (seen 13)
  (unrealized)
  (comment "1 in cohort - 0 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 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 54)
  (parent 38)
  (unrealized (6 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))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (4 0)) ((0 0) (7 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)) ((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 (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))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 59)
  (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 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 64)
  (parent 43)
  (unrealized (7 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 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 (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) (5 0)) ((0 0) (7 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)) ((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 (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 69)
  (parent 51)
  (unrealized)
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 a-4 a-5 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 (cat (enc m (pubk a)) b)) (a a-5) (b a))
  (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)) ((3 1) (6 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 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))))
    ((recv (enc (enc m (pubk b)) a-4 (pubk b)))
      (send (enc (enc m (pubk a-4)) b (pubk a-4))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-5 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-5)) a (pubk a-5)))))
  (label 74)
  (parent 53)
  (unrealized (6 0) (7 0))
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 a-4 a-5 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 a)) b)) (a a-3) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-4) (b b))
  (defstrand resp 2 (m m) (a a-5) (b b))
  (precedes ((0 0) (3 0)) ((0 0) (6 0)) ((0 0) (7 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)) ((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 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 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))))
    ((recv (enc (enc m (pubk b)) a-5 (pubk b)))
      (send (enc (enc m (pubk a-5)) b (pubk a-5)))))
  (label 80)
  (parent 58)
  (unrealized (7 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 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) (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) (7 0)) ((1 1) (0 1))
    ((2 1) (1 0)) ((3 1) (2 0)) ((3 1) (6 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 (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 (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 91)
  (parent 71)
  (unrealized (7 0))
  (comment "aborted"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 a-4 a-5 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-5) (b a))
  (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (7 0)) ((1 1) (0 1))
    ((2 1) (6 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 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)) 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 a)) a-5 (pubk a)))
      (send (enc (enc m (pubk a-5)) a (pubk a-5)))))
  (label 95)
  (parent 73)
  (unrealized (7 0))
  (comment "aborted"))