(herald "bltk example" (algebra diffie-hellman) (limit 100))

(comment "CPSA 3.4.0")
(comment "All input read from bltk_example.lsp")
(comment "Step count limited to 100")

(defprotocol bltks diffie-hellman
  (defrole init
    (vars (I R name) (n m data))
    (trace (send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    (uniq-orig n))
  (defrole resp
    (vars (I R name) (n m data))
    (trace (recv (enc I R n (bltk I R))) (send (enc R I m (bltk I R))))
    (uniq-orig m)))

(defskeleton bltks
  (vars (n m data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (non-orig (bltk I R))
  (uniq-orig n)
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R)))))
  (label 0)
  (unrealized (0 1))
  (origs (n (0 0)))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton bltks
  (vars (n m data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand init 1 (n m) (I R) (R I))
  (precedes ((1 0) (0 1)))
  (non-orig (bltk I R))
  (uniq-orig n m)
  (operation encryption-test (added-strand init 1)
    (enc R I m (bltk I R)) (0 1))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((send (enc R I m (bltk I R)))))
  (label 1)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (m (1 0)) (n (0 0))))

(defskeleton bltks
  (vars (n data) (I name))
  (defstrand init 2 (n n) (m n) (I I) (R I))
  (non-orig (bltk I I))
  (uniq-orig n)
  (operation encryption-test (displaced 1 0 init 1)
    (enc I I m (bltk I I)) (0 1))
  (traces ((send (enc I I n (bltk I I))) (recv (enc I I n (bltk I I)))))
  (label 2)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R I) (n n) (m n))))
  (origs (n (0 0))))

(defskeleton bltks
  (vars (n m n-0 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (precedes ((1 1) (0 1)))
  (non-orig (bltk I R))
  (uniq-orig n m)
  (operation encryption-test (added-strand resp 2)
    (enc R I m (bltk I R)) (0 1))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R)))))
  (label 3)
  (parent 0)
  (unrealized (1 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton bltks
  (vars (n m data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n) (m m) (I I) (R R))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (bltk I R))
  (uniq-orig n m)
  (operation encryption-test (displaced 2 0 init 1)
    (enc I R n-0 (bltk I R)) (1 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n (bltk I R))) (send (enc R I m (bltk I R)))))
  (label 4)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n (0 0)) (m (1 1))))

(defskeleton bltks
  (vars (n m n-0 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand init 1 (n n-0) (I I) (R R))
  (precedes ((1 1) (0 1)) ((2 0) (1 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0)
  (operation encryption-test (added-strand init 1)
    (enc I R n-0 (bltk I R)) (1 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((send (enc I R n-0 (bltk I R)))))
  (label 5)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n-0 (2 0)) (m (1 1)) (n (0 0))))

(defskeleton bltks
  (vars (n m n-0 n-1 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0)
  (operation encryption-test (added-strand resp 2)
    (enc I R n-0 (bltk I R)) (1 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R)))))
  (label 6)
  (parent 3)
  (unrealized (2 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton bltks
  (vars (n m n-0 data) (I name))
  (defstrand init 2 (n n) (m m) (I I) (R I))
  (defstrand resp 2 (n n-0) (m m) (I I) (R I))
  (defstrand resp 2 (n n) (m n-0) (I I) (R I))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (bltk I I))
  (uniq-orig n m n-0)
  (operation encryption-test (displaced 3 0 init 1)
    (enc R I n-1 (bltk I R)) (2 0))
  (traces ((send (enc I I n (bltk I I))) (recv (enc I I m (bltk I I))))
    ((recv (enc I I n-0 (bltk I I))) (send (enc I I m (bltk I I))))
    ((recv (enc I I n (bltk I I))) (send (enc I I n-0 (bltk I I)))))
  (label 7)
  (parent 6)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R I) (n n) (m m))))
  (origs (n (0 0)) (n-0 (2 1)) (m (1 1))))

(defskeleton bltks
  (vars (n m n-0 n-1 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand init 1 (n n-1) (I R) (R I))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 0) (2 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1)
  (operation encryption-test (added-strand init 1)
    (enc R I n-1 (bltk I R)) (2 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((send (enc R I n-1 (bltk I R)))))
  (label 8)
  (parent 6)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n-1 (3 0)) (n-0 (2 1)) (m (1 1)) (n (0 0))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1)
  (operation encryption-test (added-strand resp 2)
    (enc R I n-1 (bltk I R)) (2 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R)))))
  (label 9)
  (parent 6)
  (unrealized (3 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton bltks
  (vars (n m n-0 n-1 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n) (m n-1) (I I) (R R))
  (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1)
  (operation encryption-test (displaced 4 0 init 1)
    (enc I R n-2 (bltk I R)) (3 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n (bltk I R))) (send (enc R I n-1 (bltk I R)))))
  (label 10)
  (parent 9)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n (0 0)) (n-1 (3 1)) (n-0 (2 1)) (m (1 1))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand init 1 (n n-2) (I I) (R R))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 0) (3 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2)
  (operation encryption-test (added-strand init 1)
    (enc I R n-2 (bltk I R)) (3 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((send (enc I R n-2 (bltk I R)))))
  (label 11)
  (parent 9)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n-2 (4 0)) (n-1 (3 1)) (n-0 (2 1)) (m (1 1)) (n (0 0))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2)
  (operation encryption-test (added-strand resp 2)
    (enc I R n-2 (bltk I R)) (3 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R)))))
  (label 12)
  (parent 9)
  (unrealized (4 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 data) (I name))
  (defstrand init 2 (n n) (m m) (I I) (R I))
  (defstrand resp 2 (n n-0) (m m) (I I) (R I))
  (defstrand resp 2 (n n-1) (m n-0) (I I) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R I))
  (defstrand resp 2 (n n) (m n-2) (I I) (R I))
  (precedes ((0 0) (4 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (3 0)))
  (non-orig (bltk I I))
  (uniq-orig n m n-0 n-1 n-2)
  (operation encryption-test (displaced 5 0 init 1)
    (enc R I n-3 (bltk I R)) (4 0))
  (traces ((send (enc I I n (bltk I I))) (recv (enc I I m (bltk I I))))
    ((recv (enc I I n-0 (bltk I I))) (send (enc I I m (bltk I I))))
    ((recv (enc I I n-1 (bltk I I))) (send (enc I I n-0 (bltk I I))))
    ((recv (enc I I n-2 (bltk I I))) (send (enc I I n-1 (bltk I I))))
    ((recv (enc I I n (bltk I I))) (send (enc I I n-2 (bltk I I)))))
  (label 13)
  (parent 12)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R I) (n n) (m m))))
  (origs (n (0 0)) (n-2 (4 1)) (n-1 (3 1)) (n-0 (2 1)) (m (1 1))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand init 1 (n n-3) (I R) (R I))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 0) (4 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3)
  (operation encryption-test (added-strand init 1)
    (enc R I n-3 (bltk I R)) (4 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((send (enc R I n-3 (bltk I R)))))
  (label 14)
  (parent 12)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n-3 (5 0)) (n-2 (4 1)) (n-1 (3 1)) (n-0 (2 1)) (m (1 1))
    (n (0 0))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3)
  (operation encryption-test (added-strand resp 2)
    (enc R I n-3 (bltk I R)) (4 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R)))))
  (label 15)
  (parent 12)
  (unrealized (5 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n) (m n-3) (I I) (R R))
  (precedes ((0 0) (5 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (3 0)) ((5 1) (4 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3)
  (operation encryption-test (displaced 6 0 init 1)
    (enc I R n-4 (bltk I R)) (5 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n (bltk I R))) (send (enc R I n-3 (bltk I R)))))
  (label 16)
  (parent 15)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n (0 0)) (n-3 (5 1)) (n-2 (4 1)) (n-1 (3 1)) (n-0 (2 1))
    (m (1 1))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand init 1 (n n-4) (I I) (R R))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)) ((6 0) (5 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4)
  (operation encryption-test (added-strand init 1)
    (enc I R n-4 (bltk I R)) (5 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((send (enc I R n-4 (bltk I R)))))
  (label 17)
  (parent 15)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n-4 (6 0)) (n-3 (5 1)) (n-2 (4 1)) (n-1 (3 1)) (n-0 (2 1))
    (m (1 1)) (n (0 0))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)) ((6 1) (5 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4)
  (operation encryption-test (added-strand resp 2)
    (enc I R n-4 (bltk I R)) (5 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R)))))
  (label 18)
  (parent 15)
  (unrealized (6 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 data) (I name))
  (defstrand init 2 (n n) (m m) (I I) (R I))
  (defstrand resp 2 (n n-0) (m m) (I I) (R I))
  (defstrand resp 2 (n n-1) (m n-0) (I I) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R I))
  (defstrand resp 2 (n n-3) (m n-2) (I I) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R I))
  (defstrand resp 2 (n n) (m n-4) (I I) (R I))
  (precedes ((0 0) (6 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (3 0)) ((5 1) (4 0)) ((6 1) (5 0)))
  (non-orig (bltk I I))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4)
  (operation encryption-test (displaced 7 0 init 1)
    (enc R I n-5 (bltk I R)) (6 0))
  (traces ((send (enc I I n (bltk I I))) (recv (enc I I m (bltk I I))))
    ((recv (enc I I n-0 (bltk I I))) (send (enc I I m (bltk I I))))
    ((recv (enc I I n-1 (bltk I I))) (send (enc I I n-0 (bltk I I))))
    ((recv (enc I I n-2 (bltk I I))) (send (enc I I n-1 (bltk I I))))
    ((recv (enc I I n-3 (bltk I I))) (send (enc I I n-2 (bltk I I))))
    ((recv (enc I I n-4 (bltk I I))) (send (enc I I n-3 (bltk I I))))
    ((recv (enc I I n (bltk I I))) (send (enc I I n-4 (bltk I I)))))
  (label 19)
  (parent 18)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R I) (n n) (m m))))
  (origs (n (0 0)) (n-4 (6 1)) (n-3 (5 1)) (n-2 (4 1)) (n-1 (3 1))
    (n-0 (2 1)) (m (1 1))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (defstrand init 1 (n n-5) (I R) (R I))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)) ((6 1) (5 0)) ((7 0) (6 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5)
  (operation encryption-test (added-strand init 1)
    (enc R I n-5 (bltk I R)) (6 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R))))
    ((send (enc R I n-5 (bltk I R)))))
  (label 20)
  (parent 18)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n-5 (7 0)) (n-4 (6 1)) (n-3 (5 1)) (n-2 (4 1)) (n-1 (3 1))
    (n-0 (2 1)) (m (1 1)) (n (0 0))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (defstrand resp 2 (n n-6) (m n-5) (I I) (R R))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5)
  (operation encryption-test (added-strand resp 2)
    (enc R I n-5 (bltk I R)) (6 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R))))
    ((recv (enc I R n-6 (bltk I R))) (send (enc R I n-5 (bltk I R)))))
  (label 21)
  (parent 18)
  (unrealized (7 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (defstrand resp 2 (n n) (m n-5) (I I) (R R))
  (precedes ((0 0) (7 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (3 0)) ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5)
  (operation encryption-test (displaced 8 0 init 1)
    (enc I R n-6 (bltk I R)) (7 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R))))
    ((recv (enc I R n (bltk I R))) (send (enc R I n-5 (bltk I R)))))
  (label 22)
  (parent 21)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n (0 0)) (n-5 (7 1)) (n-4 (6 1)) (n-3 (5 1)) (n-2 (4 1))
    (n-1 (3 1)) (n-0 (2 1)) (m (1 1))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (defstrand resp 2 (n n-6) (m n-5) (I I) (R R))
  (defstrand init 1 (n n-6) (I I) (R R))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0)) ((8 0) (7 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5 n-6)
  (operation encryption-test (added-strand init 1)
    (enc I R n-6 (bltk I R)) (7 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R))))
    ((recv (enc I R n-6 (bltk I R))) (send (enc R I n-5 (bltk I R))))
    ((send (enc I R n-6 (bltk I R)))))
  (label 23)
  (parent 21)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n-6 (8 0)) (n-5 (7 1)) (n-4 (6 1)) (n-3 (5 1)) (n-2 (4 1))
    (n-1 (3 1)) (n-0 (2 1)) (m (1 1)) (n (0 0))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (defstrand resp 2 (n n-6) (m n-5) (I I) (R R))
  (defstrand resp 2 (n n-7) (m n-6) (I R) (R I))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0)) ((8 1) (7 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5 n-6)
  (operation encryption-test (added-strand resp 2)
    (enc I R n-6 (bltk I R)) (7 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R))))
    ((recv (enc I R n-6 (bltk I R))) (send (enc R I n-5 (bltk I R))))
    ((recv (enc R I n-7 (bltk I R))) (send (enc I R n-6 (bltk I R)))))
  (label 24)
  (parent 21)
  (unrealized (8 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 data) (I name))
  (defstrand init 2 (n n) (m m) (I I) (R I))
  (defstrand resp 2 (n n-0) (m m) (I I) (R I))
  (defstrand resp 2 (n n-1) (m n-0) (I I) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R I))
  (defstrand resp 2 (n n-3) (m n-2) (I I) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R I))
  (defstrand resp 2 (n n-5) (m n-4) (I I) (R I))
  (defstrand resp 2 (n n-6) (m n-5) (I I) (R I))
  (defstrand resp 2 (n n) (m n-6) (I I) (R I))
  (precedes ((0 0) (8 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (3 0)) ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0))
    ((8 1) (7 0)))
  (non-orig (bltk I I))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5 n-6)
  (operation encryption-test (displaced 9 0 init 1)
    (enc R I n-7 (bltk I R)) (8 0))
  (traces ((send (enc I I n (bltk I I))) (recv (enc I I m (bltk I I))))
    ((recv (enc I I n-0 (bltk I I))) (send (enc I I m (bltk I I))))
    ((recv (enc I I n-1 (bltk I I))) (send (enc I I n-0 (bltk I I))))
    ((recv (enc I I n-2 (bltk I I))) (send (enc I I n-1 (bltk I I))))
    ((recv (enc I I n-3 (bltk I I))) (send (enc I I n-2 (bltk I I))))
    ((recv (enc I I n-4 (bltk I I))) (send (enc I I n-3 (bltk I I))))
    ((recv (enc I I n-5 (bltk I I))) (send (enc I I n-4 (bltk I I))))
    ((recv (enc I I n-6 (bltk I I))) (send (enc I I n-5 (bltk I I))))
    ((recv (enc I I n (bltk I I))) (send (enc I I n-6 (bltk I I)))))
  (label 25)
  (parent 24)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R I) (n n) (m m))))
  (origs (n (0 0)) (n-6 (8 1)) (n-5 (7 1)) (n-4 (6 1)) (n-3 (5 1))
    (n-2 (4 1)) (n-1 (3 1)) (n-0 (2 1)) (m (1 1))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (defstrand resp 2 (n n-6) (m n-5) (I I) (R R))
  (defstrand resp 2 (n n-7) (m n-6) (I R) (R I))
  (defstrand init 1 (n n-7) (I R) (R I))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0)) ((8 1) (7 0))
    ((9 0) (8 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7)
  (operation encryption-test (added-strand init 1)
    (enc R I n-7 (bltk I R)) (8 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R))))
    ((recv (enc I R n-6 (bltk I R))) (send (enc R I n-5 (bltk I R))))
    ((recv (enc R I n-7 (bltk I R))) (send (enc I R n-6 (bltk I R))))
    ((send (enc R I n-7 (bltk I R)))))
  (label 26)
  (parent 24)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n-7 (9 0)) (n-6 (8 1)) (n-5 (7 1)) (n-4 (6 1)) (n-3 (5 1))
    (n-2 (4 1)) (n-1 (3 1)) (n-0 (2 1)) (m (1 1)) (n (0 0))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 n-8 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (defstrand resp 2 (n n-6) (m n-5) (I I) (R R))
  (defstrand resp 2 (n n-7) (m n-6) (I R) (R I))
  (defstrand resp 2 (n n-8) (m n-7) (I I) (R R))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0)) ((8 1) (7 0))
    ((9 1) (8 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7)
  (operation encryption-test (added-strand resp 2)
    (enc R I n-7 (bltk I R)) (8 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R))))
    ((recv (enc I R n-6 (bltk I R))) (send (enc R I n-5 (bltk I R))))
    ((recv (enc R I n-7 (bltk I R))) (send (enc I R n-6 (bltk I R))))
    ((recv (enc I R n-8 (bltk I R))) (send (enc R I n-7 (bltk I R)))))
  (label 27)
  (parent 24)
  (unrealized (9 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (defstrand resp 2 (n n-6) (m n-5) (I I) (R R))
  (defstrand resp 2 (n n-7) (m n-6) (I R) (R I))
  (defstrand resp 2 (n n) (m n-7) (I I) (R R))
  (precedes ((0 0) (9 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (3 0)) ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0))
    ((8 1) (7 0)) ((9 1) (8 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7)
  (operation encryption-test (displaced 10 0 init 1)
    (enc I R n-8 (bltk I R)) (9 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R))))
    ((recv (enc I R n-6 (bltk I R))) (send (enc R I n-5 (bltk I R))))
    ((recv (enc R I n-7 (bltk I R))) (send (enc I R n-6 (bltk I R))))
    ((recv (enc I R n (bltk I R))) (send (enc R I n-7 (bltk I R)))))
  (label 28)
  (parent 27)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n (0 0)) (n-7 (9 1)) (n-6 (8 1)) (n-5 (7 1)) (n-4 (6 1))
    (n-3 (5 1)) (n-2 (4 1)) (n-1 (3 1)) (n-0 (2 1)) (m (1 1))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 n-8 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (defstrand resp 2 (n n-6) (m n-5) (I I) (R R))
  (defstrand resp 2 (n n-7) (m n-6) (I R) (R I))
  (defstrand resp 2 (n n-8) (m n-7) (I I) (R R))
  (defstrand init 1 (n n-8) (I I) (R R))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0)) ((8 1) (7 0))
    ((9 1) (8 0)) ((10 0) (9 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 n-8)
  (operation encryption-test (added-strand init 1)
    (enc I R n-8 (bltk I R)) (9 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R))))
    ((recv (enc I R n-6 (bltk I R))) (send (enc R I n-5 (bltk I R))))
    ((recv (enc R I n-7 (bltk I R))) (send (enc I R n-6 (bltk I R))))
    ((recv (enc I R n-8 (bltk I R))) (send (enc R I n-7 (bltk I R))))
    ((send (enc I R n-8 (bltk I R)))))
  (label 29)
  (parent 27)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R R) (n n) (m m))))
  (origs (n-8 (10 0)) (n-7 (9 1)) (n-6 (8 1)) (n-5 (7 1)) (n-4 (6 1))
    (n-3 (5 1)) (n-2 (4 1)) (n-1 (3 1)) (n-0 (2 1)) (m (1 1))
    (n (0 0))))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 n-8 n-9 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (defstrand resp 2 (n n-6) (m n-5) (I I) (R R))
  (defstrand resp 2 (n n-7) (m n-6) (I R) (R I))
  (defstrand resp 2 (n n-8) (m n-7) (I I) (R R))
  (defstrand resp 2 (n n-9) (m n-8) (I R) (R I))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0)) ((8 1) (7 0))
    ((9 1) (8 0)) ((10 1) (9 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 n-8)
  (operation encryption-test (added-strand resp 2)
    (enc I R n-8 (bltk I R)) (9 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R))))
    ((recv (enc I R n-6 (bltk I R))) (send (enc R I n-5 (bltk I R))))
    ((recv (enc R I n-7 (bltk I R))) (send (enc I R n-6 (bltk I R))))
    ((recv (enc I R n-8 (bltk I R))) (send (enc R I n-7 (bltk I R))))
    ((recv (enc R I n-9 (bltk I R))) (send (enc I R n-8 (bltk I R)))))
  (label 30)
  (parent 27)
  (unrealized (10 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 n-8 data) (I name))
  (defstrand init 2 (n n) (m m) (I I) (R I))
  (defstrand resp 2 (n n-0) (m m) (I I) (R I))
  (defstrand resp 2 (n n-1) (m n-0) (I I) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R I))
  (defstrand resp 2 (n n-3) (m n-2) (I I) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R I))
  (defstrand resp 2 (n n-5) (m n-4) (I I) (R I))
  (defstrand resp 2 (n n-6) (m n-5) (I I) (R I))
  (defstrand resp 2 (n n-7) (m n-6) (I I) (R I))
  (defstrand resp 2 (n n-8) (m n-7) (I I) (R I))
  (defstrand resp 2 (n n) (m n-8) (I I) (R I))
  (precedes ((0 0) (10 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (3 0)) ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0))
    ((8 1) (7 0)) ((9 1) (8 0)) ((10 1) (9 0)))
  (non-orig (bltk I I))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 n-8)
  (operation encryption-test (displaced 11 0 init 1)
    (enc R I n-9 (bltk I R)) (10 0))
  (traces ((send (enc I I n (bltk I I))) (recv (enc I I m (bltk I I))))
    ((recv (enc I I n-0 (bltk I I))) (send (enc I I m (bltk I I))))
    ((recv (enc I I n-1 (bltk I I))) (send (enc I I n-0 (bltk I I))))
    ((recv (enc I I n-2 (bltk I I))) (send (enc I I n-1 (bltk I I))))
    ((recv (enc I I n-3 (bltk I I))) (send (enc I I n-2 (bltk I I))))
    ((recv (enc I I n-4 (bltk I I))) (send (enc I I n-3 (bltk I I))))
    ((recv (enc I I n-5 (bltk I I))) (send (enc I I n-4 (bltk I I))))
    ((recv (enc I I n-6 (bltk I I))) (send (enc I I n-5 (bltk I I))))
    ((recv (enc I I n-7 (bltk I I))) (send (enc I I n-6 (bltk I I))))
    ((recv (enc I I n-8 (bltk I I))) (send (enc I I n-7 (bltk I I))))
    ((recv (enc I I n (bltk I I))) (send (enc I I n-8 (bltk I I)))))
  (label 31)
  (parent 30)
  (unrealized)
  (shape)
  (maps ((0) ((I I) (R I) (n n) (m m))))
  (origs (n (0 0)) (n-8 (10 1)) (n-7 (9 1)) (n-6 (8 1)) (n-5 (7 1))
    (n-4 (6 1)) (n-3 (5 1)) (n-2 (4 1)) (n-1 (3 1)) (n-0 (2 1))
    (m (1 1))))

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

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 n-8 n-9 data) (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (defstrand resp 2 (n n-6) (m n-5) (I I) (R R))
  (defstrand resp 2 (n n-7) (m n-6) (I R) (R I))
  (defstrand resp 2 (n n-8) (m n-7) (I I) (R R))
  (defstrand resp 2 (n n-9) (m n-8) (I R) (R I))
  (defstrand init 1 (n n-9) (I R) (R I))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0)) ((8 1) (7 0))
    ((9 1) (8 0)) ((10 1) (9 0)) ((11 0) (10 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 n-8 n-9)
  (operation encryption-test (added-strand init 1)
    (enc R I n-9 (bltk I R)) (10 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R))))
    ((recv (enc I R n-6 (bltk I R))) (send (enc R I n-5 (bltk I R))))
    ((recv (enc R I n-7 (bltk I R))) (send (enc I R n-6 (bltk I R))))
    ((recv (enc I R n-8 (bltk I R))) (send (enc R I n-7 (bltk I R))))
    ((recv (enc R I n-9 (bltk I R))) (send (enc I R n-8 (bltk I R))))
    ((send (enc R I n-9 (bltk I R)))))
  (label 32)
  (parent 30)
  (unrealized)
  (comment "aborted"))

(defskeleton bltks
  (vars (n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 n-8 n-9 n-10 data)
    (I R name))
  (defstrand init 2 (n n) (m m) (I I) (R R))
  (defstrand resp 2 (n n-0) (m m) (I I) (R R))
  (defstrand resp 2 (n n-1) (m n-0) (I R) (R I))
  (defstrand resp 2 (n n-2) (m n-1) (I I) (R R))
  (defstrand resp 2 (n n-3) (m n-2) (I R) (R I))
  (defstrand resp 2 (n n-4) (m n-3) (I I) (R R))
  (defstrand resp 2 (n n-5) (m n-4) (I R) (R I))
  (defstrand resp 2 (n n-6) (m n-5) (I I) (R R))
  (defstrand resp 2 (n n-7) (m n-6) (I R) (R I))
  (defstrand resp 2 (n n-8) (m n-7) (I I) (R R))
  (defstrand resp 2 (n n-9) (m n-8) (I R) (R I))
  (defstrand resp 2 (n n-10) (m n-9) (I I) (R R))
  (precedes ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 1) (3 0))
    ((5 1) (4 0)) ((6 1) (5 0)) ((7 1) (6 0)) ((8 1) (7 0))
    ((9 1) (8 0)) ((10 1) (9 0)) ((11 1) (10 0)))
  (non-orig (bltk I R))
  (uniq-orig n m n-0 n-1 n-2 n-3 n-4 n-5 n-6 n-7 n-8 n-9)
  (operation encryption-test (added-strand resp 2)
    (enc R I n-9 (bltk I R)) (10 0))
  (traces ((send (enc I R n (bltk I R))) (recv (enc R I m (bltk I R))))
    ((recv (enc I R n-0 (bltk I R))) (send (enc R I m (bltk I R))))
    ((recv (enc R I n-1 (bltk I R))) (send (enc I R n-0 (bltk I R))))
    ((recv (enc I R n-2 (bltk I R))) (send (enc R I n-1 (bltk I R))))
    ((recv (enc R I n-3 (bltk I R))) (send (enc I R n-2 (bltk I R))))
    ((recv (enc I R n-4 (bltk I R))) (send (enc R I n-3 (bltk I R))))
    ((recv (enc R I n-5 (bltk I R))) (send (enc I R n-4 (bltk I R))))
    ((recv (enc I R n-6 (bltk I R))) (send (enc R I n-5 (bltk I R))))
    ((recv (enc R I n-7 (bltk I R))) (send (enc I R n-6 (bltk I R))))
    ((recv (enc I R n-8 (bltk I R))) (send (enc R I n-7 (bltk I R))))
    ((recv (enc R I n-9 (bltk I R))) (send (enc I R n-8 (bltk I R))))
    ((recv (enc I R n-10 (bltk I R))) (send (enc R I n-9 (bltk I R)))))
  (label 33)
  (parent 30)
  (unrealized (11 0))
  (comment "aborted"))