cpsa-4.4.4: tst/neuman-stubblebine-reauth_shapes.tst
(comment "CPSA 4.3.1")
(comment "Extracted shapes")
(herald neuman-stubblebine-reauth (bound 8))
(comment "CPSA 4.3.1")
(comment "All input read from tst/neuman-stubblebine-reauth.lsp")
(defprotocol neuman-stubblebine-reauth basic
(defrole init
(vars (a b ks name) (ra rb text) (k skey) (tb text))
(trace (send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(defrole resp
(vars (a b ks name) (ra rb text) (k skey) (tb text))
(trace (recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(defrole init-reauth
(vars (a b ks name) (ra-prime rb-prime text) (k skey) (tb text))
(trace (recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb-prime (enc ra-prime k))) (send (enc rb-prime k))))
(defrole resp-reauth
(vars (a b ks name) (ra-prime rb-prime text) (k skey) (tb text))
(trace (recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k))))
(defrole keyserver
(vars (a b ks name) (ra rb text) (k skey) (tb text))
(trace (recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
(uniq-orig k))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime tb-0 text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb-0) (a a) (b b) (ks ks))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k))))
(label 0)
(unrealized (0 2) (1 0))
(origs (rb (0 1)) (rb-prime (1 1)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb ra-prime rb-prime rb rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (0 2)) ((1 1) (3 0)) ((2 1) (1 0))
((3 1) (1 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 4 1 resp-reauth 2) (enc rb-0 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k)))))
(label 26)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb ra-prime rb-prime rb text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (2 0)) ((1 1) (0 2)) ((1 1) (3 1)) ((2 1) (1 0))
((3 0) (0 0)) ((3 2) (1 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 4 1 resp-reauth 2) (enc rb-0 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k)))))
(label 45)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (3 0)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 rb-prime-0 rb-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-1)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 0)) ((2 1) (1 0)) ((2 1) (4 0))
((3 1) (1 2)) ((4 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (4 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-1 (enc rb k)))))
(label 50)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra ra-prime rb-prime tb ra-0 rb rb-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (4 0)) ((2 1) (1 0))
((3 1) (2 0)) ((4 1) (1 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 5 1 resp-reauth 2) (enc rb-1 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra-0)) (send (cat b rb-0 (enc a ra-0 tb (ltk b ks)))))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k)))))
(label 58)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime rb-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-0)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (3 0)) ((2 1) (4 0))
((3 1) (1 0)) ((3 3) (1 2)) ((4 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (4 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb-prime (enc ra-prime k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-0 (enc rb k)))))
(label 69)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (3 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb ra-prime rb-prime rb ra-prime-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (0 2)) ((1 1) (3 2)) ((2 1) (1 0))
((2 1) (3 0)) ((2 1) (4 0)) ((3 3) (1 2)) ((4 1) (3 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 5 1 resp-reauth 2) (enc rb-0 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k)))))
(label 72)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime rb-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-0)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 1)) ((2 1) (1 0)) ((2 1) (4 0))
((3 0) (0 0)) ((3 2) (1 2)) ((4 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (4 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-0 (enc rb k)))))
(label 77)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (3 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime rb-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 0)) ((1 1) (4 2)) ((2 1) (4 0))
((3 1) (1 2)) ((4 1) (1 0)) ((4 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 5 1 resp-reauth 2)
(enc ra-prime-0 k) (4 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb (enc ra-prime k))) (send (enc rb k))))
(label 80)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime rb-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 0)) ((2 1) (1 0)) ((2 1) (4 1))
((3 1) (1 2)) ((4 0) (0 0)) ((4 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 5 2 keyserver 2)
(enc b ra-0 k tb (ltk a ks)) (4 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 83)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (4 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra ra-prime rb-prime tb ra-0 rb rb-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (4 1)) ((2 1) (1 0))
((3 1) (2 0)) ((4 2) (1 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 5 1 resp-reauth 2) (enc rb-1 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra-0)) (send (cat b rb-0 (enc a ra-0 tb (ltk b ks)))))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k)))))
(label 97)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 rb-prime-1
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-1)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 0)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
((3 1) (2 0)) ((4 1) (1 2)) ((5 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (5 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-1 (enc rb k)))))
(label 102)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb ra-prime rb-prime rb ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (2 0)) ((1 1) (0 2)) ((1 1) (3 2)) ((2 1) (1 0))
((2 1) (3 0)) ((2 1) (4 1)) ((3 3) (1 2)) ((4 0) (0 0))
((4 2) (3 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 5 1 resp-reauth 2) (enc rb-0 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k)))))
(label 112)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (4 0)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime rb-0 text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (3 0)) ((2 1) (4 1))
((3 1) (1 0)) ((3 3) (1 2)) ((4 0) (0 0)) ((4 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 5 2 keyserver 2)
(enc b ra-0 k tb (ltk a ks)) (4 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb-prime (enc ra-prime k))) (send (enc rb-prime k)))
((send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 119)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (4 0)) (rb (0 1)) (ra-prime (3 1))
(rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 rb-prime-1
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-1)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 0)) ((3 3) (1 2)) ((4 1) (3 2))
((5 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation 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 a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k))))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-1 (enc rb k)))))
(label 122)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime rb-0 text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 1)) ((1 1) (4 2)) ((2 1) (4 0))
((3 0) (0 0)) ((3 2) (1 2)) ((4 1) (1 0)) ((4 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 5 1 resp-reauth 2)
(enc ra-prime-0 k) (4 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb (enc ra-prime k))) (send (enc rb k))))
(label 125)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (3 0)) (rb (0 1)) (ra-prime (4 1))
(rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 rb-prime-0 ra-prime-0 rb-prime-1
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 0)) ((2 1) (1 0)) ((2 1) (4 0))
((2 1) (5 0)) ((3 1) (1 2)) ((4 3) (0 2)) ((5 1) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (5 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-1 (enc ra-prime-0 k)))))
(label 130)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-0)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 0)) ((1 1) (4 2)) ((2 1) (4 0)) ((2 1) (5 0))
((3 1) (2 0)) ((4 1) (1 0)) ((4 3) (1 2)) ((5 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (5 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb-prime (enc ra-prime k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-0 (enc rb k)))))
(label 138)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra ra-prime rb-prime tb ra-0 rb rb-0 ra-prime-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (4 2)) ((2 1) (1 0))
((2 1) (4 0)) ((2 1) (5 0)) ((3 1) (2 0)) ((4 3) (1 2))
((5 1) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 6 1 resp-reauth 2) (enc rb-1 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra-0)) (send (cat b rb-0 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k)))))
(label 141)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-0)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 0)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
((3 1) (2 0)) ((4 2) (1 2)) ((5 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (5 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-0 (enc rb k)))))
(label 146)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 2)) ((1 1) (4 0)) ((1 1) (5 2)) ((2 1) (5 0))
((3 1) (2 0)) ((4 1) (1 2)) ((5 1) (1 0)) ((5 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 1 resp-reauth 2)
(enc ra-prime-0 k) (5 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb (enc ra-prime k))) (send (enc rb k))))
(label 149)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (5 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 1)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 1))
((3 1) (2 0)) ((4 1) (1 2)) ((5 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 2 keyserver 2)
(enc b ra-1 k tb (ltk a ks)) (5 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 152)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-0)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (4 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 0)) ((3 3) (1 2)) ((4 1) (1 0)) ((4 3) (3 2))
((5 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (5 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-0 (enc rb k)))))
(label 161)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb ra-prime rb-prime rb ra-prime-0 ra-prime-1 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (0 2)) ((1 1) (3 2)) ((2 1) (1 0))
((2 1) (3 0)) ((2 1) (4 0)) ((2 1) (5 0)) ((3 3) (1 2))
((4 3) (3 2)) ((5 1) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 6 1 resp-reauth 2) (enc rb-0 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-0 (enc ra-prime-1 k)))))
(label 164)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-0)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 1)) ((2 1) (5 0)) ((3 3) (1 2)) ((4 0) (0 0))
((4 2) (3 2)) ((5 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (5 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-0 (enc rb k)))))
(label 169)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (4 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 0)) ((3 1) (1 0)) ((3 3) (1 2)) ((4 3) (0 2))
((5 1) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (5 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb-prime (enc ra-prime k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k)))))
(label 172)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (3 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((1 1) (5 2)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 0)) ((3 3) (1 2)) ((4 1) (3 2))
((5 1) (1 0)) ((5 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 1 resp-reauth 2)
(enc ra-prime-1 k) (5 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb (enc ra-prime k))) (send (enc rb k))))
(label 173)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (5 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 0)) ((3 3) (1 2)) ((4 1) (3 2))
((4 1) (5 2)) ((5 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 4 resp-reauth 2)
(enc ra-prime-1 k) (5 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
(label 176)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 1)) ((3 3) (1 2)) ((4 1) (3 2))
((5 0) (0 0)) ((5 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 2 keyserver 2)
(enc b ra-0 k tb (ltk a ks)) (5 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k))))
((send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 179)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (5 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 1)) ((2 1) (1 0)) ((2 1) (4 0))
((2 1) (5 0)) ((3 0) (0 0)) ((3 2) (1 2)) ((4 3) (0 2))
((5 1) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (5 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k)))))
(label 182)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (3 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 rb-prime-0 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 0)) ((1 1) (5 2)) ((2 1) (4 0))
((2 1) (5 0)) ((3 1) (1 2)) ((4 3) (0 2)) ((5 1) (1 0))
((5 3) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 1 resp-reauth 2)
(enc ra-prime-1 k) (5 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k))))
(label 185)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (5 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 rb-prime-0 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 0)) ((2 1) (1 0)) ((2 1) (4 0))
((2 1) (5 1)) ((3 1) (1 2)) ((4 3) (0 2)) ((5 0) (0 0))
((5 2) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 2 keyserver 2)
(enc b ra-0 k tb (ltk a ks)) (5 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k)))))
(label 188)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (5 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra ra-prime rb-prime tb ra-0 rb rb-0 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (4 2)) ((2 1) (1 0))
((2 1) (4 0)) ((2 1) (5 1)) ((3 1) (2 0)) ((4 3) (1 2))
((5 2) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 6 1 resp-reauth 2) (enc rb-1 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra-0)) (send (cat b rb-0 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k)))))
(label 202)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 1)) ((1 1) (4 2)) ((2 1) (4 0)) ((2 1) (5 1))
((3 1) (2 0)) ((4 1) (1 0)) ((4 3) (1 2)) ((5 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 2 keyserver 2)
(enc b ra-1 k tb (ltk a ks)) (5 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb-prime (enc ra-prime k))) (send (enc rb-prime k)))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 209)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
rb-prime-1 text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-1)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (6 0)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
((5 1) (4 2)) ((6 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k))))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-1 (enc rb k)))))
(label 212)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 2)) ((1 1) (4 1)) ((1 1) (5 2)) ((2 1) (5 0))
((3 1) (2 0)) ((4 2) (1 2)) ((5 1) (1 0)) ((5 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 1 resp-reauth 2)
(enc ra-prime-0 k) (5 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb (enc ra-prime k))) (send (enc rb k))))
(label 215)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (5 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 1)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 1))
((3 1) (2 0)) ((4 2) (1 2)) ((5 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 2 keyserver 2)
(enc b ra-1 k tb (ltk a ks)) (5 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 218)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-prime-0
rb-prime-1 text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 2)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
((2 1) (6 0)) ((3 1) (2 0)) ((4 1) (1 2)) ((5 3) (0 2))
((6 1) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-1 (enc ra-prime-0 k)))))
(label 221)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb ra-prime rb-prime rb ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-1) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (2 0)) ((1 1) (0 2)) ((1 1) (3 2)) ((2 1) (1 0))
((2 1) (3 0)) ((2 1) (4 0)) ((2 1) (5 1)) ((3 3) (1 2))
((4 3) (3 2)) ((5 0) (0 0)) ((5 2) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 6 1 resp-reauth 2) (enc rb-0 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-1))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-1 k)))))
(label 231)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (5 0)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (4 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 0)) ((3 3) (1 2)) ((4 1) (1 0)) ((4 3) (3 2))
((4 3) (5 2)) ((5 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 4 init-reauth 4)
(enc ra-prime-1 k) (5 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
(label 234)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (4 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 1)) ((3 3) (1 2)) ((4 1) (1 0)) ((4 3) (3 2))
((5 0) (0 0)) ((5 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 2 keyserver 2)
(enc b ra-0 k tb (ltk a ks)) (5 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k)))
((send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 239)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (5 0)) (rb (0 1)) (ra-prime (4 1))
(rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 rb-prime-0
rb-prime-1 text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-1)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2))
((4 3) (3 2)) ((5 1) (4 2)) ((6 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation 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 a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-0 (enc ra-prime-1 k))))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-1 (enc rb k)))))
(label 242)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 1)) ((2 1) (5 0)) ((3 3) (1 2)) ((4 0) (0 0))
((4 2) (3 2)) ((4 2) (5 2)) ((5 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 4 init 3) (enc ra-prime-1 k)
(5 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
(label 245)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (4 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((1 1) (5 2)) ((2 1) (3 0))
((2 1) (4 1)) ((2 1) (5 0)) ((3 3) (1 2)) ((4 0) (0 0))
((4 2) (3 2)) ((5 1) (1 0)) ((5 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 1 resp-reauth 2)
(enc ra-prime-1 k) (5 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb (enc ra-prime k))) (send (enc rb k))))
(label 246)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (4 0)) (rb (0 1)) (ra-prime (5 1))
(rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 1)) ((3 1) (1 0)) ((3 3) (1 2)) ((4 3) (0 2))
((5 0) (0 0)) ((5 2) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 2 keyserver 2)
(enc b ra-0 k tb (ltk a ks)) (5 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb-prime (enc ra-prime k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k)))))
(label 253)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (5 0)) (rb (0 1)) (ra-prime (3 1))
(rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 ra-prime-1
rb-prime-1 text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2))
((4 1) (3 2)) ((5 3) (0 2)) ((6 1) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-1 (enc ra-prime-1 k)))))
(label 256)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey) (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 1)) ((1 1) (5 2)) ((2 1) (4 0))
((2 1) (5 0)) ((3 0) (0 0)) ((3 2) (1 2)) ((4 3) (0 2))
((5 1) (1 0)) ((5 3) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 6 1 resp-reauth 2)
(enc ra-prime-1 k) (5 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k))))
(label 259)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (3 0)) (rb (0 1)) (ra-prime (5 1))
(rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 rb-prime-0 ra-prime-0 ra-prime-1
rb-prime-1 text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 0)) ((2 1) (1 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (1 2)) ((4 3) (0 2))
((5 3) (4 2)) ((6 1) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-1 (enc ra-prime-1 k)))))
(label 264)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-0)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (6 0)) ((1 1) (5 2)) ((2 1) (4 0)) ((2 1) (5 0))
((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 1) (1 0))
((5 3) (4 2)) ((6 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-0 (enc rb k)))))
(label 269)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (5 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra ra-prime rb-prime tb ra-0 rb rb-0 ra-prime-0 ra-prime-1
rb-prime-0 text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (4 2)) ((2 1) (1 0))
((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0))
((4 3) (1 2)) ((5 3) (4 2)) ((6 1) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2) (enc rb-1 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra-0)) (send (cat b rb-0 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-0 (enc ra-prime-1 k)))))
(label 272)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-0)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (6 0)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
((2 1) (5 1)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
((5 2) (4 2)) ((6 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-0 (enc rb k)))))
(label 277)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 2)) ((1 1) (4 2)) ((2 1) (4 0)) ((2 1) (5 0))
((2 1) (6 0)) ((3 1) (2 0)) ((4 1) (1 0)) ((4 3) (1 2))
((5 3) (0 2)) ((6 1) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb-prime (enc ra-prime k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k)))))
(label 280)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (6 2)) ((1 1) (4 2)) ((1 1) (6 2)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
((5 1) (4 2)) ((6 1) (1 0)) ((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2)
(enc ra-prime-1 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb (enc ra-prime k))) (send (enc rb k))))
(label 281)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (6 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (6 2)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
((5 1) (4 2)) ((5 1) (6 2)) ((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 5 resp-reauth 2)
(enc ra-prime-1 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
(label 284)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (6 1)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 1)) ((3 1) (2 0)) ((4 3) (1 2))
((5 1) (4 2)) ((6 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 2 keyserver 2)
(enc b ra-1 k tb (ltk a ks)) (6 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k))))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 287)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 2)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
((2 1) (6 0)) ((3 1) (2 0)) ((4 2) (1 2)) ((5 3) (0 2))
((6 1) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k)))))
(label 290)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 2)) ((1 1) (4 0)) ((1 1) (6 2)) ((2 1) (5 0))
((2 1) (6 0)) ((3 1) (2 0)) ((4 1) (1 2)) ((5 3) (0 2))
((6 1) (1 0)) ((6 3) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2)
(enc ra-prime-1 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k))))
(label 293)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (6 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 rb-prime-0 ra-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (5 2)) ((1 1) (4 0)) ((2 1) (1 0)) ((2 1) (5 0))
((2 1) (6 1)) ((3 1) (2 0)) ((4 1) (1 2)) ((5 3) (0 2))
((6 2) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 2 keyserver 2)
(enc b ra-1 k tb (ltk a ks)) (6 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k)))))
(label 296)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-0)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (5 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2)) ((4 3) (3 2))
((5 1) (1 0)) ((5 3) (4 2)) ((6 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-1 (enc ra-prime k)))
(send (enc ra-prime-1 k)))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-0 (enc rb k)))))
(label 305)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (5 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb ra-prime rb-prime rb ra-prime-0 ra-prime-1 ra-prime-2
rb-prime-0 text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-2)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-2)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (0 2)) ((1 1) (3 2)) ((2 1) (1 0))
((2 1) (3 0)) ((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 0))
((3 3) (1 2)) ((4 3) (3 2)) ((5 3) (4 2)) ((6 1) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2) (enc rb-0 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-2))
(recv (cat ra-prime-1 (enc ra-prime-2 k)))
(send (enc ra-prime-1 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-2))
(send (cat rb-prime-0 (enc ra-prime-2 k)))))
(label 308)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-1) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb) (rb-prime rb-prime-0)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 1)) ((2 1) (6 0)) ((3 3) (1 2))
((4 3) (3 2)) ((5 0) (0 0)) ((5 2) (4 2)) ((6 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-1))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-1 k))))
((recv (cat (enc a k tb (ltk b ks)) rb))
(send (cat rb-prime-0 (enc rb k)))))
(label 313)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (5 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (4 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2)) ((4 1) (1 0))
((4 3) (3 2)) ((5 3) (0 2)) ((6 1) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-0 (enc ra-prime-1 k)))))
(label 316)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2))
((4 3) (3 2)) ((4 3) (6 2)) ((5 1) (4 2)) ((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 4 init-reauth 4)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-0 (enc ra-prime-1 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
(label 318)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2))
((4 3) (3 2)) ((5 1) (4 2)) ((5 1) (6 2)) ((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 5 resp-reauth 2)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-0 (enc ra-prime-1 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k))))
(label 320)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((1 1) (6 2)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2))
((4 3) (3 2)) ((5 1) (4 2)) ((6 1) (1 0)) ((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-0 (enc ra-prime-1 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb (enc ra-prime k))) (send (enc rb k))))
(label 321)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (6 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 1)) ((3 3) (1 2))
((4 3) (3 2)) ((5 1) (4 2)) ((6 0) (0 0)) ((6 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 2 keyserver 2)
(enc b ra-0 k tb (ltk a ks)) (6 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-0 (enc ra-prime-1 k))))
((send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 324)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (6 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 1)) ((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2))
((4 0) (0 0)) ((4 2) (3 2)) ((5 3) (0 2)) ((6 1) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-0 (enc ra-prime-1 k)))))
(label 327)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (4 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (1 0)) ((3 3) (1 2))
((4 3) (0 2)) ((5 3) (4 2)) ((6 1) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb-prime (enc ra-prime k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-0 (enc ra-prime-1 k)))))
(label 330)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (3 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 ra-prime-1
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((1 1) (6 2)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2))
((4 1) (3 2)) ((5 3) (0 2)) ((6 1) (1 0)) ((6 3) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-1 (enc ra-prime k)))
(send (enc ra-prime-1 k))))
(label 331)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (6 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 ra-prime-1
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2))
((4 1) (3 2)) ((4 1) (6 2)) ((5 3) (0 2)) ((6 3) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 4 resp-reauth 2)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat ra-prime-1 (enc ra-prime-0 k)))
(send (enc ra-prime-1 k))))
(label 334)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 ra-prime-1
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-1) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 1)) ((3 3) (1 2))
((4 1) (3 2)) ((5 3) (0 2)) ((6 0) (0 0)) ((6 2) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 2 keyserver 2)
(enc b ra-0 k tb (ltk a ks)) (6 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-1))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-1 k)))))
(label 337)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (6 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 rb-prime-0
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime ra-prime-1)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 1)) ((2 1) (1 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 0) (0 0)) ((3 2) (1 2))
((4 3) (0 2)) ((5 3) (4 2)) ((6 1) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-0 (enc ra-prime-1 k)))))
(label 340)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (3 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 rb-prime-0 ra-prime-0 ra-prime-1
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 0)) ((1 1) (6 2)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 1) (1 2)) ((4 3) (0 2))
((5 3) (4 2)) ((6 1) (1 0)) ((6 3) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-1 (enc ra-prime k)))
(send (enc ra-prime-1 k))))
(label 343)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (6 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 rb-prime-0 ra-prime-0 ra-prime-1
text) (a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 2 (k k) (ra-prime rb-prime)
(rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-1) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 0)) ((2 1) (1 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 1)) ((3 1) (1 2)) ((4 3) (0 2))
((5 3) (4 2)) ((6 0) (0 0)) ((6 2) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 2 keyserver 2)
(enc b ra-0 k tb (ltk a ks)) (6 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-1))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-1 k)))))
(label 346)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (6 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra ra-prime rb-prime tb ra-0 rb rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb ra-prime-1) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (1 0)) ((1 1) (0 2)) ((1 1) (4 2)) ((2 1) (1 0))
((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 1)) ((3 1) (2 0))
((4 3) (1 2)) ((5 3) (4 2)) ((6 2) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2) (enc rb-1 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra-0)) (send (cat b rb-0 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-1))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-1 k)))))
(label 353)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (6 2)) ((1 1) (5 2)) ((2 1) (4 0)) ((2 1) (5 0))
((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 1) (1 0))
((5 3) (4 2)) ((5 3) (6 2)) ((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 5 init-reauth 4)
(enc ra-prime-1 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
(label 356)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (5 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (6 1)) ((1 1) (5 2)) ((2 1) (4 0)) ((2 1) (5 0))
((2 1) (6 1)) ((3 1) (2 0)) ((4 3) (1 2)) ((5 1) (1 0))
((5 3) (4 2)) ((6 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 2 keyserver 2)
(enc b ra-1 k tb (ltk a ks)) (6 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k)))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 361)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (5 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (6 2)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
((2 1) (5 1)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
((5 2) (4 2)) ((5 2) (6 2)) ((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 5 init 3) (enc ra-prime-1 k)
(6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
(label 364)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (6 2)) ((1 1) (4 2)) ((1 1) (6 2)) ((2 1) (4 0))
((2 1) (5 1)) ((2 1) (6 0)) ((3 1) (2 0)) ((4 3) (1 2))
((5 2) (4 2)) ((6 1) (1 0)) ((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2)
(enc ra-prime-1 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb (enc ra-prime k))) (send (enc rb k))))
(label 365)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (6 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (6 1)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
((2 1) (5 1)) ((2 1) (6 1)) ((3 1) (2 0)) ((4 3) (1 2))
((5 2) (4 2)) ((6 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 2 keyserver 2)
(enc b ra-1 k tb (ltk a ks)) (6 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 368)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (5 2)) ((1 1) (4 2)) ((2 1) (4 0)) ((2 1) (5 0))
((2 1) (6 1)) ((3 1) (2 0)) ((4 1) (1 0)) ((4 3) (1 2))
((5 3) (0 2)) ((6 2) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 2 keyserver 2)
(enc b ra-1 k tb (ltk a ks)) (6 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb-prime (enc ra-prime k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k)))))
(label 373)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (5 2)) ((1 1) (4 1)) ((1 1) (6 2)) ((2 1) (5 0))
((2 1) (6 0)) ((3 1) (2 0)) ((4 2) (1 2)) ((5 3) (0 2))
((6 1) (1 0)) ((6 3) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2)
(enc ra-prime-1 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k))))
(label 376)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (6 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra-0) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (5 2)) ((1 1) (4 1)) ((2 1) (1 0)) ((2 1) (5 0))
((2 1) (6 1)) ((3 1) (2 0)) ((4 2) (1 2)) ((5 3) (0 2))
((6 2) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 2 keyserver 2)
(enc b ra-1 k tb (ltk a ks)) (6 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((send (cat a ra-0))
(recv
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k)))))
(label 379)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb ra-prime rb-prime rb ra-prime-0 ra-prime-1 ra-prime-2 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb ra-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-2)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-2) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (2 0)) ((1 1) (0 2)) ((1 1) (3 2)) ((2 1) (1 0))
((2 1) (3 0)) ((2 1) (4 0)) ((2 1) (5 0)) ((2 1) (6 1))
((3 3) (1 2)) ((4 3) (3 2)) ((5 3) (4 2)) ((6 0) (0 0))
((6 2) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2) (enc rb-0 k)
(0 2))
(traces
((recv (cat a ra)) (send (cat b ra-prime (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc ra-prime k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-2))
(recv (cat ra-prime-1 (enc ra-prime-2 k)))
(send (enc ra-prime-1 k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-2))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-2 k)))))
(label 386)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (6 0)) (ra-prime (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (5 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2)) ((4 3) (3 2))
((5 1) (1 0)) ((5 3) (4 2)) ((5 3) (6 2)) ((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 5 init-reauth 4)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-1 (enc ra-prime k)))
(send (enc ra-prime-1 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k))))
(label 389)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (5 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (5 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2)) ((4 3) (3 2))
((4 3) (6 2)) ((5 1) (1 0)) ((5 3) (4 2)) ((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 4 init-reauth 4)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-1 (enc ra-prime k)))
(send (enc ra-prime-1 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
(label 390)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (5 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (5 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 1)) ((3 3) (1 2)) ((4 3) (3 2))
((5 1) (1 0)) ((5 3) (4 2)) ((6 0) (0 0)) ((6 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 2 keyserver 2)
(enc b ra-0 k tb (ltk a ks)) (6 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-1 (enc ra-prime k)))
(send (enc ra-prime-1 k)))
((send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
(send (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 395)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (6 0)) (rb (0 1)) (ra-prime (5 1))
(rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-1) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 1)) ((2 1) (6 0)) ((3 3) (1 2))
((4 3) (3 2)) ((4 3) (6 2)) ((5 0) (0 0)) ((5 2) (4 2))
((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 4 init-reauth 4)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-1))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-1 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k))))
(label 396)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (5 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-1) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 1)) ((2 1) (6 0)) ((3 3) (1 2))
((4 3) (3 2)) ((5 0) (0 0)) ((5 2) (4 2)) ((5 2) (6 2))
((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 5 init 3) (enc ra-prime-2 k)
(6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-1))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-1 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k))))
(label 398)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (5 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-1) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((1 1) (6 2)) ((2 1) (3 0))
((2 1) (4 0)) ((2 1) (5 1)) ((2 1) (6 0)) ((3 3) (1 2))
((4 3) (3 2)) ((5 0) (0 0)) ((5 2) (4 2)) ((6 1) (1 0))
((6 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-1))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-1 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb (enc ra-prime k))) (send (enc rb k))))
(label 399)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (5 0)) (rb (0 1)) (ra-prime (6 1))
(rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-1) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (2 0)) ((1 1) (4 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 1)) ((3 3) (1 2)) ((4 1) (1 0))
((4 3) (3 2)) ((5 3) (0 2)) ((6 0) (0 0)) ((6 2) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 2 keyserver 2)
(enc b ra-0 k tb (ltk a ks)) (6 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-1))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-1 k)))))
(label 403)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (6 0)) (rb (0 1)) (ra-prime (4 1))
(rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (4 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2)) ((4 1) (1 0))
((4 3) (3 2)) ((4 3) (6 2)) ((5 3) (0 2)) ((6 3) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 4 init-reauth 4)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat ra-prime-1 (enc ra-prime-0 k)))
(send (enc ra-prime-1 k))))
(label 404)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
((2 1) (4 1)) ((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2))
((4 0) (0 0)) ((4 2) (3 2)) ((4 2) (6 2)) ((5 3) (0 2))
((6 3) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 4 init 3) (enc ra-prime-2 k)
(6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat ra-prime-1 (enc ra-prime-0 k)))
(send (enc ra-prime-1 k))))
(label 411)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (4 0)) (rb (0 1)) (rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((1 1) (6 2)) ((2 1) (3 0))
((2 1) (4 1)) ((2 1) (5 0)) ((2 1) (6 0)) ((3 3) (1 2))
((4 0) (0 0)) ((4 2) (3 2)) ((5 3) (0 2)) ((6 1) (1 0))
((6 3) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-0))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-0 k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat rb (enc ra-prime-1 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-1 (enc ra-prime k)))
(send (enc ra-prime-1 k))))
(label 412)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (4 0)) (rb (0 1)) (ra-prime (6 1))
(rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (k k) (ra ra) (rb ra-prime-1) (tb tb) (a a) (b b)
(ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (3 0)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 1)) ((3 1) (1 0)) ((3 3) (1 2))
((4 3) (0 2)) ((5 3) (4 2)) ((6 0) (0 0)) ((6 2) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 2 keyserver 2)
(enc b ra-0 k tb (ltk a ks)) (6 1))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat rb-prime (enc ra-prime k))) (send (enc rb-prime k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
ra-prime-1))
(send (cat (enc a k tb (ltk b ks)) (enc ra-prime-1 k)))))
(label 419)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (6 0)) (rb (0 1)) (ra-prime (3 1))
(rb-prime (1 1))))
(defskeleton neuman-stubblebine-reauth
(vars (k skey)
(ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name))
(defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb) (a a) (b b) (ks ks))
(defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
(ks ks))
(defstrand init 3 (k k) (ra ra) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-0) (rb-prime rb)
(tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (k k) (ra-prime ra-prime)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 1) (2 0)) ((1 1) (3 1)) ((1 1) (6 2)) ((2 1) (4 0))
((2 1) (5 0)) ((2 1) (6 0)) ((3 0) (0 0)) ((3 2) (1 2))
((4 3) (0 2)) ((5 3) (4 2)) ((6 1) (1 0)) ((6 3) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig k ra rb ra-prime rb-prime)
(operation encryption-test (displaced 7 1 resp-reauth 2)
(enc ra-prime-2 k) (6 2))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((send (cat a ra))
(recv
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-prime))
(send (cat (enc a k tb (ltk b ks)) (enc rb-prime k))))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-0))
(recv (cat rb (enc ra-prime-0 k))) (send (enc rb k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (enc a k tb (ltk b ks)))
(send (cat (enc a k tb (ltk b ks)) ra-prime))
(recv (cat ra-prime-1 (enc ra-prime k)))
(send (enc ra-prime-1 k))))
(label 422)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
(ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
(origs (k (2 1)) (ra (3 0)) (rb (0 1)) (ra-prime (6 1))
(rb-prime (1 1))))
(comment "Strand bound exceeded--aborting run")