(comment "CPSA 2.1.1")
(comment "All input read")

(defprotocol nsl4cm basic
  (defrole init
    (vars (a b c d name) (na nb nc nd text))
    (trace (send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b)))))
  (defrole resp1
    (vars (a b c d name) (na nb nc nd text))
    (trace (recv (enc a c d na (pubk b)))
      (send (enc a b d na nb (pubk c))) (recv (enc nb nc nd (pubk b)))
      (send (enc nc nd (pubk c)))))
  (defrole resp2
    (vars (a b c d name) (na nb nc nd text))
    (trace (recv (enc a b d na nb (pubk c)))
      (send (enc a b c na nb nc (pubk d))) (recv (enc nc nd (pubk c)))
      (send (enc nd (pubk d)))))
  (defrole resp3
    (vars (a b c d name) (na nb nc nd text))
    (trace (recv (enc a b c na nb nc (pubk d)))
      (send (enc b c d na nb nc nd (pubk a)))
      (recv (enc nd (pubk d))))))

(defskeleton nsl4cm
  (vars (na nb nc nd text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b)))))
  (label 0)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nb-0 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp1 2) na (0 1)
    (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b)))
      (send (enc a b d na nb-0 (pubk c)))))
  (label 1)
  (parent 0)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nb-0 nc-0 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp2 2) na (0 1)
    (enc a b d na nb-0 (pubk c)) (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d)))))
  (label 2)
  (parent 1)
  (unrealized (0 1) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nb-0 nc-0 nb-1 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (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) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp1 2) na (2 0)
    (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b)))
      (send (enc a b d na nb-1 (pubk c)))))
  (label 3)
  (parent 2)
  (unrealized (0 1) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nc-0 nb-0 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (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) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (contracted (nb-1 nb-0)) na (2 0)
    (enc a b d na nb-0 (pubk c)) (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b)))
      (send (enc a b d na nb-0 (pubk c)))))
  (label 4)
  (parent 3)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nb-0 nc-0 nb-1 nc-1 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-1) (nc nc-1) (a a) (b b) (c c)
    (d d))
  (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) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp2 2) na (2 0)
    (enc a b d na nb-1 (pubk c)) (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-1 (pubk c))))
    ((recv (enc a b d na nb-1 (pubk c)))
      (send (enc a b c na nb-1 nc-1 (pubk d)))))
  (label 5)
  (parent 3)
  (unrealized (0 1) (2 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nc-0 nb-0 nd-0 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp3 2 (na na) (nb nb-0) (nc nc-0) (nd nd-0) (a a) (b b)
    (c c) (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (0 1)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp3 2) na (0 1)
    (enc a b c na nb-0 nc-0 (pubk d)) (enc a b d na nb-0 (pubk c))
    (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b c na nb-0 nc-0 (pubk d)))
      (send (enc b c d na nb-0 nc-0 nd-0 (pubk a)))))
  (label 6)
  (parent 4)
  (unrealized (0 1) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nb-0 nc-0 nb-1 nc-1 nb-2 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-1) (nc nc-1) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-2) (a a) (b b) (c c) (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp1 2) na (4 0)
    (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-1 (pubk c))))
    ((recv (enc a b d na nb-1 (pubk c)))
      (send (enc a b c na nb-1 nc-1 (pubk d))))
    ((recv (enc a c d na (pubk b)))
      (send (enc a b d na nb-2 (pubk c)))))
  (label 7)
  (parent 5)
  (unrealized (0 1) (2 0) (4 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nc-0 nb-0 nd-0 nb-1 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp3 2 (na na) (nb nb-0) (nc nc-0) (nd nd-0) (a a) (b b)
    (c c) (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (0 1)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp1 2) na (4 0)
    (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b c na nb-0 nc-0 (pubk d)))
      (send (enc b c d na nb-0 nc-0 nd-0 (pubk a))))
    ((recv (enc a c d na (pubk b)))
      (send (enc a b d na nb-1 (pubk c)))))
  (label 8)
  (parent 6)
  (unrealized (0 1) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nb-0 nc-0 nc-1 nb-1 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-1) (nc nc-1) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (contracted (nb-2 nb-1)) na (4 0)
    (enc a b d na nb-1 (pubk c)) (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-1 (pubk c))))
    ((recv (enc a b d na nb-1 (pubk c)))
      (send (enc a b c na nb-1 nc-1 (pubk d))))
    ((recv (enc a c d na (pubk b)))
      (send (enc a b d na nb-1 (pubk c)))))
  (label 9)
  (parent 7)
  (unrealized (0 1) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nb-0 nc-0 nb-1 nc-1 nb-2 nc-2 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-1) (nc nc-1) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-2) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-2) (nc nc-2) (a a) (b b) (c c)
    (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (6 0))
    ((1 1) (0 1)) ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0))
    ((5 1) (4 0)) ((6 1) (4 0)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp2 2) na (4 0)
    (enc a b d na nb-2 (pubk c)) (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-1 (pubk c))))
    ((recv (enc a b d na nb-1 (pubk c)))
      (send (enc a b c na nb-1 nc-1 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-2 (pubk c))))
    ((recv (enc a b d na nb-2 (pubk c)))
      (send (enc a b c na nb-2 nc-2 (pubk d)))))
  (label 10)
  (parent 7)
  (unrealized (0 1) (2 0) (4 0) (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nc-0 nb-0 nd-0 nb-1 nc-1 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp3 2 (na na) (nb nb-0) (nc nc-0) (nd nd-0) (a a) (b b)
    (c c) (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-1) (nc nc-1) (a a) (b b) (c c)
    (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (6 0))
    ((1 1) (0 1)) ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (0 1))
    ((5 1) (4 0)) ((6 1) (4 0)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp2 2) na (4 0)
    (enc a b d na nb-1 (pubk c)) (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b c na nb-0 nc-0 (pubk d)))
      (send (enc b c d na nb-0 nc-0 nd-0 (pubk a))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-1 (pubk c))))
    ((recv (enc a b d na nb-1 (pubk c)))
      (send (enc a b c na nb-1 nc-1 (pubk d)))))
  (label 11)
  (parent 8)
  (unrealized (0 1) (4 0) (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nc-0 nc-1 nb-0 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-1) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0)) ((5 1) (4 0)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (contracted (nb-1 nb-0)) na (2 0)
    (enc a b c na nb-0 nc-1 (pubk d)) (enc a b d na nb-0 (pubk c))
    (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-1 (pubk d))))
    ((recv (enc a c d na (pubk b)))
      (send (enc a b d na nb-0 (pubk c)))))
  (label 12)
  (parent 9)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton nsl4cm
  (vars (na nb nc nd nb-0 nc-0 nc-1 nb-1 nd-0 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-1) (nc nc-1) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (defstrand resp3 2 (na na) (nb nb-1) (nc nc-1) (nd nd-0) (a a) (b b)
    (c c) (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (6 0))
    ((1 1) (0 1)) ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0))
    ((5 1) (4 0)) ((6 1) (2 0)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp3 2) na (2 0)
    (enc a b c na nb-1 nc-1 (pubk d)) (enc a b d na nb-1 (pubk c))
    (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-1 (pubk c))))
    ((recv (enc a b d na nb-1 (pubk c)))
      (send (enc a b c na nb-1 nc-1 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-1 (pubk c))))
    ((recv (enc a b c na nb-1 nc-1 (pubk d)))
      (send (enc b c d na nb-1 nc-1 nd-0 (pubk a)))))
  (label 13)
  (parent 9)
  (unrealized (0 1) (2 0) (6 0))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton nsl4cm
  (vars (na nb nc nd nb-0 nc-0 nb-1 nc-1 nb-2 nc-2 nb-3 text)
    (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-1) (nc nc-1) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-2) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-2) (nc nc-2) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-3) (a a) (b b) (c c) (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (7 0))
    ((1 1) (0 1)) ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0))
    ((5 1) (4 0)) ((6 1) (4 0)) ((7 1) (6 0)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp1 2) na (6 0)
    (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-1 (pubk c))))
    ((recv (enc a b d na nb-1 (pubk c)))
      (send (enc a b c na nb-1 nc-1 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-2 (pubk c))))
    ((recv (enc a b d na nb-2 (pubk c)))
      (send (enc a b c na nb-2 nc-2 (pubk d))))
    ((recv (enc a c d na (pubk b)))
      (send (enc a b d na nb-3 (pubk c)))))
  (label 14)
  (parent 10)
  (unrealized (0 1) (2 0) (4 0) (6 0))
  (comment "aborted"))

(defskeleton nsl4cm
  (vars (na nb nc nd nc-0 nb-0 nd-0 nb-1 nc-1 nb-2 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp3 2 (na na) (nb nb-0) (nc nc-0) (nd nd-0) (a a) (b b)
    (c c) (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-1) (nc nc-1) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-2) (a a) (b b) (c c) (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (7 0))
    ((1 1) (0 1)) ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (0 1))
    ((5 1) (4 0)) ((6 1) (4 0)) ((7 1) (6 0)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp1 2) na (6 0)
    (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b c na nb-0 nc-0 (pubk d)))
      (send (enc b c d na nb-0 nc-0 nd-0 (pubk a))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-1 (pubk c))))
    ((recv (enc a b d na nb-1 (pubk c)))
      (send (enc a b c na nb-1 nc-1 (pubk d))))
    ((recv (enc a c d na (pubk b)))
      (send (enc a b d na nb-2 (pubk c)))))
  (label 15)
  (parent 11)
  (unrealized (0 1) (4 0) (6 0))
  (comment "aborted"))

(defskeleton nsl4cm
  (vars (na nb nc nd nc-0 nc-1 nb-0 nd-0 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-1) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp3 2 (na na) (nb nb-0) (nc nc-0) (nd nd-0) (a a) (b b)
    (c c) (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (6 0))
    ((1 1) (0 1)) ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0))
    ((5 1) (4 0)) ((6 1) (0 1)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp3 2) na (0 1)
    (enc a b c na nb-0 nc-0 (pubk d)) (enc a b c na nb-0 nc-1 (pubk d))
    (enc a b d na nb-0 (pubk c)) (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-1 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b c na nb-0 nc-0 (pubk d)))
      (send (enc b c d na nb-0 nc-0 nd-0 (pubk a)))))
  (label 16)
  (parent 12)
  (unrealized (0 1) (6 0))
  (comment "aborted"))

(defskeleton nsl4cm
  (vars (na nb nc nd nc-0 nc-1 nb-0 nd-0 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-1) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp3 2 (na na) (nb nb-0) (nc nc-1) (nd nd-0) (a a) (b b)
    (c c) (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (6 0))
    ((1 1) (0 1)) ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0))
    ((5 1) (4 0)) ((6 1) (0 1)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp3 2) na (0 1)
    (enc a b c na nb-0 nc-0 (pubk d)) (enc a b c na nb-0 nc-1 (pubk d))
    (enc a b d na nb-0 (pubk c)) (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-1 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b c na nb-0 nc-1 (pubk d)))
      (send (enc b c d na nb-0 nc-1 nd-0 (pubk a)))))
  (label 17)
  (parent 12)
  (unrealized (0 1) (6 0))
  (comment "aborted"))

(defskeleton nsl4cm
  (vars (na nb nc nd nb-0 nc-0 nc-1 nb-1 nd-0 nb-2 text) (a b c d name))
  (defstrand init 3 (na na) (nb nb) (nc nc) (nd nd) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-0) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-0) (nc nc-0) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (defstrand resp2 2 (na na) (nb nb-1) (nc nc-1) (a a) (b b) (c c)
    (d d))
  (defstrand resp1 2 (na na) (nb nb-1) (a a) (b b) (c c) (d d))
  (defstrand resp3 2 (na na) (nb nb-1) (nc nc-1) (nd nd-0) (a a) (b b)
    (c c) (d d))
  (defstrand resp1 2 (na na) (nb nb-2) (a a) (b b) (c c) (d d))
  (precedes ((0 0) (1 0)) ((0 0) (3 0)) ((0 0) (5 0)) ((0 0) (7 0))
    ((1 1) (0 1)) ((2 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0))
    ((5 1) (4 0)) ((6 1) (2 0)) ((7 1) (6 0)))
  (non-orig (privk a) (privk b) (privk c) (privk d))
  (uniq-orig na)
  (operation nonce-test (added-strand resp1 2) na (6 0)
    (enc a c d na (pubk b)))
  (traces
    ((send (enc a c d na (pubk b)))
      (recv (enc b c d na nb nc nd (pubk a)))
      (send (enc nb nc nd (pubk b))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-0 (pubk c))))
    ((recv (enc a b d na nb-0 (pubk c)))
      (send (enc a b c na nb-0 nc-0 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-1 (pubk c))))
    ((recv (enc a b d na nb-1 (pubk c)))
      (send (enc a b c na nb-1 nc-1 (pubk d))))
    ((recv (enc a c d na (pubk b))) (send (enc a b d na nb-1 (pubk c))))
    ((recv (enc a b c na nb-1 nc-1 (pubk d)))
      (send (enc b c d na nb-1 nc-1 nd-0 (pubk a))))
    ((recv (enc a c d na (pubk b)))
      (send (enc a b d na nb-2 (pubk c)))))
  (label 18)
  (parent 13)
  (unrealized (0 1) (2 0) (6 0))
  (comment "aborted"))