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

(comment "CPSA 2.2.11")
(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 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (0 1)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 2)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (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 3)
  (parent 0)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

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

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

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

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

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

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

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

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

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

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

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m 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)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (4 0)) ((4 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 5 3 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 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 15)
  (parent 11)
  (seen 19 21)
  (unrealized (2 0))
  (comment "7 in cohort - 4 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (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)) ((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 nonce-test (displaced 5 1 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 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 16)
  (parent 11)
  (unrealized (4 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))
  (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 17)
  (parent 14)
  (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) (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))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (4 0)) ((4 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 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)))))
  (label 18)
  (parent 15)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

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

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

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (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)) ((1 1) (2 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((4 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 5 1 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 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 21)
  (parent 15)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (b a a-0 a-1 name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-1) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (4 0)) ((2 1) (0 1))
    ((3 1) (2 0)) ((4 1) (2 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-2 b)) m (4 0) (enc 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))))
    ((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 22)
  (parent 16)
  (seen 10)
  (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)) ((1 1) (4 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((4 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 5 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 (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 23)
  (parent 16)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (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))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((1 1) (4 0))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (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 (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))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3)))))
  (label 24)
  (parent 16)
  (seen 23 33 34)
  (unrealized (5 0))
  (comment "5 in cohort - 2 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 a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-0) (b a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (3 0)) ((3 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc 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))))
    ((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)))))
  (label 25)
  (parent 18)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (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))
  (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) (3 0)) ((0 0) (6 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (4 0)) ((4 1) (2 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 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))))
    ((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 28)
  (parent 20)
  (seen 30 38 44)
  (unrealized (5 0))
  (comment "7 in cohort - 4 not yet seen"))

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

(defskeleton dy
  (vars (m text) (a a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a-2) (b a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (3 0)) ((3 1) (4 0))
    ((4 1) (1 0)))
  (non-orig (privk a))
  (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 a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a-0 (pubk a)))
      (send (enc (enc m (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk a)) a-2 (pubk a)))
      (send (enc (enc m (pubk a-2)) a (pubk a-2)))))
  (label 30)
  (parent 20)
  (seen 19)
  (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) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (3 0))
    ((3 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 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)))))
  (label 31)
  (parent 21)
  (seen 35)
  (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) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (3 0)) ((2 1) (3 0))
    ((3 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 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)))))
  (label 32)
  (parent 23)
  (seen 35)
  (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 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))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (4 0)) ((2 1) (0 1))
    ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (4 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 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))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3)))))
  (label 33)
  (parent 24)
  (seen 50)
  (unrealized (5 0))
  (comment "5 in cohort - 4 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (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))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (2 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 6 1 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 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))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3)))))
  (label 34)
  (parent 24)
  (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))
  (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 (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)))))
  (label 35)
  (parent 25)
  (seen 2)
  (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))
  (defstrand resp 2 (m m) (a b) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (5 0)) ((4 1) (2 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 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))))
    ((recv (enc (enc m (pubk a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b)))))
  (label 36)
  (parent 27)
  (seen 53 54)
  (unrealized (2 0))
  (comment "6 in cohort - 3 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 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))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (2 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 6 1 resp 2) m (5 0)
    (enc (enc m (pubk a-3)) b (pubk a-3))
    (enc (enc m (pubk b)) a-3 (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc 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))))
    ((recv (enc (enc m (pubk b)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2)))))
  (label 37)
  (parent 27)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (4 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 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))))
    ((recv (enc (enc m (pubk a)) a-3 (pubk a)))
      (send (enc (enc m (pubk a-3)) a (pubk a-3)))))
  (label 38)
  (parent 27)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (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) (3 0)) ((0 0) (6 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (4 0)) ((3 1) (5 0)) ((4 1) (2 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 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))))
    ((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 39)
  (parent 27)
  (seen 37 38 58)
  (unrealized (6 0))
  (comment "6 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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 6 1 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 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))))
    ((recv (enc (enc m (pubk a)) a-3 (pubk a)))
      (send (enc (enc m (pubk a-3)) a (pubk a-3)))))
  (label 40)
  (parent 27)
  (seen 37)
  (unrealized (5 0))
  (comment "5 in cohort - 3 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (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))
  (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)) ((0 0) (6 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (4 0)) ((4 1) (2 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 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))))
    ((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 41)
  (parent 28)
  (seen 64 65)
  (unrealized (2 0))
  (comment "7 in cohort - 3 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 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))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (6 0)) ((1 1) (5 0))
    ((2 1) (0 1)) ((3 1) (4 0)) ((4 1) (2 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 1 resp 2) m (5 0)
    (enc (enc m (pubk a-3)) b (pubk a-3))
    (enc (enc m (pubk b)) a-3 (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc 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))))
    ((recv (enc (enc m (pubk b)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 42)
  (parent 28)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (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) (3 0)) ((0 0) (6 0)) ((1 1) (5 0))
    ((2 1) (0 1)) ((3 1) (4 0)) ((4 1) (2 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 1 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 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))))
    ((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 44)
  (parent 28)
  (seen 42 61)
  (unrealized (5 0))
  (comment "5 in cohort - 2 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 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))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((4 1) (2 0)) ((5 1) (2 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-3 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 (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2)))))
  (label 45)
  (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 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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (defstrand resp 2 (m m) (a a-4) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (6 0)) ((1 1) (5 0))
    ((2 1) (0 1)) ((3 1) (4 0)) ((4 1) (2 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 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))))
    ((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))))
    ((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-4 (pubk b)))
      (send (enc (enc m (pubk a-4)) b (pubk a-4)))))
  (label 46)
  (parent 29)
  (seen 44 72)
  (unrealized (6 0))
  (comment "6 in cohort - 4 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (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))
  (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) (5 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-3 a)) m (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 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))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 47)
  (parent 33)
  (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 (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 6 1 resp 2) m (5 0)
    (enc (enc m (pubk a-3)) b (pubk a-3))
    (enc (enc m (pubk b)) a-3 (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc 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))))
    ((recv (enc (enc m (pubk b)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2)))))
  (label 48)
  (parent 33)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-4) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (6 0)) ((1 1) (4 0))
    ((2 1) (0 1)) ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (4 0))
    ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (added-strand resp 2) m (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 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))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-4 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-4)) a (pubk a-4)))))
  (label 49)
  (parent 33)
  (seen 48 76 77)
  (unrealized (5 0) (6 0))
  (comment "5 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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 6 1 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 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))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3)))))
  (label 50)
  (parent 33)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

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

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

(defskeleton dy
  (vars (m text) (a a-0 a-1 name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (3 0)) ((2 1) (4 0))
    ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation nonce-test (contracted (b a) (a-2 a-1)) m (2 0)
    (enc m (pubk a)) (enc (enc m (pubk a)) a (pubk a)))
  (traces
    ((send (enc (enc m (pubk a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a-0 (pubk a)))
      (send (enc (enc m (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a)))))
  (label 53)
  (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 (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))
  (defstrand resp 2 (m m) (a b) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (2 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 6 1 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 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))))
    ((recv (enc (enc m (pubk a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b)))))
  (label 54)
  (parent 36)
  (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 (cat (enc m (pubk b)) b)) (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) (4 0)) ((2 1) (3 0))
    ((2 1) (4 0)) ((3 1) (0 1)) ((4 1) (0 1)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1)))))
  (label 55)
  (parent 37)
  (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 m) (a a-2) (b a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (3 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-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 a)) a-2 (pubk a)))
      (send (enc (enc m (pubk a-2)) a (pubk a-2)))))
  (label 56)
  (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 (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))
  (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) (3 0)) ((1 1) (6 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 1 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 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))))
    ((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 58)
  (parent 39)
  (unrealized (6 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton dy
  (vars (m text) (a a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a-2) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-3) (b a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (3 0)) ((3 1) (5 0))
    ((4 1) (1 0)) ((5 1) (4 0)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation nonce-test (displaced 7 4 resp 2) m (6 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a-0 (pubk a)))
      (send (enc (enc m (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk a)) a-2 (pubk a)))
      (send (enc (enc m (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-3 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-3)) a (pubk a-3)))))
  (label 59)
  (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 (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))
  (defstrand resp 2 (m m) (a b) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (5 0)) ((4 1) (2 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 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 (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))))
    ((recv (enc (enc m (pubk a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b)))))
  (label 60)
  (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 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))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (4 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 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 (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))))
    ((recv (enc (enc m (pubk a)) a-3 (pubk a)))
      (send (enc (enc m (pubk a-3)) a (pubk a-3)))))
  (label 61)
  (parent 40)
  (seen 56)
  (unrealized)
  (comment "1 in cohort - 0 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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (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) (3 0)) ((0 0) (6 0)) ((1 1) (5 0))
    ((2 1) (0 1)) ((3 1) (4 0)) ((3 1) (5 0)) ((4 1) (2 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 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 (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))))
    ((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 62)
  (parent 40)
  (seen 37 58 59 61)
  (unrealized (6 0))
  (comment "6 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 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 b) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (6 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (4 0)) ((4 1) (2 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 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 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 63)
  (parent 41)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (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)) ((0 0) (6 0)) ((1 1) (2 0))
    ((2 1) (0 1)) ((3 1) (4 0)) ((4 1) (2 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 1 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 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))))
    ((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 65)
  (parent 41)
  (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 (cat (enc m (pubk b)) b)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (4 0))
    ((2 1) (3 0)) ((3 1) (0 1)) ((4 1) (0 1)) ((5 1) (4 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 66)
  (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 (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))
  (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)) ((0 0) (6 0)) ((1 1) (5 0))
    ((2 1) (0 1)) ((3 1) (4 0)) ((4 1) (2 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 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 (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))))
    ((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 67)
  (parent 44)
  (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 (cat (enc m (pubk b)) b)) (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) (4 0)) ((2 1) (3 0))
    ((3 1) (0 1)) ((4 1) (0 1)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1)))))
  (label 69)
  (parent 45)
  (seen 83)
  (unrealized)
  (comment "1 in cohort - 0 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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (defstrand resp 2 (m m) (a a-4) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (6 0)) ((4 1) (2 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 3 resp 2) m (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 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))))
    ((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-4 (pubk b)))
      (send (enc (enc m (pubk a-4)) b (pubk a-4)))))
  (label 70)
  (parent 46)
  (seen 73 100)
  (unrealized (6 0))
  (comment "7 in cohort - 5 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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (defstrand resp 2 (m m) (a a-4) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (6 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((4 1) (2 0)) ((5 1) (2 0)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 1 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 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))))
    ((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-4 (pubk b)))
      (send (enc (enc m (pubk a-4)) b (pubk a-4)))))
  (label 72)
  (parent 46)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (3 0)) ((3 1) (5 0))
    ((4 1) (1 0)) ((5 1) (4 0)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation nonce-test (displaced 7 4 resp 2) m (6 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces
    ((send (enc (enc m (pubk a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a-0 (pubk a)))
      (send (enc (enc m (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk a)) a-2 (pubk a)))
      (send (enc (enc m (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc m (pubk a)) a-3 (pubk a)))
      (send (enc (enc m (pubk a-3)) a (pubk a-3)))))
  (label 73)
  (parent 46)
  (seen 30)
  (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) (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) (2 0)) ((1 1) (3 0)) ((2 1) (4 0))
    ((3 1) (0 1)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 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 74)
  (parent 47)
  (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 (cat (enc m (pubk b)) b)) (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) (4 0)) ((2 1) (4 0))
    ((3 1) (0 1)) ((4 1) (3 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1)))))
  (label 75)
  (parent 48)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-4) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (4 0)) ((2 1) (0 1))
    ((3 1) (6 0)) ((4 1) (2 0)) ((5 1) (4 0)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (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 (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))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-4 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-4)) a (pubk a-4)))))
  (label 76)
  (parent 49)
  (seen 105 107)
  (unrealized (5 0))
  (comment "7 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 (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))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-4) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (6 0)) ((2 1) (0 1))
    ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (4 0)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 1 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 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))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-4 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-4)) a (pubk a-4)))))
  (label 77)
  (parent 49)
  (unrealized (6 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) (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))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (4 0)) ((2 1) (4 0))
    ((3 1) (0 1)) ((4 1) (3 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 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-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2)))))
  (label 78)
  (parent 50)
  (seen 79)
  (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 (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (3 0)) ((2 1) (0 1)) ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 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 (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)))))
  (label 79)
  (parent 51)
  (seen 8)
  (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 a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a b) (b a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (3 0)) ((2 1) (4 0))
    ((3 1) (1 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 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 a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b)))))
  (label 80)
  (parent 52)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a a-0 name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((1 1) (3 0)) ((2 1) (0 1))
    ((3 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-0 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a)))))
  (label 81)
  (parent 53)
  (seen 14)
  (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) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a b) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (3 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 (2 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 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 a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b)))))
  (label 82)
  (parent 54)
  (seen 111)
  (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 (cat (enc m (pubk b)) b)) (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) (3 0)) ((2 1) (0 1))
    ((3 1) (0 1)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1)))))
  (label 83)
  (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 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 a))
  (precedes ((0 0) (1 0)) ((1 1) (2 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 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 a)) a-1 (pubk a)))
      (send (enc (enc m (pubk a-1)) a (pubk a-1)))))
  (label 84)
  (parent 56)
  (seen 35)
  (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 (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-3) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (6 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-4 b)) m (6 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 (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-1)) b (pubk a-1))))
    ((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)) b (pubk b)) a-3 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-3)) b (pubk a-3)))))
  (label 85)
  (parent 58)
  (seen 37)
  (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 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 m) (a a-2) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-3) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 3 resp 2) m (6 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 (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 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)))))
  (label 86)
  (parent 58)
  (seen 56)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

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

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

(defskeleton dy
  (vars (m text) (a b a-0 a-1 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a b) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (3 0)) ((3 1) (0 1)) ((4 1) (0 1)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 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 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 93)
  (parent 65)
  (seen 114)
  (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 (cat (enc m (pubk b)) b)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (4 0)) ((1 1) (3 0))
    ((2 1) (0 1)) ((3 1) (0 1)) ((4 1) (3 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 94)
  (parent 66)
  (seen 10)
  (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) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (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) (2 0)) ((0 0) (5 0)) ((1 1) (4 0))
    ((2 1) (3 0)) ((3 1) (0 1)) ((4 1) (0 1)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 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 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 95)
  (parent 67)
  (seen 114)
  (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 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))
  (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) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (6 0)) ((4 1) (2 0)) ((5 1) (2 0))
    ((6 1) (5 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 (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))))
    ((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 96)
  (parent 70)
  (seen 117)
  (unrealized (5 0))
  (comment "5 in cohort - 4 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 (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (6 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (6 0)) ((4 1) (2 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 1 resp 2) m (6 0)
    (enc (enc m (pubk a-4)) b (pubk a-4))
    (enc (enc m (pubk b)) a-4 (pubk b)))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3)))))
  (label 97)
  (parent 70)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (defstrand resp 2 (m m) (a a-4) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((4 1) (6 0)) ((5 1) (2 0)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 4 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 (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))))
    ((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-4 (pubk b)))
      (send (enc (enc m (pubk a-4)) b (pubk a-4)))))
  (label 98)
  (parent 70)
  (seen 73 123)
  (unrealized (6 0))
  (comment "7 in cohort - 3 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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (defstrand resp 2 (m m) (a a-4) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (6 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (6 0)) ((4 1) (2 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 1 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 (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))))
    ((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-4 (pubk b)))
      (send (enc (enc m (pubk a-4)) b (pubk a-4)))))
  (label 100)
  (parent 70)
  (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) (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 a))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (5 0)) ((2 1) (3 0))
    ((3 1) (0 1)) ((4 1) (0 1)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 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 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)))))
  (label 101)
  (parent 72)
  (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) (1 0)) ((1 1) (3 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 m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (label 102)
  (parent 74)
  (seen 35)
  (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 (cat (enc m (pubk b)) b)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (3 0)) ((2 1) (0 1)) ((3 1) (2 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1)))))
  (label 103)
  (parent 75)
  (seen 112)
  (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 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))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-3) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (4 0)) ((2 1) (0 1))
    ((3 1) (6 0)) ((4 1) (2 0)) ((5 1) (4 0)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-4 a)) m (5 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 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))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-3 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-3)) a (pubk a-3)))))
  (label 104)
  (parent 76)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dy
  (vars (m text) (a a-0 a-1 a-2 a-3 name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a-2) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-3) (b a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (5 0)) ((3 1) (1 0))
    ((4 1) (3 0)) ((5 1) (4 0)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation nonce-test (contracted (b a) (a-4 a-3)) m (5 0)
    (enc m (pubk a)) (enc (enc m (pubk a)) a (pubk a)))
  (traces
    ((send (enc (enc m (pubk a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a-0 (pubk a)))
      (send (enc (enc m (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc m (pubk a)) a-2 (pubk a)))
      (send (enc (enc m (pubk a-2)) a (pubk a-2))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-3 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-3)) a (pubk a-3)))))
  (label 105)
  (parent 76)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-4) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (6 0)) ((4 1) (2 0)) ((5 1) (4 0)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 1 resp 2) m (5 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 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))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-4 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-4)) a (pubk a-4)))))
  (label 107)
  (parent 76)
  (unrealized)
  (comment "1 in cohort - 1 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 (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-3) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (6 0)) ((2 1) (0 1))
    ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (4 0)) ((6 1) (5 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-4 b)) m (6 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 (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-1)) b (pubk a-1))))
    ((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)) b (pubk b)) a-3 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-3)) b (pubk a-3)))))
  (label 108)
  (parent 77)
  (seen 48)
  (unrealized)
  (comment "1 in cohort - 0 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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-4) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (6 0)) ((2 1) (0 1))
    ((3 1) (6 0)) ((4 1) (2 0)) ((5 1) (4 0)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 3 resp 2) m (6 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 (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))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-4 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-4)) a (pubk a-4)))))
  (label 109)
  (parent 77)
  (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 b) (b a))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((1 1) (3 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 (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 a)) b (pubk a)))
      (send (enc (enc m (pubk b)) a (pubk b)))))
  (label 111)
  (parent 80)
  (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 (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0)))))
  (label 112)
  (parent 83)
  (seen 4)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

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

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

(defskeleton dy
  (vars (m text) (a b a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (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) (5 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (6 0)) ((4 1) (2 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 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 (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))))
    ((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 116)
  (parent 96)
  (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 (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (6 0)) ((4 1) (2 0)) ((5 1) (2 0))
    ((6 1) (5 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation nonce-test (contracted (a-3 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 (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-1 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 117)
  (parent 96)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (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) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((3 1) (6 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 (displaced 7 4 resp 2) m (5 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 (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))))
    ((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 118)
  (parent 96)
  (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 (cat (enc m (pubk b)) b)) (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 m) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (5 0)) ((2 1) (3 0))
    ((2 1) (5 0)) ((3 1) (0 1)) ((4 1) (0 1)) ((5 1) (4 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2)))))
  (label 120)
  (parent 97)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (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) (3 0)) ((1 1) (5 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((4 1) (6 0)) ((5 1) (2 0)) ((6 1) (5 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 (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))))
    ((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 121)
  (parent 98)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (defstrand resp 2 (m m) (a a-4) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((1 1) (6 0)) ((2 1) (0 1))
    ((3 1) (4 0)) ((4 1) (6 0)) ((5 1) (2 0)) ((6 1) (5 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 7 1 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 (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))))
    ((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-4 (pubk b)))
      (send (enc (enc m (pubk a-4)) b (pubk a-4)))))
  (label 123)
  (parent 98)
  (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) (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 a))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (5 0)) ((2 1) (3 0))
    ((2 1) (5 0)) ((3 1) (0 1)) ((4 1) (0 1)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 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 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)))))
  (label 124)
  (parent 100)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

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

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

(defskeleton dy
  (vars (m text) (a a-0 a-1 a-2 name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a-1) (b a))
  (defstrand resp 2 (m (cat (enc m (pubk a)) a)) (a a-2) (b a))
  (precedes ((0 0) (1 0)) ((1 1) (4 0)) ((2 1) (0 1)) ((3 1) (2 0))
    ((4 1) (3 0)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-0 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-0)) a (pubk a-0))))
    ((recv (enc (enc m (pubk a)) a-1 (pubk a)))
      (send (enc (enc m (pubk a-1)) a (pubk a-1))))
    ((recv (enc (enc (enc m (pubk a)) a (pubk a)) a-2 (pubk a)))
      (send (enc (enc (enc m (pubk a)) a (pubk a-2)) a (pubk a-2)))))
  (label 127)
  (parent 105)
  (seen 103)
  (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 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-2) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-3) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (4 0)) ((2 1) (5 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 (2 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 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-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (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)))))
  (label 128)
  (parent 107)
  (seen 21)
  (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 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-2) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-3) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (5 0)) ((2 1) (5 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 (2 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 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-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (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)))))
  (label 129)
  (parent 109)
  (seen 23)
  (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 (2 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 130)
  (parent 111)
  (seen 2)
  (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 (2 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 131)
  (parent 114)
  (seen 130)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dy
  (vars (m text) (a name))
  (defstrand init 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (defstrand resp 2 (m m) (a a) (b a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig m)
  (operation generalization deleted (1 0))
  (traces
    ((send (enc (enc m (pubk a)) a (pubk a)))
      (recv (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a))))
    ((recv (enc (enc m (pubk a)) a (pubk a)))
      (send (enc (enc m (pubk a)) a (pubk a)))))
  (label 132)
  (parent 115)
  (seen 17)
  (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) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-1) (b a))
  (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) (2 0)) ((1 1) (4 0)) ((2 1) (3 0))
    ((2 1) (5 0)) ((3 1) (0 1)) ((4 1) (0 1)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 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 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 133)
  (parent 116)
  (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 (cat (enc m (pubk b)) b)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m m) (a b) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (4 0)) ((2 1) (3 0))
    ((2 1) (5 0)) ((3 1) (0 1)) ((4 1) (0 1)) ((5 1) (4 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc m (pubk b)) b (pubk b)))
      (send (enc (enc m (pubk b)) b (pubk b)))))
  (label 134)
  (parent 117)
  (seen 94)
  (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 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 a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (3 0)) ((2 1) (5 0))
    ((3 1) (4 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-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 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)))))
  (label 135)
  (parent 118)
  (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 (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))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (4 0)) ((2 1) (0 1))
    ((3 1) (0 1)) ((4 1) (3 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1))))
    ((recv (enc (enc m (pubk b)) a-2 (pubk b)))
      (send (enc (enc m (pubk a-2)) b (pubk a-2)))))
  (label 136)
  (parent 120)
  (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 m) (a a-2) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (3 0)) ((3 1) (5 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-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 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)))))
  (label 137)
  (parent 121)
  (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) (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 a))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (5 0)) ((2 1) (3 0))
    ((3 1) (5 0)) ((4 1) (0 1)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 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 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)))))
  (label 138)
  (parent 123)
  (seen 139)
  (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) (b b))
  (defstrand resp 2 (m m) (a a-1) (b a))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (4 0)) ((2 1) (4 0))
    ((3 1) (0 1)) ((4 1) (3 0)))
  (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 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 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)))))
  (label 139)
  (parent 124)
  (seen 140)
  (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 a))
  (defstrand resp 2 (m m) (a a-2) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (3 0)) ((2 1) (0 1)) ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 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 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)))))
  (label 140)
  (parent 125)
  (seen 8)
  (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) (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 a)) b)) (a a-1) (b a))
  (precedes ((0 0) (1 0)) ((1 1) (4 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 (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 a)) b (pubk a)) a-1 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-1)) a (pubk a-1)))))
  (label 141)
  (parent 126)
  (seen 25)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

(defskeleton dy
  (vars (m text) (b a a-0 a-1 name))
  (defstrand init 2 (m m) (a b) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk b)) b)) (a a) (b b))
  (defstrand resp 2 (m m) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (3 0)) ((2 1) (0 1)) ((3 1) (2 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 0))
  (traces
    ((send (enc (enc m (pubk b)) b (pubk b)))
      (recv (enc (enc m (pubk b)) b (pubk b))))
    ((recv (enc (enc (enc m (pubk b)) b (pubk b)) a (pubk b)))
      (send (enc (enc (enc m (pubk b)) b (pubk a)) b (pubk a))))
    ((recv (enc (enc m (pubk b)) a-0 (pubk b)))
      (send (enc (enc m (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 144)
  (parent 136)
  (seen 112)
  (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) (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 a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (4 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 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 a)) a-1 (pubk a)))
      (send (enc (enc m (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 145)
  (parent 137)
  (seen 25)
  (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)) ((1 1) (3 0)) ((2 1) (0 1)) ((3 1) (2 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation generalization deleted (2 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 146)
  (parent 142)
  (seen 130)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton dy
  (vars (m text) (a b a-0 name))
  (defstrand init 2 (m m) (a a) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-0) (b a))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((1 1) (3 0)) ((2 1) (0 1))
    ((3 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 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 147)
  (parent 143)
  (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 m) (a a) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-2) (b a))
  (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) (3 0)) ((0 0) (6 0)) ((0 0) (7 0))
    ((1 1) (0 1)) ((2 1) (0 1)) ((3 1) (4 0)) ((4 1) (2 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 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))))
    ((recv (enc (enc m (pubk a)) a-3 (pubk a)))
      (send (enc (enc m (pubk a-3)) a (pubk a-3))))
    ((recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-4 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-4)) a (pubk a-4)))))
  (label 43)
  (parent 28)
  (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 (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))
  (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) (3 0)) ((0 0) (7 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (4 0)) ((3 1) (5 0)) ((4 1) (2 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 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))))
    ((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 57)
  (parent 39)
  (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 (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))
  (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) (3 0)) ((0 0) (6 0)) ((0 0) (7 0))
    ((1 1) (5 0)) ((2 1) (0 1)) ((3 1) (4 0)) ((4 1) (2 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 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 (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))))
    ((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 68)
  (parent 44)
  (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 (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))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (defstrand resp 2 (m m) (a a-4) (b b))
  (defstrand resp 2 (m m) (a a) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (7 0)) ((1 1) (5 0))
    ((2 1) (0 1)) ((3 1) (4 0)) ((4 1) (2 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 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))))
    ((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-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 71)
  (parent 46)
  (unrealized (6 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 (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))
  (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-5) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (7 0)) ((1 1) (6 0))
    ((2 1) (0 1)) ((3 1) (4 0)) ((3 1) (5 0)) ((4 1) (2 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 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))))
    ((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))))
    ((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-5 (pubk b)))
      (send (enc (enc m (pubk a-5)) b (pubk a-5)))))
  (label 87)
  (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 (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))
  (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) (3 0)) ((0 0) (7 0)) ((1 1) (5 0))
    ((2 1) (0 1)) ((3 1) (4 0)) ((3 1) (5 0)) ((4 1) (2 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 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))))
    ((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 90)
  (parent 62)
  (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 (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))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (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) (1 0)) ((0 0) (3 0)) ((0 0) (7 0)) ((1 1) (5 0))
    ((2 1) (0 1)) ((3 1) (4 0)) ((3 1) (6 0)) ((4 1) (2 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 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))))
    ((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-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 99)
  (parent 70)
  (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 (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))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-4) (b a))
  (defstrand resp 2 (m m) (a a-5) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (7 0)) ((1 1) (4 0))
    ((2 1) (0 1)) ((3 1) (6 0)) ((4 1) (2 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 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 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))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-4 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-4)) a (pubk a-4))))
    ((recv (enc (enc m (pubk a)) a-5 (pubk a)))
      (send (enc (enc m (pubk a-5)) a (pubk a-5)))))
  (label 106)
  (parent 76)
  (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 (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))
  (defstrand resp 2 (m m) (a a-3) (b b))
  (defstrand resp 2 (m (cat (enc m (pubk a)) b)) (a a-4) (b a))
  (defstrand resp 2 (m m) (a a-5) (b b))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (7 0)) ((1 1) (6 0))
    ((2 1) (0 1)) ((3 1) (5 0)) ((4 1) (2 0)) ((5 1) (4 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 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))))
    ((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))))
    ((recv (enc (enc m (pubk b)) a-3 (pubk b)))
      (send (enc (enc m (pubk a-3)) b (pubk a-3))))
    ((recv (enc (enc (enc m (pubk a)) b (pubk a)) a-4 (pubk a)))
      (send (enc (enc (enc m (pubk a)) b (pubk a-4)) a (pubk a-4))))
    ((recv (enc (enc m (pubk b)) a-5 (pubk b)))
      (send (enc (enc m (pubk a-5)) b (pubk a-5)))))
  (label 110)
  (parent 77)
  (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 (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))
  (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) (3 0)) ((0 0) (7 0)) ((1 1) (5 0))
    ((2 1) (0 1)) ((3 1) (4 0)) ((3 1) (6 0)) ((4 1) (2 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 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 (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))))
    ((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 119)
  (parent 96)
  (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 (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))
  (defstrand resp 2 (m m) (a a-3) (b a))
  (defstrand resp 2 (m m) (a a-4) (b b))
  (defstrand resp 2 (m m) (a a-5) (b a))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (7 0)) ((1 1) (5 0))
    ((2 1) (0 1)) ((3 1) (4 0)) ((4 1) (6 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 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 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))))
    ((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-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 122)
  (parent 98)
  (unrealized (7 0))
  (comment "aborted"))