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

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

(defprotocol neuman-stubblebine basic
  (defrole init
    (vars (a b ks name) (ra rb text) (k skey) (tb text) (tkt mesg))
    (trace (send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
      (send (cat tkt (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 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))
  (defrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2))
        (false))))
  (defrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))))

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

(defskeleton neuman-stubblebine
  (vars (ra tb rb 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 keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (precedes ((1 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb 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 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))))
  (label 1)
  (parent 0)
  (unrealized (0 2) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb 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 keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc a ra-0 tb (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 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))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb 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 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))
  (precedes ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb k)
  (operation encryption-test (added-strand resp 2)
    (enc a ra-0 tb (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 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))))))
  (label 3)
  (parent 1)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (tkt mesg) (ra tb rb rb-0 ra-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 keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init 3 (tkt tkt) (ra ra-0) (rb rb) (tb tb-0) (a a-0)
    (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((2 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb 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 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-0 ra-0))
      (recv (cat (enc b-0 ra-0 k tb-0 (ltk a-0 ks-0)) tkt rb))
      (send (cat tkt (enc rb k)))))
  (label 4)
  (parent 2)
  (unrealized (2 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb 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 keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((1 1) (2 0)) ((2 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb 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 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 (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars (tkt mesg) (ra tb rb 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 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 (tkt tkt) (ra ra-1) (rb rb) (tb tb-0) (a a-0)
    (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (3 1)) ((1 1) (3 1)) ((2 1) (1 0)) ((3 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb 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 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-0 ra-1))
      (recv (cat (enc b-0 ra-1 k tb-0 (ltk a-0 ks-0)) tkt rb))
      (send (cat tkt (enc rb k)))))
  (label 6)
  (parent 3)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb 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 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))
  (deflistener k)
  (precedes ((1 1) (3 0)) ((2 1) (1 0)) ((3 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb 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 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 k) (send k)))
  (label 7)
  (parent 3)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars (tkt mesg) (ra tb rb 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 keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init 3 (tkt tkt) (ra ra) (rb rb) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-0 ra) (tb-0 tb)) k (2 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 rb 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)) tkt rb))
      (send (cat tkt (enc rb k)))))
  (label 8)
  (parent 4)
  (realized)
  (shape)
  (maps ((0) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k))))
  (origs (k (1 1)) (ra (2 0)) (rb (0 1))))

(defskeleton neuman-stubblebine
  (vars (tkt mesg) (ra tb rb 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 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 (tkt tkt) (ra ra-0) (rb rb) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (precedes ((0 1) (3 1)) ((1 1) (3 1)) ((2 1) (1 0)) ((3 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-1 ra-0) (tb-0 tb)) k (3 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 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)) tkt rb))
      (send (cat tkt (enc rb k)))))
  (label 9)
  (parent 6)
  (realized)
  (shape)
  (maps ((0) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k))))
  (origs (k (1 1)) (rb (0 1))))

(comment "Nothing left to do")

(defprotocol neuman-stubblebine basic
  (defrole init
    (vars (a b ks name) (ra rb text) (k skey) (tb text) (tkt mesg))
    (trace (send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
      (send (cat tkt (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 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))
  (defrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2))
        (false))))
  (defrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))))

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

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

(defskeleton neuman-stubblebine
  (vars (tkt mesg) (ra tb rb rb-0 rb-1 text) (a b ks name) (k skey))
  (defstrand init 3 (tkt tkt) (ra ra) (rb rb) (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 2 (ra ra) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb k)
  (operation encryption-test (added-strand resp 2)
    (enc a ra tb (ltk b ks)) (1 0))
  (traces
    ((send (cat a ra)) (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
      (send (cat tkt (enc rb 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 a ra)) (send (cat b rb-1 (enc a ra tb (ltk b ks))))))
  (label 12)
  (parent 11)
  (realized)
  (shape)
  (maps
    ((0) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (tkt tkt))))
  (origs (k (1 1)) (ra (0 0))))

(comment "Nothing left to do")

(defprotocol neuman-stubblebine basic
  (defrole init
    (vars (a b ks name) (ra rb text) (k skey) (tb text) (tkt mesg))
    (trace (send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
      (send (cat tkt (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 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))
  (defrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2))
        (false))))
  (defrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))))

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

(defskeleton neuman-stubblebine
  (vars (ra tb rb 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 keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (precedes ((1 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb 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 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))))
  (label 14)
  (parent 13)
  (unrealized (0 2) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb 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 keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb k)
  (operation encryption-test (displaced 2 0 resp 2)
    (enc a ra-0 tb (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 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 15)
  (parent 14)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb 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 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))
  (precedes ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb k)
  (operation encryption-test (added-strand resp 2)
    (enc a ra-0 tb (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 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))))))
  (label 16)
  (parent 14)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (tkt mesg) (ra tb rb rb-0 ra-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 keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init 3 (tkt tkt) (ra ra-0) (rb rb) (tb tb-0) (a a-0)
    (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((2 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb 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 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-0 ra-0))
      (recv (cat (enc b-0 ra-0 k tb-0 (ltk a-0 ks-0)) tkt rb))
      (send (cat tkt (enc rb k)))))
  (label 17)
  (parent 15)
  (unrealized (2 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb 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 keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((1 1) (2 0)) ((2 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb 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 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 18)
  (parent 15)
  (unrealized (2 0))
  (dead)
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars (tkt mesg) (ra tb rb 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 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 (tkt tkt) (ra ra-1) (rb rb) (tb tb-0) (a a-0)
    (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (3 1)) ((1 1) (3 1)) ((2 1) (1 0)) ((3 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb 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 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-0 ra-1))
      (recv (cat (enc b-0 ra-1 k tb-0 (ltk a-0 ks-0)) tkt rb))
      (send (cat tkt (enc rb k)))))
  (label 19)
  (parent 16)
  (unrealized (3 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine
  (vars (ra tb rb 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 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))
  (deflistener k)
  (precedes ((1 1) (3 0)) ((2 1) (1 0)) ((3 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb 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 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 k) (send k)))
  (label 20)
  (parent 16)
  (unrealized (3 0))
  (dead)
  (comment "empty cohort"))

(defskeleton neuman-stubblebine
  (vars (tkt mesg) (ra tb rb 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 keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
    (k k))
  (defstrand init 3 (tkt tkt) (ra ra) (rb rb) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-0 ra) (tb-0 tb)) k (2 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 rb 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)) tkt rb))
      (send (cat tkt (enc rb k)))))
  (label 21)
  (parent 17)
  (realized)
  (shape)
  (maps ((0) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k))))
  (origs (k (1 1)) (ra (2 0)) (rb (0 1))))

(defskeleton neuman-stubblebine
  (vars (tkt mesg) (ra tb rb 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 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 (tkt tkt) (ra ra-0) (rb rb) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (precedes ((0 1) (3 1)) ((1 1) (3 1)) ((2 1) (1 0)) ((3 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-1 ra-0) (tb-0 tb)) k (3 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 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)) tkt rb))
      (send (cat tkt (enc rb k)))))
  (label 22)
  (parent 19)
  (realized)
  (shape)
  (maps ((0) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k))))
  (origs (k (1 1)) (rb (0 1))))

(comment "Nothing left to do")

(defprotocol neuman-stubblebine basic
  (defrole init
    (vars (a b ks name) (ra rb text) (k skey) (tb text) (tkt mesg))
    (trace (send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
      (send (cat tkt (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 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))
  (defrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2))
        (false))))
  (defrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))))

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

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

(defskeleton neuman-stubblebine
  (vars (tkt mesg) (ra tb rb rb-0 rb-1 text) (a b ks name) (k skey))
  (defstrand init 3 (tkt tkt) (ra ra) (rb rb) (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 2 (ra ra) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra rb k)
  (operation encryption-test (added-strand resp 2)
    (enc a ra tb (ltk b ks)) (1 0))
  (traces
    ((send (cat a ra)) (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
      (send (cat tkt (enc rb 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 a ra)) (send (cat b rb-1 (enc a ra tb (ltk b ks))))))
  (label 25)
  (parent 24)
  (realized)
  (shape)
  (maps
    ((0) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (tkt tkt))))
  (origs (k (1 1)) (ra (0 0))))

(comment "Nothing left to do")

(defprotocol neuman-stubblebine-reauth basic
  (defrole init
    (vars (a b ks name) (ra rb tb text) (k skey) (tkt mesg))
    (trace (send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
      (send (cat tkt (enc rb k)))))
  (defrole resp
    (vars (a b ks name) (ra rb tb text) (k skey))
    (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 ra-prime rb-prime text) (k skey) (tb text)
      (tkt mesg))
    (trace (recv (cat (enc b ra k tb (ltk a ks)) tkt))
      (send (cat tkt ra-prime)) (recv (cat rb-prime (enc ra-prime k)))
      (send (enc rb-prime k))))
  (defrole resp-reauth
    (vars (a b ks name) (tb ra-prime rb-prime text) (k skey))
    (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))
  (defrule cakeRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
          (leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2))
        (false))))
  (defrule no-interruption
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (leads-to z0 i0 z2 i2) (trans z1 i1)
          (same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
        (false))))
  (defrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (defrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defrule scissorsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
        (and (= z1 z2) (= i1 i2)))))
  (defrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))))

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

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

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

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

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

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

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

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

(defskeleton neuman-stubblebine-reauth
  (vars (tkt mesg) (ra-prime rb-prime tb ra rb rb-0 text) (a b ks name)
    (k skey))
  (defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
    (rb-prime rb-prime) (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 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (tkt tkt) (ra ra) (rb rb-prime) (tb tb) (a a) (b b)
    (ks ks) (k k))
  (precedes ((0 1) (3 1)) ((1 1) (0 0)) ((2 1) (1 0)) ((3 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-0 ra) (tb-0 tb)) k (3 1)
    (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
  (traces
    ((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 a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
    ((send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) tkt rb-prime))
      (send (cat tkt (enc rb-prime k)))))
  (label 34)
  (parent 30)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
        (tb tb))))
  (origs (k (1 1)) (rb-prime (0 1))))

(defskeleton neuman-stubblebine-reauth
  (vars (ra-prime rb-prime tb ra rb rb-0 rb-prime-0 text) (a b ks name)
    (k skey))
  (defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
    (rb-prime rb-prime) (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 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (tb tb) (ra-prime rb-prime)
    (rb-prime rb-prime-0) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (3 0)) ((1 1) (0 0)) ((2 1) (1 0)) ((3 1) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra-prime rb-prime k)
  (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 (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 a ra)) (send (cat b rb-0 (enc a ra 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 35)
  (parent 31)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
        (tb tb))))
  (origs (k (1 1)) (rb-prime (0 1))))

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

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

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

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

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

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

(defskeleton neuman-stubblebine-reauth
  (vars (tkt tkt-0 mesg)
    (ra-prime rb-prime tb ra rb rb-0 ra-prime-0 text) (a b ks name)
    (k skey))
  (defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
    (rb-prime rb-prime) (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 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (tkt tkt-0) (ra ra) (rb ra-prime-0) (tb tb) (a a)
    (b b) (ks ks) (k k))
  (precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 1))
    ((2 1) (1 0)) ((3 3) (0 2)) ((4 2) (3 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-0 ra) (tb-0 tb)) k (4 1)
    (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
  (traces
    ((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 a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt))
      (send (cat tkt 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)) tkt-0 ra-prime-0))
      (send (cat tkt-0 (enc ra-prime-0 k)))))
  (label 42)
  (parent 37)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
        (tb tb))))
  (origs (k (1 1)) (rb-prime (0 1))))

(defskeleton neuman-stubblebine-reauth
  (vars (tkt mesg)
    (ra-prime rb-prime tb ra rb rb-0 ra-prime-0 rb-prime-0 text)
    (a b ks name) (k skey))
  (defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
    (rb-prime rb-prime) (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 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (tb tb) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
    ((2 1) (1 0)) ((3 3) (0 2)) ((4 1) (3 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra-prime rb-prime k)
  (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 (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 a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt))
      (send (cat tkt 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 43)
  (parent 39)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
        (tb tb))))
  (origs (k (1 1)) (rb-prime (0 1))))

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

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

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

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

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

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

(defskeleton neuman-stubblebine-reauth
  (vars (tkt tkt-0 tkt-1 mesg)
    (ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 text)
    (a b ks name) (k skey))
  (defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
    (rb-prime rb-prime) (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 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
    (rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (tkt tkt-1) (ra ra) (rb ra-prime-1) (tb tb) (a a)
    (b b) (ks ks) (k k))
  (precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
    ((1 1) (5 1)) ((2 1) (1 0)) ((3 3) (0 2)) ((4 3) (3 2))
    ((5 2) (4 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-0 ra) (tb-0 tb)) k (5 1)
    (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
  (traces
    ((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 a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt))
      (send (cat tkt ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
      (send (cat tkt-0 ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) tkt-1 ra-prime-1))
      (send (cat tkt-1 (enc ra-prime-1 k)))))
  (label 50)
  (parent 45)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
        (tb tb))))
  (origs (k (1 1)) (rb-prime (0 1))))

(defskeleton neuman-stubblebine-reauth
  (vars (tkt tkt-0 mesg)
    (ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 rb-prime-0
      text) (a b ks name) (k skey))
  (defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
    (rb-prime rb-prime) (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 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
    (rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (tb tb) (ra-prime ra-prime-1)
    (rb-prime rb-prime-0) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
    ((1 1) (5 0)) ((2 1) (1 0)) ((3 3) (0 2)) ((4 3) (3 2))
    ((5 1) (4 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig 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 k tb (ltk a ks)))
  (traces
    ((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 a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt))
      (send (cat tkt ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
      (send (cat tkt-0 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 51)
  (parent 47)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
        (tb tb))))
  (origs (k (1 1)) (rb-prime (0 1))))

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

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

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

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

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

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

(defskeleton neuman-stubblebine-reauth
  (vars (tkt tkt-0 tkt-1 tkt-2 mesg)
    (ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 ra-prime-2
      text) (a b ks name) (k skey))
  (defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
    (rb-prime rb-prime) (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 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
    (rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-1) (ra ra) (ra-prime ra-prime-2)
    (rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (tkt tkt-2) (ra ra) (rb ra-prime-2) (tb tb) (a a)
    (b b) (ks ks) (k k))
  (precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
    ((1 1) (5 0)) ((1 1) (6 1)) ((2 1) (1 0)) ((3 3) (0 2))
    ((4 3) (3 2)) ((5 3) (4 2)) ((6 2) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra-prime rb-prime k)
  (operation nonce-test
    (contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-0 ra) (tb-0 tb)) k (6 1)
    (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
  (traces
    ((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 a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt))
      (send (cat tkt ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
      (send (cat tkt-0 ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-1))
      (send (cat tkt-1 ra-prime-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k)))
    ((send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) tkt-2 ra-prime-2))
      (send (cat tkt-2 (enc ra-prime-2 k)))))
  (label 58)
  (parent 53)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
        (tb tb))))
  (origs (k (1 1)) (rb-prime (0 1))))

(defskeleton neuman-stubblebine-reauth
  (vars (tkt tkt-0 tkt-1 mesg)
    (ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 ra-prime-2
      rb-prime-0 text) (a b ks name) (k skey))
  (defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
    (rb-prime rb-prime) (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 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
    (rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-1) (ra ra) (ra-prime ra-prime-2)
    (rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (tb tb) (ra-prime ra-prime-2)
    (rb-prime rb-prime-0) (a a) (b b) (ks ks) (k k))
  (precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
    ((1 1) (5 0)) ((1 1) (6 0)) ((2 1) (1 0)) ((3 3) (0 2))
    ((4 3) (3 2)) ((5 3) (4 2)) ((6 1) (5 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig 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 k tb (ltk a ks)))
  (traces
    ((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 a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt))
      (send (cat tkt ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
      (send (cat tkt-0 ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-1))
      (send (cat tkt-1 ra-prime-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-2))
      (send (cat rb-prime-0 (enc ra-prime-2 k)))))
  (label 59)
  (parent 55)
  (realized)
  (shape)
  (maps
    ((0)
      ((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
        (tb tb))))
  (origs (k (1 1)) (rb-prime (0 1))))

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

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

(defskeleton neuman-stubblebine-reauth
  (vars (tkt tkt-0 tkt-1 tkt-2 tkt-3 mesg)
    (ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 ra-prime-2
      ra-prime-3 ra-0 ra-prime-4 tb-0 text) (a b ks a-0 b-0 ks-0 name)
    (k skey))
  (defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
    (rb-prime rb-prime) (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 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
    (rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-1) (ra ra) (ra-prime ra-prime-2)
    (rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-2) (ra ra) (ra-prime ra-prime-3)
    (rb-prime ra-prime-2) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-3) (ra ra-0) (ra-prime ra-prime-4)
    (rb-prime ra-prime-3) (tb tb-0) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
    ((1 1) (5 0)) ((1 1) (6 0)) ((1 1) (7 0)) ((2 1) (1 0))
    ((3 3) (0 2)) ((4 3) (3 2)) ((5 3) (4 2)) ((6 3) (5 2))
    ((7 3) (6 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra-prime rb-prime k)
  (operation encryption-test (added-strand init-reauth 4)
    (enc ra-prime-3 k) (6 2))
  (traces
    ((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 a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt))
      (send (cat tkt ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
      (send (cat tkt-0 ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-1))
      (send (cat tkt-1 ra-prime-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-2))
      (send (cat tkt-2 ra-prime-3))
      (recv (cat ra-prime-2 (enc ra-prime-3 k)))
      (send (enc ra-prime-2 k)))
    ((recv (cat (enc b-0 ra-0 k tb-0 (ltk a-0 ks-0)) tkt-3))
      (send (cat tkt-3 ra-prime-4))
      (recv (cat ra-prime-3 (enc ra-prime-4 k)))
      (send (enc ra-prime-3 k))))
  (label 60)
  (parent 57)
  (unrealized (7 0) (7 2))
  (aborted)
  (comment "aborted"))

(defskeleton neuman-stubblebine-reauth
  (vars (tkt tkt-0 tkt-1 tkt-2 tkt-3 mesg)
    (ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 ra-prime-2
      ra-prime-3 ra-0 tb-0 text) (a b ks a-0 b-0 ks-0 name) (k skey))
  (defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
    (rb-prime rb-prime) (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 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
    (rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-1) (ra ra) (ra-prime ra-prime-2)
    (rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-2) (ra ra) (ra-prime ra-prime-3)
    (rb-prime ra-prime-2) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init 3 (tkt tkt-3) (ra ra-0) (rb ra-prime-3) (tb tb-0)
    (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
    ((1 1) (5 0)) ((1 1) (6 0)) ((1 1) (7 1)) ((2 1) (1 0))
    ((3 3) (0 2)) ((4 3) (3 2)) ((5 3) (4 2)) ((6 3) (5 2))
    ((7 2) (6 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra-prime rb-prime k)
  (operation encryption-test (added-strand init 3) (enc ra-prime-3 k)
    (6 2))
  (traces
    ((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 a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt))
      (send (cat tkt ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
      (send (cat tkt-0 ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-1))
      (send (cat tkt-1 ra-prime-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-2))
      (send (cat tkt-2 ra-prime-3))
      (recv (cat ra-prime-2 (enc ra-prime-3 k)))
      (send (enc ra-prime-2 k)))
    ((send (cat a-0 ra-0))
      (recv (cat (enc b-0 ra-0 k tb-0 (ltk a-0 ks-0)) tkt-3 ra-prime-3))
      (send (cat tkt-3 (enc ra-prime-3 k)))))
  (label 61)
  (parent 57)
  (unrealized (7 1))
  (aborted)
  (comment "aborted"))

(defskeleton neuman-stubblebine-reauth
  (vars (tkt tkt-0 tkt-1 tkt-2 mesg)
    (ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 ra-prime-2
      ra-prime-3 tb-0 rb-prime-0 text) (a b ks a-0 b-0 ks-0 name)
    (k skey))
  (defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
    (rb-prime rb-prime) (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 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
    (rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-1) (ra ra) (ra-prime ra-prime-2)
    (rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand init-reauth 4 (tkt tkt-2) (ra ra) (ra-prime ra-prime-3)
    (rb-prime ra-prime-2) (tb tb) (a a) (b b) (ks ks) (k k))
  (defstrand resp-reauth 2 (tb tb-0) (ra-prime ra-prime-3)
    (rb-prime rb-prime-0) (a a-0) (b b-0) (ks ks-0) (k k))
  (precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
    ((1 1) (5 0)) ((1 1) (6 0)) ((1 1) (7 0)) ((2 1) (1 0))
    ((3 3) (0 2)) ((4 3) (3 2)) ((5 3) (4 2)) ((6 3) (5 2))
    ((7 1) (6 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig ra-prime rb-prime k)
  (operation encryption-test (added-strand resp-reauth 2)
    (enc ra-prime-3 k) (6 2))
  (traces
    ((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 a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt))
      (send (cat tkt ra-prime-0))
      (recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
      (send (cat tkt-0 ra-prime-1))
      (recv (cat ra-prime-0 (enc ra-prime-1 k)))
      (send (enc ra-prime-0 k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-1))
      (send (cat tkt-1 ra-prime-2))
      (recv (cat ra-prime-1 (enc ra-prime-2 k)))
      (send (enc ra-prime-1 k)))
    ((recv (cat (enc b ra k tb (ltk a ks)) tkt-2))
      (send (cat tkt-2 ra-prime-3))
      (recv (cat ra-prime-2 (enc ra-prime-3 k)))
      (send (enc ra-prime-2 k)))
    ((recv (cat (enc a-0 k tb-0 (ltk b-0 ks-0)) ra-prime-3))
      (send (cat rb-prime-0 (enc ra-prime-3 k)))))
  (label 63)
  (parent 57)
  (unrealized (7 0))
  (aborted)
  (comment "aborted"))

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