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

(defprotocol neuman-stubblebine basic
  (defrole init
    (vars (a b ks name) (ra rb text) (k skey) (tb text))
    (trace (send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
  (defrole resp
    (vars (a b ks name) (ra rb text) (k skey) (tb text))
    (trace (recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k)))))
  (defrole init-reauth
    (vars (a b ks name) (ra-prime rb-prime text) (k skey) (tb text))
    (trace (recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime))
      (recv (cat rb-prime (enc ra-prime k))) (send (enc rb-prime k))))
  (defrole resp-reauth
    (vars (a b ks name) (ra-prime rb-prime text) (k skey) (tb text))
    (trace (recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k))))
  (defrole keyserver
    (vars (a b ks name) (ra rb text) (k skey) (tb text))
    (trace (recv (cat b rb (enc a ra tb (ltk b ks))))
      (send
        (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
    (uniq-orig k)))

(defskeleton neuman-stubblebine
  (vars (ra tb rb ra-prime rb-prime tb-0 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k))))
  (label 0)
  (unrealized (0 2) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 text) (a b ks name)
    (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (precedes ((2 1) (0 2)) ((2 1) (1 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand keyserver 2)
    (enc a k tb-0 (ltk b ks)) (1 0))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0))))
  (label 1)
  (parent 0)
  (unrealized (0 2) (1 2) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (precedes ((2 1) (0 2)) ((2 1) (1 0)) ((3 1) (2 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand resp 2)
    (enc a ra-0 tb-0 (ltk b ks)) (2 0))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks))))))
  (label 2)
  (parent 1)
  (unrealized (0 2) (1 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-1 tb-1 text)
    (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-1) (rb rb-prime) (tb tb-1) (a a-0) (b b-0)
    (ks ks-0) (k k))
  (precedes ((1 1) (4 1)) ((2 1) (0 2)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 2) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init 3) (enc rb-prime k)
    (1 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((send (cat a-0 ra-1))
      (recv
        (cat (enc b-0 ra-1 k tb-1 (ltk a-0 ks-0))
          (enc a-0 k tb-1 (ltk b-0 ks-0)) rb-prime))
      (send (cat (enc a-0 k tb-1 (ltk b-0 ks-0)) (enc rb-prime k)))))
  (label 3)
  (parent 2)
  (unrealized (0 2) (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0 tb-1
      text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-1) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((3 1) (2 0)) ((4 3) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init-reauth 4)
    (enc rb-prime k) (1 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a-0 k tb-1 (ltk b-0 ks-0)))
      (send (cat (enc a-0 k tb-1 (ltk b-0 ks-0)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k))))
  (label 4)
  (parent 2)
  (unrealized (0 2) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 rb-prime-0 tb-1
      text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb-1) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((1 1) (4 0)) ((2 1) (0 2)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand resp-reauth 2)
    (enc rb-prime k) (1 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (cat (enc a-0 k tb-1 (ltk b-0 ks-0)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k)))))
  (label 5)
  (parent 2)
  (unrealized (0 2) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (deflistener k)
  (precedes ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0)) ((3 1) (2 0))
    ((4 1) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-listener k) (enc rb-prime k) (1 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv k) (send k)))
  (label 6)
  (parent 2)
  (unrealized (0 2) (4 0))
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-1 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-1) (rb rb-prime) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (precedes ((1 1) (4 1)) ((2 1) (0 2)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 2) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-1 tb-0)) k (4 1)
    (enc a k tb-0 (ltk b ks)) (enc b ra-0 k tb-0 (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((send (cat a ra-1))
      (recv
        (cat (enc b ra-1 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb-0 (ltk b ks)) (enc rb-prime k)))))
  (label 7)
  (parent 3)
  (unrealized (0 2) (4 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((3 1) (2 0)) ((4 3) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-1 tb-0)) k (4 0)
    (enc a k tb-0 (ltk b ks)) (enc b ra-0 k tb-0 (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k))))
  (label 8)
  (parent 4)
  (unrealized (0 2) (4 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 rb-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (precedes ((1 1) (4 0)) ((2 1) (0 2)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-1 tb-0)) k (4 0)
    (enc a k tb-0 (ltk b ks)) (enc b ra-0 k tb-0 (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k)))))
  (label 9)
  (parent 5)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (precedes ((1 1) (4 1)) ((2 1) (0 2)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 2) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand keyserver 2)
    (enc b ra-0 k tb-0 (ltk a ks)) (4 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb-0 (ltk b ks)) (enc rb-prime k)))))
  (label 10)
  (parent 7)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0 ra-1 tb-1
      text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb ra-prime-0) (tb tb-1) (a a-0) (b b-0)
    (ks ks-0) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 1)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 2) (4 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init 3) (enc ra-prime-0 k)
    (4 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((send (cat a-0 ra-1))
      (recv
        (cat (enc b-0 ra-1 k tb-1 (ltk a-0 ks-0))
          (enc a-0 k tb-1 (ltk b-0 ks-0)) ra-prime-0))
      (send (cat (enc a-0 k tb-1 (ltk b-0 ks-0)) (enc ra-prime-0 k)))))
  (label 11)
  (parent 8)
  (unrealized (0 2) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 tb-1 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-1) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 3) (4 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init-reauth 4)
    (enc ra-prime-0 k) (4 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a-0 k tb-1 (ltk b-0 ks-0)))
      (send (cat (enc a-0 k tb-1 (ltk b-0 ks-0)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k))))
  (label 12)
  (parent 8)
  (unrealized (0 2) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      rb-prime-0 tb-1 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-0)
    (tb tb-1) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 1) (4 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand resp-reauth 2)
    (enc ra-prime-0 k) (4 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc a-0 k tb-1 (ltk b-0 ks-0)) ra-prime-0))
      (send (cat rb-prime-0 (enc ra-prime-0 k)))))
  (label 13)
  (parent 8)
  (unrealized (0 2) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (deflistener k)
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 1) (4 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-listener k) (enc ra-prime-0 k)
    (4 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv k) (send k)))
  (label 14)
  (parent 8)
  (unrealized (0 2) (5 0))
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((1 1) (4 0)) ((2 1) (0 2)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 1) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand keyserver 2)
    (enc a k tb (ltk b ks)) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k)))))
  (label 15)
  (parent 9)
  (unrealized (0 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 text) (a b ks name)
    (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (precedes ((1 1) (4 1)) ((2 1) (0 2)) ((2 1) (1 0)) ((3 1) (2 0))
    ((4 2) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand keyserver 2)
    (enc a k tb (ltk b ks)) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k)))))
  (label 16)
  (parent 10)
  (unrealized (0 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0 ra-1
      text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb ra-prime-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 1)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 2) (4 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-1 tb-0)) k (5 1)
    (enc a k tb-0 (ltk b ks)) (enc b ra-0 k tb-0 (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((send (cat a ra-1))
      (recv
        (cat (enc b ra-1 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          ra-prime-0))
      (send (cat (enc a k tb-0 (ltk b ks)) (enc ra-prime-0 k)))))
  (label 17)
  (parent 11)
  (unrealized (0 2) (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 3) (4 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-1 tb-0)) k (5 0)
    (enc a k tb-0 (ltk b ks)) (enc b ra-0 k tb-0 (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k))))
  (label 18)
  (parent 12)
  (unrealized (0 2) (5 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      rb-prime-0 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 1) (4 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-1 tb-0)) k (5 0)
    (enc a k tb-0 (ltk b ks)) (enc b ra-0 k tb-0 (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc ra-prime-0 k)))))
  (label 19)
  (parent 13)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-1 tb-0
      text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb rb) (tb tb-0) (a a-0) (b b-0)
    (ks ks-0) (k k))
  (precedes ((0 1) (5 1)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 1))
    ((3 1) (2 0)) ((4 1) (1 2)) ((5 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init 3) (enc rb k) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((send (cat a-0 ra-1))
      (recv
        (cat (enc b-0 ra-1 k tb-0 (ltk a-0 ks-0))
          (enc a-0 k tb-0 (ltk b-0 ks-0)) rb))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) (enc rb k)))))
  (label 20)
  (parent 15)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-prime-0
      tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb-0)
    (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
    ((3 1) (2 0)) ((4 1) (1 2)) ((5 3) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init-reauth 4) (enc rb k)
    (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((recv (enc a-0 k tb-0 (ltk b-0 ks-0)))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
  (label 21)
  (parent 15)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 rb-prime-1
      tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime rb) (rb-prime rb-prime-1) (tb tb-0)
    (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (5 0)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
    ((3 1) (2 0)) ((4 1) (1 2)) ((5 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand resp-reauth 2) (enc rb k)
    (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((recv (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) rb))
      (send (cat rb-prime-1 (enc rb k)))))
  (label 22)
  (parent 15)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (deflistener k)
  (precedes ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0)) ((3 1) (2 0))
    ((4 1) (1 2)) ((5 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-listener k) (enc rb k) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k)))) ((recv k) (send k)))
  (label 23)
  (parent 15)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-1 tb-0 text)
    (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init 3 (ra ra-1) (rb rb) (tb tb-0) (a a-0) (b b-0)
    (ks ks-0) (k k))
  (precedes ((0 1) (5 1)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 1))
    ((3 1) (2 0)) ((4 2) (1 2)) ((5 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init 3) (enc rb k) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((send (cat a-0 ra-1))
      (recv
        (cat (enc b-0 ra-1 k tb-0 (ltk a-0 ks-0))
          (enc a-0 k tb-0 (ltk b-0 ks-0)) rb))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) (enc rb k)))))
  (label 24)
  (parent 16)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 tb-0 text)
    (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb-0)
    (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
    ((3 1) (2 0)) ((4 2) (1 2)) ((5 3) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init-reauth 4) (enc rb k)
    (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv (enc a-0 k tb-0 (ltk b-0 ks-0)))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
  (label 25)
  (parent 16)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 tb-0 text)
    (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp-reauth 2 (ra-prime rb) (rb-prime rb-prime-0) (tb tb-0)
    (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (5 0)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
    ((3 1) (2 0)) ((4 2) (1 2)) ((5 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand resp-reauth 2) (enc rb k)
    (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) rb))
      (send (cat rb-prime-0 (enc rb k)))))
  (label 26)
  (parent 16)
  (unrealized (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 text) (a b ks name)
    (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (deflistener k)
  (precedes ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0)) ((3 1) (2 0))
    ((4 2) (1 2)) ((5 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-listener k) (enc rb k) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv k) (send k)))
  (label 27)
  (parent 16)
  (unrealized (5 0))
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-0) (rb ra-prime-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 1)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 2) (4 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand keyserver 2)
    (enc b ra-0 k tb-0 (ltk a ks)) (5 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          ra-prime-0))
      (send (cat (enc a k tb-0 (ltk b ks)) (enc ra-prime-0 k)))))
  (label 28)
  (parent 17)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 ra-1 tb-1 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb ra-prime-1) (tb tb-1) (a a-0) (b b-0)
    (ks ks-0) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 1)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 3) (4 2)) ((6 2) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init 3) (enc ra-prime-1 k)
    (5 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((send (cat a-0 ra-1))
      (recv
        (cat (enc b-0 ra-1 k tb-1 (ltk a-0 ks-0))
          (enc a-0 k tb-1 (ltk b-0 ks-0)) ra-prime-1))
      (send (cat (enc a-0 k tb-1 (ltk b-0 ks-0)) (enc ra-prime-1 k)))))
  (label 29)
  (parent 18)
  (unrealized (0 2) (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 ra-prime-2 tb-1 text) (a b ks a-0 b-0 ks-0 name)
    (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-2) (rb-prime ra-prime-1)
    (tb tb-1) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 3) (4 2)) ((6 3) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init-reauth 4)
    (enc ra-prime-1 k) (5 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (enc a-0 k tb-1 (ltk b-0 ks-0)))
      (send (cat (enc a-0 k tb-1 (ltk b-0 ks-0)) ra-prime-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k))))
  (label 30)
  (parent 18)
  (unrealized (0 2) (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 rb-prime-0 tb-1 text) (a b ks a-0 b-0 ks-0 name)
    (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-1) (rb-prime rb-prime-0)
    (tb tb-1) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 3) (4 2)) ((6 1) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand resp-reauth 2)
    (enc ra-prime-1 k) (5 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (cat (enc a-0 k tb-1 (ltk b-0 ks-0)) ra-prime-1))
      (send (cat rb-prime-0 (enc ra-prime-1 k)))))
  (label 31)
  (parent 18)
  (unrealized (0 2) (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (deflistener k)
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 3) (4 2)) ((6 1) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-listener k) (enc ra-prime-1 k)
    (5 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k))) ((recv k) (send k)))
  (label 32)
  (parent 18)
  (unrealized (0 2) (6 0))
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 1) (4 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand keyserver 2)
    (enc a k tb (ltk b ks)) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc ra-prime-0 k)))))
  (label 33)
  (parent 19)
  (unrealized (0 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-1 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 1)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 1))
    ((3 1) (2 0)) ((4 1) (1 2)) ((5 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (5 1) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((send (cat a ra-1))
      (recv
        (cat (enc b ra-1 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
  (label 34)
  (parent 20)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-prime-0
      text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
    ((3 1) (2 0)) ((4 1) (1 2)) ((5 3) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (5 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
  (label 35)
  (parent 21)
  (unrealized (5 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 rb-prime-1
      text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime rb) (rb-prime rb-prime-1) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 0)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
    ((3 1) (2 0)) ((4 1) (1 2)) ((5 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (5 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((recv (cat (enc a k tb (ltk b ks)) rb))
      (send (cat rb-prime-1 (enc rb k)))))
  (label 36)
  (parent 22)
  (unrealized)
  (shape)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-1 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init 3 (ra ra-1) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 1)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 1))
    ((3 1) (2 0)) ((4 2) (1 2)) ((5 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (5 1) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((send (cat a ra-1))
      (recv
        (cat (enc b ra-1 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
  (label 37)
  (parent 24)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
    ((3 1) (2 0)) ((4 2) (1 2)) ((5 3) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (5 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
  (label 38)
  (parent 25)
  (unrealized (5 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp-reauth 2 (ra-prime rb) (rb-prime rb-prime-0) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 0)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
    ((3 1) (2 0)) ((4 2) (1 2)) ((5 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (5 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv (cat (enc a k tb (ltk b ks)) rb))
      (send (cat rb-prime-0 (enc rb k)))))
  (label 39)
  (parent 26)
  (unrealized)
  (shape)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 1)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 2) (4 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand keyserver 2)
    (enc a k tb (ltk b ks)) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          ra-prime-0))
      (send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k)))))
  (label 40)
  (parent 28)
  (unrealized (0 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 ra-1 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb ra-prime-1) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 1)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 3) (4 2)) ((6 2) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-1 tb-0)) k (6 1)
    (enc a k tb-0 (ltk b ks)) (enc b ra-0 k tb-0 (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((send (cat a ra-1))
      (recv
        (cat (enc b ra-1 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          ra-prime-1))
      (send (cat (enc a k tb-0 (ltk b ks)) (enc ra-prime-1 k)))))
  (label 41)
  (parent 29)
  (unrealized (0 2) (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 ra-prime-2 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-2) (rb-prime ra-prime-1)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 3) (4 2)) ((6 3) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-1 tb-0)) k (6 0)
    (enc a k tb-0 (ltk b ks)) (enc b ra-0 k tb-0 (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k))))
  (label 42)
  (parent 30)
  (unrealized (0 2) (6 2))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 rb-prime-0 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-1) (rb-prime rb-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 3) (4 2)) ((6 1) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-1 tb-0)) k (6 0)
    (enc a k tb-0 (ltk b ks)) (enc b ra-0 k tb-0 (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (send (cat rb-prime-0 (enc ra-prime-1 k)))))
  (label 43)
  (parent 31)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      ra-1 tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb rb) (tb tb-0) (a a-0) (b b-0)
    (ks ks-0) (k k))
  (precedes ((0 1) (6 1)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 1)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 1) (4 2)) ((6 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init 3) (enc rb k) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc ra-prime-0 k))))
    ((send (cat a-0 ra-1))
      (recv
        (cat (enc b-0 ra-1 k tb-0 (ltk a-0 ks-0))
          (enc a-0 k tb-0 (ltk b-0 ks-0)) rb))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) (enc rb k)))))
  (label 44)
  (parent 33)
  (unrealized (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      ra-prime-1 tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime rb) (tb tb-0)
    (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (6 2)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 1) (4 2)) ((6 3) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init-reauth 4) (enc rb k)
    (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc ra-prime-0 k))))
    ((recv (enc a-0 k tb-0 (ltk b-0 ks-0)))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-1))
      (recv (cat rb (enc ra-prime-1 k))) (send (enc rb k))))
  (label 45)
  (parent 33)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      rb-prime-1 tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime rb) (rb-prime rb-prime-1) (tb tb-0)
    (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (6 0)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 1) (4 2)) ((6 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand resp-reauth 2) (enc rb k)
    (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc ra-prime-0 k))))
    ((recv (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) rb))
      (send (cat rb-prime-1 (enc rb k)))))
  (label 46)
  (parent 33)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (deflistener k)
  (precedes ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0)) ((2 1) (5 0))
    ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 1) (4 2))
    ((6 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-listener k) (enc rb k) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc ra-prime-0 k)))) ((recv k) (send k)))
  (label 47)
  (parent 33)
  (unrealized (6 0))
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 1)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 1))
    ((3 1) (2 0)) ((4 1) (1 2)) ((5 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand keyserver 2)
    (enc b ra-0 k tb (ltk a ks)) (5 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
  (label 48)
  (parent 34)
  (unrealized)
  (shape)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-prime-0
      ra-1 tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb ra-prime-0) (tb tb-0) (a a-0) (b b-0)
    (ks ks-0) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 1)) ((3 1) (2 0)) ((4 1) (1 2)) ((5 3) (0 2))
    ((6 2) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init 3) (enc ra-prime-0 k)
    (5 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((send (cat a-0 ra-1))
      (recv
        (cat (enc b-0 ra-1 k tb-0 (ltk a-0 ks-0))
          (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-0))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) (enc ra-prime-0 k)))))
  (label 49)
  (parent 35)
  (unrealized (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-prime-0
      ra-prime-1 tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 0)) ((3 1) (2 0)) ((4 1) (1 2)) ((5 3) (0 2))
    ((6 3) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init-reauth 4)
    (enc ra-prime-0 k) (5 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((recv (enc a-0 k tb-0 (ltk b-0 ks-0)))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k))))
  (label 50)
  (parent 35)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-prime-0
      rb-prime-1 tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-1)
    (tb tb-0) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 0)) ((3 1) (2 0)) ((4 1) (1 2)) ((5 3) (0 2))
    ((6 1) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand resp-reauth 2)
    (enc ra-prime-0 k) (5 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((recv (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-0))
      (send (cat rb-prime-1 (enc ra-prime-0 k)))))
  (label 51)
  (parent 35)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-prime-0
      text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (deflistener k)
  (precedes ((0 1) (5 2)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 0)) ((3 1) (2 0)) ((4 1) (1 2)) ((5 3) (0 2))
    ((6 1) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-listener k) (enc ra-prime-0 k)
    (5 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((recv k) (send k)))
  (label 52)
  (parent 35)
  (unrealized (6 0))
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb rb-0 rb-prime-0 rb-prime-1 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime rb) (rb-prime rb-prime-1) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (2 0)) ((1 1) (3 0)) ((2 1) (1 0)) ((2 1) (4 0))
    ((3 1) (1 2)) ((4 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation collapsed 3 0)
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
      (send
        (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((recv (cat (enc a k tb (ltk b ks)) rb))
      (send (cat rb-prime-1 (enc rb k)))))
  (label 53)
  (parent 36)
  (unrealized)
  (shape)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra ra-prime rb-prime tb ra-0 rb rb-0 rb-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb ra-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (4 0)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 1) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra ra-prime rb-prime k)
  (operation collapsed 5 1)
  (traces
    ((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
    ((recv (cat a ra-0)) (send (cat b rb-0 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k)))))
  (label 54)
  (parent 36)
  (seen 79)
  (unrealized)
  (shape)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 text) (a b ks name)
    (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init 3 (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 1)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 1))
    ((3 1) (2 0)) ((4 2) (1 2)) ((5 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand keyserver 2)
    (enc b ra-0 k tb (ltk a ks)) (5 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
  (label 55)
  (parent 37)
  (unrealized)
  (shape))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 ra-1 tb-0
      text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb ra-prime-0) (tb tb-0) (a a-0) (b b-0)
    (ks ks-0) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 1)) ((3 1) (2 0)) ((4 2) (1 2)) ((5 3) (0 2))
    ((6 2) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init 3) (enc ra-prime-0 k)
    (5 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((send (cat a-0 ra-1))
      (recv
        (cat (enc b-0 ra-1 k tb-0 (ltk a-0 ks-0))
          (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-0))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) (enc ra-prime-0 k)))))
  (label 56)
  (parent 38)
  (unrealized (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 ra-prime-1
      tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 0)) ((3 1) (2 0)) ((4 2) (1 2)) ((5 3) (0 2))
    ((6 3) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init-reauth 4)
    (enc ra-prime-0 k) (5 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((recv (enc a-0 k tb-0 (ltk b-0 ks-0)))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k))))
  (label 57)
  (parent 38)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-0)
    (tb tb-0) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 0)) ((3 1) (2 0)) ((4 2) (1 2)) ((5 3) (0 2))
    ((6 1) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand resp-reauth 2)
    (enc ra-prime-0 k) (5 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((recv (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-0))
      (send (cat rb-prime-0 (enc ra-prime-0 k)))))
  (label 58)
  (parent 38)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (deflistener k)
  (precedes ((0 1) (5 2)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 0)) ((3 1) (2 0)) ((4 2) (1 2)) ((5 3) (0 2))
    ((6 1) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-listener k) (enc ra-prime-0 k)
    (5 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((recv k) (send k)))
  (label 59)
  (parent 38)
  (unrealized (6 0))
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb rb-0 rb-prime-0 text) (a b ks name)
    (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init 3 (ra ra) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp-reauth 2 (ra-prime rb) (rb-prime rb-prime-0) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (2 0)) ((1 1) (3 1)) ((2 1) (1 0)) ((2 1) (4 0))
    ((3 0) (0 0)) ((3 2) (1 2)) ((4 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation collapsed 3 0)
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
      (send
        (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
    ((send (cat a ra))
      (recv
        (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv (cat (enc a k tb (ltk b ks)) rb))
      (send (cat rb-prime-0 (enc rb k)))))
  (label 60)
  (parent 39)
  (unrealized)
  (shape)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra ra-prime rb-prime tb ra-0 rb rb-0 text) (a b ks name)
    (k skey))
  (defstrand resp 3 (ra ra) (rb ra-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (4 1)) ((2 1) (1 0))
    ((3 1) (2 0)) ((4 2) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra ra-prime rb-prime k)
  (operation collapsed 5 1)
  (traces
    ((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
    ((recv (cat a ra-0)) (send (cat b rb-0 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k)))))
  (label 61)
  (parent 39)
  (seen 83)
  (unrealized)
  (shape)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 ra-1 tb-0
      text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb rb) (tb tb-0) (a a-0) (b b-0)
    (ks ks-0) (k k))
  (precedes ((0 1) (6 1)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 1)) ((2 1) (6 1)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 2) (4 2)) ((6 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init 3) (enc rb k) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          ra-prime-0))
      (send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
    ((send (cat a-0 ra-1))
      (recv
        (cat (enc b-0 ra-1 k tb-0 (ltk a-0 ks-0))
          (enc a-0 k tb-0 (ltk b-0 ks-0)) rb))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) (enc rb k)))))
  (label 62)
  (parent 40)
  (unrealized (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 ra-prime-1
      tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime rb) (tb tb-0)
    (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (6 2)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 1)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 2) (4 2)) ((6 3) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init-reauth 4) (enc rb k)
    (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          ra-prime-0))
      (send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
    ((recv (enc a-0 k tb-0 (ltk b-0 ks-0)))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-1))
      (recv (cat rb (enc ra-prime-1 k))) (send (enc rb k))))
  (label 63)
  (parent 40)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime rb) (rb-prime rb-prime-0) (tb tb-0)
    (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (6 0)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 1)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 2) (4 2)) ((6 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand resp-reauth 2) (enc rb k)
    (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          ra-prime-0))
      (send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
    ((recv (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) rb))
      (send (cat rb-prime-0 (enc rb k)))))
  (label 64)
  (parent 40)
  (unrealized (6 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (deflistener k)
  (precedes ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0)) ((2 1) (5 1))
    ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 2) (4 2))
    ((6 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-listener k) (enc rb k) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          ra-prime-0))
      (send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
    ((recv k) (send k)))
  (label 65)
  (parent 40)
  (unrealized (6 0))
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-0) (rb ra-prime-1) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 1)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 3) (4 2)) ((6 2) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand keyserver 2)
    (enc b ra-0 k tb-0 (ltk a ks)) (6 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          ra-prime-1))
      (send (cat (enc a k tb-0 (ltk b ks)) (enc ra-prime-1 k)))))
  (label 66)
  (parent 41)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 ra-prime-2 ra-1 tb-1 text) (a b ks a-0 b-0 ks-0 name)
    (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-2) (rb-prime ra-prime-1)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb ra-prime-2) (tb tb-1) (a a-0) (b b-0)
    (ks ks-0) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((2 1) (7 1)) ((3 1) (2 0))
    ((4 3) (1 2)) ((5 3) (4 2)) ((6 3) (5 2)) ((7 2) (6 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init 3) (enc ra-prime-2 k)
    (6 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k)))
    ((send (cat a-0 ra-1))
      (recv
        (cat (enc b-0 ra-1 k tb-1 (ltk a-0 ks-0))
          (enc a-0 k tb-1 (ltk b-0 ks-0)) ra-prime-2))
      (send (cat (enc a-0 k tb-1 (ltk b-0 ks-0)) (enc ra-prime-2 k)))))
  (label 67)
  (parent 42)
  (unrealized (0 2) (7 1))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 ra-prime-2 ra-prime-3 tb-1 text)
    (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-2) (rb-prime ra-prime-1)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-3) (rb-prime ra-prime-2)
    (tb tb-1) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((2 1) (7 0)) ((3 1) (2 0))
    ((4 3) (1 2)) ((5 3) (4 2)) ((6 3) (5 2)) ((7 3) (6 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand init-reauth 4)
    (enc ra-prime-2 k) (6 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k)))
    ((recv (enc a-0 k tb-1 (ltk b-0 ks-0)))
      (send (cat (enc a-0 k tb-1 (ltk b-0 ks-0)) ra-prime-3))
      (recv (cat ra-prime-2 (enc ra-prime-3 k)))
      (send (enc ra-prime-2 k))))
  (label 68)
  (parent 42)
  (unrealized (0 2) (7 0))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 ra-prime-2 rb-prime-0 tb-1 text)
    (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-2) (rb-prime ra-prime-1)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-2) (rb-prime rb-prime-0)
    (tb tb-1) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((2 1) (7 0)) ((3 1) (2 0))
    ((4 3) (1 2)) ((5 3) (4 2)) ((6 3) (5 2)) ((7 1) (6 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand resp-reauth 2)
    (enc ra-prime-2 k) (6 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k)))
    ((recv (cat (enc a-0 k tb-1 (ltk b-0 ks-0)) ra-prime-2))
      (send (cat rb-prime-0 (enc ra-prime-2 k)))))
  (label 69)
  (parent 42)
  (unrealized (0 2) (7 0))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0
      ra-prime-1 ra-prime-2 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-2) (rb-prime ra-prime-1)
    (tb tb-0) (a a) (b b) (ks ks) (k k))
  (deflistener k)
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((2 1) (7 0)) ((3 1) (2 0))
    ((4 3) (1 2)) ((5 3) (4 2)) ((6 3) (5 2)) ((7 1) (6 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-listener k) (enc ra-prime-2 k)
    (6 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb-0 (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb-0 (ltk a ks)) (enc a k tb-0 (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0))
      (send (cat b rb-1 (enc a ra-0 tb-0 (ltk b ks)))))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (enc a k tb-0 (ltk b ks)))
      (send (cat (enc a k tb-0 (ltk b ks)) ra-prime-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k))) ((recv k) (send k)))
  (label 70)
  (parent 42)
  (unrealized (0 2) (7 0))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 ra-prime-1
      rb-prime-0 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-1) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 3) (4 2)) ((6 1) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand keyserver 2)
    (enc a k tb (ltk b ks)) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
      (send (cat rb-prime-0 (enc ra-prime-1 k)))))
  (label 71)
  (parent 43)
  (unrealized (0 2))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      ra-1 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (6 1)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 1)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 1) (4 2)) ((6 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 1) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc ra-prime-0 k))))
    ((send (cat a ra-1))
      (recv
        (cat (enc b ra-1 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
  (label 72)
  (parent 44)
  (unrealized (6 1))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      ra-prime-1 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (6 2)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 1) (4 2)) ((6 3) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc ra-prime-0 k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-1))
      (recv (cat rb (enc ra-prime-1 k))) (send (enc rb k))))
  (label 73)
  (parent 45)
  (unrealized (6 2))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      rb-prime-1 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime rb) (rb-prime rb-prime-1) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (6 0)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 1) (4 2)) ((6 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc ra-prime-0 k))))
    ((recv (cat (enc a k tb (ltk b ks)) rb))
      (send (cat rb-prime-1 (enc rb k)))))
  (label 74)
  (parent 46)
  (unrealized)
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb rb-0 rb-prime-0 text) (a b ks name)
    (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (2 0)) ((1 1) (3 0)) ((2 1) (1 0)) ((2 1) (4 1))
    ((3 1) (1 2)) ((4 0) (0 0)) ((4 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation collapsed 3 0)
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
      (send
        (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
  (label 75)
  (parent 48)
  (unrealized)
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-prime-0
      ra-1 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb ra-prime-0) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 1)) ((3 1) (2 0)) ((4 1) (1 2)) ((5 3) (0 2))
    ((6 2) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 1) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((send (cat a ra-1))
      (recv
        (cat (enc b ra-1 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          ra-prime-0))
      (send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k)))))
  (label 76)
  (parent 49)
  (unrealized (6 1))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-prime-0
      ra-prime-1 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 0)) ((3 1) (2 0)) ((4 1) (1 2)) ((5 3) (0 2))
    ((6 3) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k))))
  (label 77)
  (parent 50)
  (unrealized (6 2))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-prime-0
      rb-prime-1 text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-1)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 0)) ((3 1) (2 0)) ((4 1) (1 2)) ((5 3) (0 2))
    ((6 1) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-1 (enc ra-prime-0 k)))))
  (label 78)
  (parent 51)
  (unrealized)
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars (ra ra-prime rb-prime tb rb rb-prime-0 text) (a b ks name)
    (k skey))
  (defstrand resp 3 (ra ra) (rb ra-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp-reauth 2 (ra-prime rb-prime) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((1 1) (3 0)) ((2 1) (1 0))
    ((3 1) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra ra-prime rb-prime k)
  (operation collapsed 4 1)
  (traces
    ((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb (enc a ra tb (ltk b ks))))
      (send
        (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
    ((recv (cat (enc a k tb (ltk b ks)) rb-prime))
      (send (cat rb-prime-0 (enc rb-prime k)))))
  (label 79)
  (parent 53)
  (unrealized)
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 ra-1 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb ra-prime-0) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 1)) ((3 1) (2 0)) ((4 2) (1 2)) ((5 3) (0 2))
    ((6 2) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 1) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((send (cat a ra-1))
      (recv
        (cat (enc b ra-1 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          ra-prime-0))
      (send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k)))))
  (label 80)
  (parent 56)
  (unrealized (6 1))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 ra-prime-1
      text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 0)) ((3 1) (2 0)) ((4 2) (1 2)) ((5 3) (0 2))
    ((6 3) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k))))
  (label 81)
  (parent 57)
  (unrealized (6 2))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime ra-prime-0) (rb-prime rb-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 0)) ((3 1) (2 0)) ((4 2) (1 2)) ((5 3) (0 2))
    ((6 1) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc ra-prime-0 k)))))
  (label 82)
  (parent 58)
  (unrealized)
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars (ra ra-prime rb-prime tb rb text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb ra-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init 3 (ra ra) (rb rb-prime) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((1 1) (3 1)) ((2 1) (1 0))
    ((3 0) (0 0)) ((3 2) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra ra-prime rb-prime k)
  (operation collapsed 4 1)
  (traces
    ((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb (enc a ra tb (ltk b ks))))
      (send
        (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
    ((send (cat a ra))
      (recv
        (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-prime))
      (send (cat (enc a k tb (ltk b ks)) (enc rb-prime k)))))
  (label 83)
  (parent 60)
  (unrealized)
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 ra-1 text)
    (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (6 1)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 1)) ((2 1) (6 1)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 2) (4 2)) ((6 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 1) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          ra-prime-0))
      (send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
    ((send (cat a ra-1))
      (recv
        (cat (enc b ra-1 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
  (label 84)
  (parent 62)
  (unrealized (6 1))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 ra-prime-1
      text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (6 2)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 1)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 2) (4 2)) ((6 3) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          ra-prime-0))
      (send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-1))
      (recv (cat rb (enc ra-prime-1 k))) (send (enc rb k))))
  (label 85)
  (parent 63)
  (unrealized (6 2))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (defstrand resp-reauth 2 (ra-prime rb) (rb-prime rb-prime-0) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (6 0)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 1)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 2) (4 2)) ((6 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          ra-prime-0))
      (send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
    ((recv (cat (enc a k tb (ltk b ks)) rb))
      (send (cat rb-prime-0 (enc rb k)))))
  (label 86)
  (parent 64)
  (unrealized)
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 ra-prime-1
      text) (a b ks name) (k skey))
  (defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 3 (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (ra-prime ra-prime-0) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (ra-prime ra-prime-1) (rb-prime ra-prime-0)
    (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-0) (rb ra-prime-1) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 1)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 3) (4 2)) ((6 2) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation encryption-test (added-strand keyserver 2)
    (enc a k tb (ltk b ks)) (0 2))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          ra-prime-1))
      (send (cat (enc a k tb (ltk b ks)) (enc ra-prime-1 k)))))
  (label 87)
  (parent 66)
  (unrealized (0 2))
  (comment "aborted"))