(comment "CPSA 2.0.4")
(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 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 nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-1 ra-0) (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-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 7)
  (parent 3)
  (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 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 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 10)
  (parent 7)
  (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 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 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 16)
  (parent 10)
  (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 17)
  (parent 10)
  (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 18)
  (parent 10)
  (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 19)
  (parent 10)
  (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 nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-1 ra-0) (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-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 20)
  (parent 11)
  (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 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 21)
  (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 22)
  (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 23)
  (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 24)
  (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 25)
  (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 26)
  (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 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 nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-1 ra-0) (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-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 27)
  (parent 16)
  (unrealized)
  (shape))

(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 28)
  (parent 17)
  (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 29)
  (parent 18)
  (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 30)
  (parent 20)
  (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 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 31)
  (parent 21)
  (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 32)
  (parent 21)
  (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 33)
  (parent 21)
  (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 34)
  (parent 21)
  (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 35)
  (parent 22)
  (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 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 nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-1 ra-0) (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-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 36)
  (parent 23)
  (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
      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 37)
  (parent 24)
  (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 38)
  (parent 25)
  (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 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 39)
  (parent 28)
  (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 40)
  (parent 28)
  (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 41)
  (parent 28)
  (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 42)
  (parent 28)
  (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 43)
  (parent 29)
  (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 44)
  (parent 29)
  (seen 66)
  (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 45)
  (parent 30)
  (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 46)
  (parent 30)
  (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 47)
  (parent 30)
  (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 48)
  (parent 30)
  (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 nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-1 ra-0) (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-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 49)
  (parent 31)
  (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-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 50)
  (parent 32)
  (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 51)
  (parent 33)
  (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 52)
  (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 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 53)
  (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 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 54)
  (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 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 55)
  (parent 35)
  (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 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 56)
  (parent 36)
  (unrealized)
  (shape))

(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 57)
  (parent 37)
  (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 58)
  (parent 37)
  (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 59)
  (parent 37)
  (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 60)
  (parent 37)
  (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 61)
  (parent 38)
  (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 62)
  (parent 38)
  (seen 82)
  (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 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-0) (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) (ra-1 ra-0) (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-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 63)
  (parent 39)
  (unrealized)
  (shape))

(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 64)
  (parent 40)
  (unrealized (6 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 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 65)
  (parent 41)
  (unrealized)
  (shape)
  (comment "2 in cohort - 2 not yet seen"))

(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 66)
  (parent 43)
  (unrealized)
  (shape))

(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))
  (defstrand init 3 (ra ra-0) (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) (ra-1 ra-0) (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-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 67)
  (parent 45)
  (unrealized)
  (shape))

(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 68)
  (parent 46)
  (unrealized (6 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 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 69)
  (parent 47)
  (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 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 70)
  (parent 49)
  (unrealized (0 2))
  (comment "4 in cohort - 4 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 71)
  (parent 50)
  (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 72)
  (parent 50)
  (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 73)
  (parent 50)
  (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 74)
  (parent 50)
  (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 75)
  (parent 51)
  (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
      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-0) (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) (ra-1 ra-0) (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-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 76)
  (parent 52)
  (unrealized)
  (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 77)
  (parent 53)
  (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 78)
  (parent 54)
  (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
      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-0) (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) (ra-1 ra-0) (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-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 79)
  (parent 57)
  (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-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 80)
  (parent 58)
  (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 81)
  (parent 59)
  (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 82)
  (parent 61)
  (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
      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-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-1) (rb ra-prime-1) (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)) ((2 1) (7 1)) ((3 1) (2 0)) ((4 2) (1 2))
    ((5 3) (0 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-1 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 (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)))
    ((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-1))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) (enc ra-prime-1 k)))))
  (label 83)
  (parent 64)
  (unrealized (7 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
      ra-prime-2 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) (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-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)) ((2 1) (7 0)) ((3 1) (2 0)) ((4 2) (1 2))
    ((5 3) (0 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-1 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 (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)))
    ((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-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k))))
  (label 84)
  (parent 64)
  (unrealized (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 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) (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-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)) ((2 1) (7 0)) ((3 1) (2 0)) ((4 2) (1 2))
    ((5 3) (0 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-1 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 (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)))
    ((recv (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-1))
      (send (cat rb-prime-0 (enc ra-prime-1 k)))))
  (label 85)
  (parent 64)
  (unrealized (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
      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))
  (deflistener k)
  (precedes ((0 1) (5 2)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
    ((2 1) (6 0)) ((2 1) (7 0)) ((3 1) (2 0)) ((4 2) (1 2))
    ((5 3) (0 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-1 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 (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))) ((recv k) (send k)))
  (label 86)
  (parent 64)
  (unrealized (7 0))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb rb-0 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) (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 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) (2 0)) ((1 1) (3 1)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((3 0) (0 0)) ((3 2) (1 2)) ((4 3) (0 2))
    ((5 1) (4 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 (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 87)
  (parent 65)
  (unrealized)
  (comment "aborted"))

(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-reauth 4 (ra-prime ra-prime) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (5 2)) ((1 1) (4 1)) ((1 1) (5 2)) ((2 1) (5 0))
    ((3 1) (2 0)) ((4 2) (1 2)) ((5 1) (1 0)) ((5 3) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb ra-prime rb-prime k)
  (operation collapsed 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 (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))
      (recv (cat rb (enc ra-prime k))) (send (enc rb k))))
  (label 88)
  (parent 65)
  (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
      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-reauth 4 (ra-prime ra-prime-1) (rb-prime rb) (tb tb)
    (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (ra ra-1) (rb ra-prime-1) (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)) ((2 1) (7 1)) ((3 1) (2 0))
    ((4 3) (1 2)) ((5 2) (4 2)) ((6 3) (0 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-1 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 (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)))
    ((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-1))
      (send (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) (enc ra-prime-1 k)))))
  (label 89)
  (parent 68)
  (unrealized (7 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
      ra-prime-2 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)
    (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-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)) ((2 1) (7 0)) ((3 1) (2 0))
    ((4 3) (1 2)) ((5 2) (4 2)) ((6 3) (0 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-1 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 (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)))
    ((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-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k))))
  (label 90)
  (parent 68)
  (unrealized (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 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)
    (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-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)) ((2 1) (7 0)) ((3 1) (2 0))
    ((4 3) (1 2)) ((5 2) (4 2)) ((6 3) (0 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-1 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 (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)))
    ((recv (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-1))
      (send (cat rb-prime-0 (enc ra-prime-1 k)))))
  (label 91)
  (parent 68)
  (unrealized (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
      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))
  (deflistener 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)) ((2 1) (7 0)) ((3 1) (2 0))
    ((4 3) (1 2)) ((5 2) (4 2)) ((6 3) (0 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-1 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 (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)))
    ((recv k) (send k)))
  (label 92)
  (parent 68)
  (unrealized (7 0))
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars (ra rb ra-prime rb-prime tb rb-0 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) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (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) (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) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
    ((2 1) (4 1)) ((2 1) (5 0)) ((3 3) (1 2)) ((4 0) (0 0))
    ((4 2) (3 2)) ((5 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 (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))
      (recv
        (cat (enc b ra 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 93)
  (parent 69)
  (unrealized)
  (comment "aborted"))

(defskeleton neuman-stubblebine
  (vars (ra ra-prime rb-prime tb ra-0 rb rb-0 ra-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 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 ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (4 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 ra-prime rb-prime k)
  (operation collapsed 6 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 (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 94)
  (parent 69)
  (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
      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-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))
  (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) (7 1)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 1)) ((2 1) (7 1)) ((3 1) (2 0))
    ((4 3) (1 2)) ((5 3) (4 2)) ((6 2) (5 2)) ((7 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 (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))))
    ((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 95)
  (parent 70)
  (unrealized (7 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
      ra-prime-2 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-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))
  (defstrand init-reauth 4 (ra-prime ra-prime-2) (rb-prime rb) (tb tb-0)
    (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (7 2)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 1)) ((2 1) (7 0)) ((3 1) (2 0))
    ((4 3) (1 2)) ((5 3) (4 2)) ((6 2) (5 2)) ((7 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 (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))))
    ((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-2))
      (recv (cat rb (enc ra-prime-2 k))) (send (enc rb k))))
  (label 96)
  (parent 70)
  (unrealized (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 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-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))
  (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) (7 0)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 1)) ((2 1) (7 0)) ((3 1) (2 0))
    ((4 3) (1 2)) ((5 3) (4 2)) ((6 2) (5 2)) ((7 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 (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))))
    ((recv (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) rb))
      (send (cat rb-prime-0 (enc rb k)))))
  (label 97)
  (parent 70)
  (unrealized (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
      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))
  (deflistener k)
  (precedes ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0)) ((2 1) (5 0))
    ((2 1) (6 1)) ((2 1) (7 0)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 3) (4 2)) ((6 2) (5 2)) ((7 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 (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))))
    ((recv k) (send k)))
  (label 98)
  (parent 70)
  (unrealized (7 0))
  (comment "aborted"))