(herald neuman-stubblebine-reauth (bound 8))

(comment "CPSA 4.3.1")
(comment "All input read from tst/neuman-stubblebine-reauth-tagged.lsp")

(defprotocol neuman-stubblebine-reauth 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 "one" 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 "one" 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 "two" ra-prime k)))
      (send (enc "three" 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 "two" ra-prime k)))
      (recv (enc "three" 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))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime tb-0 text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (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 "one" rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" rb-prime k))))
  (label 0)
  (unrealized (0 2) (1 0))
  (origs (rb (0 1)) (rb-prime (1 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks))
  (precedes ((2 1) (0 2)) ((2 1) (1 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (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 "one" rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "2 in cohort - 2 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime rb-0 text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (precedes ((0 1) (2 0)) ((2 1) (0 2)) ((2 1) (1 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 3 0 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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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))))
  (label 2)
  (parent 1)
  (unrealized (0 2) (1 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks))
  (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 k ra rb ra-prime rb-prime)
  (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 "one" rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 3)
  (parent 1)
  (unrealized (0 2) (1 2))
  (comment "2 in cohort - 2 not yet seen"))

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

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime rb-0 text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (deflistener k)
  (precedes ((0 1) (2 0)) ((2 1) (0 2)) ((2 1) (1 0)) ((2 1) (3 0))
    ((3 1) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (added-listener k) (enc "three" 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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 k) (send k)))
  (label 5)
  (parent 2)
  (unrealized (0 2) (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (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))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb-1) (a a-0) (b b-0) (ks ks-0))
  (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 k ra rb ra-prime rb-prime)
  (operation encryption-test (added-strand init-reauth 4)
    (enc "three" 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 "one" rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k))))
  (label 6)
  (parent 3)
  (unrealized (0 2) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks))
  (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 k ra rb ra-prime rb-prime)
  (operation encryption-test (added-listener k) (enc "three" 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 "one" rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 7)
  (parent 3)
  (unrealized (0 2) (4 0))
  (dead)
  (comment "empty cohort"))

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

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb-0) (a a) (b b) (ks ks))
  (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 k ra rb ra-prime rb-prime)
  (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 "one" rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k))))
  (label 9)
  (parent 6)
  (unrealized (0 2) (4 2))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime rb-0 text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (0 2)) ((2 1) (3 0))
    ((3 1) (1 0)) ((3 3) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 4 1 resp-reauth 2)
    (enc "two" ra-prime-0 k) (3 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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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))
      (recv (cat rb-prime (enc "two" ra-prime k)))
      (send (enc "three" rb-prime k))))
  (label 10)
  (parent 8)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

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

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
  (deflistener k)
  (precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (0 2)) ((2 1) (1 0))
    ((2 1) (3 0)) ((2 1) (4 0)) ((3 3) (1 2)) ((4 1) (3 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (added-listener k) (enc "two" ra-prime-0 k)
    (3 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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k))) ((recv k) (send k)))
  (label 12)
  (parent 8)
  (unrealized (0 2) (4 0))
  (dead)
  (comment "empty cohort"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (4 0)) ((3 1) (2 0))
    ((4 1) (1 0)) ((4 3) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 5 1 resp-reauth 2)
    (enc "two" 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 "one" rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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))
      (recv (cat rb-prime (enc "two" ra-prime k)))
      (send (enc "three" rb-prime k))))
  (label 13)
  (parent 9)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (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))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (tb tb-1) (a a-0) (b b-0) (ks ks-0))
  (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 k ra rb ra-prime rb-prime)
  (operation encryption-test (added-strand resp-reauth 2)
    (enc "two" 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 "one" rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" 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 "two" ra-prime-0 k)))))
  (label 14)
  (parent 9)
  (unrealized (0 2) (5 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (ra tb rb ra-prime rb-prime tb-0 ra-0 rb-0 rb-1 ra-prime-0 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb-0) (a a) (b b) (ks ks))
  (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 k ra rb ra-prime rb-prime)
  (operation encryption-test (added-listener k) (enc "two" 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 "one" rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k))) ((recv k) (send k)))
  (label 15)
  (parent 9)
  (unrealized (0 2) (5 0))
  (dead)
  (comment "empty cohort"))

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

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime rb-0 text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (deflistener k)
  (precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (3 0)) ((2 1) (4 0))
    ((3 1) (1 0)) ((3 3) (1 2)) ((4 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (added-listener k) (enc "one" 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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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))
      (recv (cat rb-prime (enc "two" ra-prime k)))
      (send (enc "three" rb-prime k))) ((recv k) (send k)))
  (label 17)
  (parent 10)
  (unrealized (4 0))
  (dead)
  (comment "empty cohort"))

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

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (precedes ((1 1) (4 2)) ((2 1) (0 2)) ((2 1) (4 0)) ((3 1) (2 0))
    ((4 1) (1 0)) ((4 3) (1 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 5 2 keyserver 2)
    (enc a k tb-0 (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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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))
      (recv (cat rb-prime (enc "two" ra-prime k)))
      (send (enc "three" rb-prime k))))
  (label 19)
  (parent 13)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (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))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb-0) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb-0) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (tb tb-0) (a a) (b b) (ks ks))
  (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 k ra rb ra-prime rb-prime)
  (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 "one" rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k)))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc "two" ra-prime-0 k)))))
  (label 20)
  (parent 14)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 ra-0 tb-0
      text) (a b ks a-0 b-0 ks-0 name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (ra ra-0) (rb rb) (tb tb-0) (a a-0) (b b-0)
    (ks ks-0))
  (precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
    ((2 1) (4 0)) ((2 1) (5 1)) ((3 3) (1 2)) ((4 1) (3 2))
    ((5 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (added-strand init 3) (enc "one" 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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc "two" ra-prime-0 k))))
    ((send (cat a-0 ra-0))
      (recv
        (cat (enc b-0 ra-0 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 "one" rb k)))))
  (label 22)
  (parent 18)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
  (deflistener k)
  (precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
    ((2 1) (4 0)) ((2 1) (5 0)) ((3 3) (1 2)) ((4 1) (3 2))
    ((5 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (added-listener k) (enc "one" 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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc "two" ra-prime-0 k))))
    ((recv k) (send k)))
  (label 23)
  (parent 18)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (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))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (ra ra-1) (rb rb) (tb tb-0) (a a-0) (b b-0)
    (ks ks-0))
  (precedes ((0 1) (5 1)) ((1 1) (4 2)) ((2 1) (4 0)) ((2 1) (5 1))
    ((3 1) (2 0)) ((4 1) (1 0)) ((4 3) (1 2)) ((5 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (added-strand init 3) (enc "one" 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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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))
      (recv (cat rb-prime (enc "two" ra-prime k)))
      (send (enc "three" 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 "one" rb k)))))
  (label 24)
  (parent 19)
  (unrealized (5 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (deflistener k)
  (precedes ((1 1) (4 2)) ((2 1) (4 0)) ((2 1) (5 0)) ((3 1) (2 0))
    ((4 1) (1 0)) ((4 3) (1 2)) ((5 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (added-listener k) (enc "one" 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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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))
      (recv (cat rb-prime (enc "two" ra-prime k)))
      (send (enc "three" rb-prime k))) ((recv k) (send k)))
  (label 25)
  (parent 19)
  (unrealized (5 0))
  (dead)
  (comment "empty cohort"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
  (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 k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 6 2 keyserver 2)
    (enc a k tb-0 (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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc "two" ra-prime-0 k)))))
  (label 26)
  (parent 20)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime rb-0 text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (3 0)) ((2 1) (4 1))
    ((3 1) (1 0)) ((3 3) (1 2)) ((4 0) (0 0)) ((4 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 5 2 keyserver 2)
    (enc b ra-0 k tb (ltk a ks)) (4 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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))
      (recv (cat rb-prime (enc "two" ra-prime k)))
      (send (enc "three" 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 "one" rb k)))))
  (label 27)
  (parent 21)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
        (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
  (origs (k (2 1)) (ra (4 0)) (rb (0 1)) (ra-prime (3 1))
    (rb-prime (1 1))))

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

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

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (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))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (ra ra-1) (rb rb) (tb tb-0) (a a-0) (b b-0)
    (ks ks-0))
  (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 k ra rb ra-prime rb-prime)
  (operation encryption-test (added-strand init 3) (enc "one" 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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc "two" 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 "one" rb k)))))
  (label 30)
  (parent 26)
  (unrealized (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
  (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 k ra rb ra-prime rb-prime)
  (operation encryption-test (added-listener k) (enc "one" 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 "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc "two" ra-prime-0 k))))
    ((recv k) (send k)))
  (label 31)
  (parent 26)
  (unrealized (6 0))
  (dead)
  (comment "empty cohort"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
    ((2 1) (4 0)) ((2 1) (5 1)) ((3 3) (1 2)) ((4 1) (3 2))
    ((5 0) (0 0)) ((5 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 6 2 keyserver 2)
    (enc b ra-0 k tb (ltk a ks)) (5 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc "two" ra-prime-0 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 "one" rb k)))))
  (label 32)
  (parent 28)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
        (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
  (origs (k (2 1)) (ra (5 0)) (rb (0 1)) (rb-prime (1 1))))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (precedes ((0 1) (5 1)) ((1 1) (4 2)) ((2 1) (4 0)) ((2 1) (5 1))
    ((3 1) (2 0)) ((4 1) (1 0)) ((4 3) (1 2)) ((5 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 6 2 keyserver 2)
    (enc b ra-1 k tb (ltk a ks)) (5 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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))
      (recv (cat rb-prime (enc "two" ra-prime k)))
      (send (enc "three" 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 "one" rb k)))))
  (label 33)
  (parent 29)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
        (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
  (origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1))))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      ra-1 text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (ra ra-1) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (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 k ra rb ra-prime rb-prime)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
    k (6 1) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc "two" ra-prime-0 k))))
    ((send (cat a ra-1))
      (recv
        (cat (enc b ra-1 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc "one" rb k)))))
  (label 34)
  (parent 30)
  (unrealized (6 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (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 k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 7 2 keyserver 2)
    (enc b ra-1 k tb (ltk a ks)) (6 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" 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 "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc "two" 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 "one" rb k)))))
  (label 35)
  (parent 34)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
        (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
  (origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))

(comment "Nothing left to do")