cpsa-4.4.4: tst/jdg-neuman-stubblebine-reauth_shapes.tst
(comment "CPSA 4.3.1")
(comment "Extracted shapes")
(herald jdg-neuman-stubblebine-reauth (bound 8))
(comment "CPSA 4.3.0")
(comment "All input read from tst/jdg-neuman-stubblebine-reauth.lsp")
(defprotocol neuman-stubblebine basic
(defrole init
(vars (a b ks name) (ra rb text) (k skey) (tb text) (tkt mesg))
(trace (send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k)))))
(defrole resp
(vars (a b ks name) (ra rb text) (k skey) (tb text))
(trace (recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(defrole keyserver
(vars (a b ks name) (ra rb text) (k skey) (tb text))
(trace (recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
(uniq-orig k))
(defrule cakeRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
(leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2))
(false))))
(defrule no-interruption
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (leads-to z0 i0 z2 i2) (trans z1 i1)
(same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
(false))))
(defrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defrule scissorsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
(and (= z1 z2) (= i1 i2)))))
(defrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))))
(defskeleton neuman-stubblebine
(vars (ra tb rb text) (a b ks name) (k skey))
(defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra rb k)
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 0)
(unrealized (0 2))
(origs (rb (0 1)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton neuman-stubblebine
(vars (tkt mesg) (ra tb rb rb-0 text) (a b ks name) (k skey))
(defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand init 3 (tkt tkt) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks) (k k))
(precedes ((0 1) (1 0)) ((1 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra rb k)
(operation nonce-test
(contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-0 ra) (tb-0 tb)) k (2 1)
(enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((send (cat a ra)) (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k)))))
(label 8)
(parent 0)
(realized)
(shape)
(maps ((0) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k))))
(origs (k (1 1)) (ra (2 0)) (rb (0 1))))
(defskeleton neuman-stubblebine
(vars (tkt mesg) (ra tb rb ra-0 rb-0 rb-1 text) (a b ks name)
(k skey))
(defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (tkt tkt) (ra ra-0) (rb rb) (tb tb) (a a) (b b)
(ks ks) (k k))
(precedes ((0 1) (3 1)) ((1 1) (3 1)) ((2 1) (1 0)) ((3 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra rb k)
(operation nonce-test
(contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-1 ra-0) (tb-0 tb)) k (3 1)
(enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((send (cat a ra-0))
(recv (cat (enc b ra-0 k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k)))))
(label 9)
(parent 0)
(realized)
(shape)
(maps ((0) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k))))
(origs (k (1 1)) (rb (0 1))))
(comment "Nothing left to do")
(defprotocol neuman-stubblebine basic
(defrole init
(vars (a b ks name) (ra rb text) (k skey) (tb text) (tkt mesg))
(trace (send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k)))))
(defrole resp
(vars (a b ks name) (ra rb text) (k skey) (tb text))
(trace (recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(defrole keyserver
(vars (a b ks name) (ra rb text) (k skey) (tb text))
(trace (recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
(uniq-orig k))
(defrule cakeRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
(leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2))
(false))))
(defrule no-interruption
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (leads-to z0 i0 z2 i2) (trans z1 i1)
(same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
(false))))
(defrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defrule scissorsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
(and (= z1 z2) (= i1 i2)))))
(defrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))))
(defskeleton neuman-stubblebine
(vars (tkt mesg) (ra tb rb text) (a b ks name) (k skey))
(defstrand init 3 (tkt tkt) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks) (k k))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra rb k)
(traces
((send (cat a ra)) (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k)))))
(label 10)
(unrealized (0 1))
(origs (ra (0 0)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton neuman-stubblebine
(vars (tkt mesg) (ra tb rb rb-0 rb-1 text) (a b ks name) (k skey))
(defstrand init 3 (tkt tkt) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra rb k)
(operation encryption-test (added-strand resp 2)
(enc a ra tb (ltk b ks)) (1 0))
(traces
((send (cat a ra)) (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k))))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (cat a ra)) (send (cat b rb-1 (enc a ra tb (ltk b ks))))))
(label 12)
(parent 10)
(realized)
(shape)
(maps
((0) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (tkt tkt))))
(origs (k (1 1)) (ra (0 0))))
(comment "Nothing left to do")
(defprotocol neuman-stubblebine basic
(defrole init
(vars (a b ks name) (ra rb text) (k skey) (tb text) (tkt mesg))
(trace (send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k)))))
(defrole resp
(vars (a b ks name) (ra rb text) (k skey) (tb text))
(trace (recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(defrole keyserver
(vars (a b ks name) (ra rb text) (k skey) (tb text))
(trace (recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
(uniq-orig k))
(defrule cakeRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
(leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2))
(false))))
(defrule no-interruption
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (leads-to z0 i0 z2 i2) (trans z1 i1)
(same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
(false))))
(defrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defrule scissorsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
(and (= z1 z2) (= i1 i2)))))
(defrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))))
(defskeleton neuman-stubblebine
(vars (ra tb rb text) (a b ks name) (k skey))
(defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra rb k)
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(label 13)
(unrealized (0 2))
(origs (rb (0 1)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton neuman-stubblebine
(vars (tkt mesg) (ra tb rb rb-0 text) (a b ks name) (k skey))
(defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand init 3 (tkt tkt) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks) (k k))
(precedes ((0 1) (1 0)) ((1 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra rb k)
(operation nonce-test
(contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-0 ra) (tb-0 tb)) k (2 1)
(enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((send (cat a ra)) (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k)))))
(label 21)
(parent 13)
(realized)
(shape)
(maps ((0) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k))))
(origs (k (1 1)) (ra (2 0)) (rb (0 1))))
(defskeleton neuman-stubblebine
(vars (tkt mesg) (ra tb rb ra-0 rb-0 rb-1 text) (a b ks name)
(k skey))
(defstrand resp 3 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra-0) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (tkt tkt) (ra ra-0) (rb rb) (tb tb) (a a) (b b)
(ks ks) (k k))
(precedes ((0 1) (3 1)) ((1 1) (3 1)) ((2 1) (1 0)) ((3 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra rb k)
(operation nonce-test
(contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-1 ra-0) (tb-0 tb)) k (3 1)
(enc a k tb (ltk b ks)) (enc b ra-0 k tb (ltk a ks)))
(traces
((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k))))
((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
(send
(cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
rb-0)))
((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
((send (cat a ra-0))
(recv (cat (enc b ra-0 k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k)))))
(label 22)
(parent 13)
(realized)
(shape)
(maps ((0) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k))))
(origs (k (1 1)) (rb (0 1))))
(comment "Nothing left to do")
(defprotocol neuman-stubblebine basic
(defrole init
(vars (a b ks name) (ra rb text) (k skey) (tb text) (tkt mesg))
(trace (send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k)))))
(defrole resp
(vars (a b ks name) (ra rb text) (k skey) (tb text))
(trace (recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(defrole keyserver
(vars (a b ks name) (ra rb text) (k skey) (tb text))
(trace (recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
(uniq-orig k))
(defrule cakeRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
(leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2))
(false))))
(defrule no-interruption
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (leads-to z0 i0 z2 i2) (trans z1 i1)
(same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
(false))))
(defrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defrule scissorsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
(and (= z1 z2) (= i1 i2)))))
(defrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))))
(defskeleton neuman-stubblebine
(vars (tkt mesg) (ra tb rb text) (a b ks name) (k skey))
(defstrand init 3 (tkt tkt) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks) (k k))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra rb k)
(traces
((send (cat a ra)) (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k)))))
(label 23)
(unrealized (0 1))
(origs (ra (0 0)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton neuman-stubblebine
(vars (tkt mesg) (ra tb rb rb-0 rb-1 text) (a b ks name) (k skey))
(defstrand init 3 (tkt tkt) (ra ra) (rb rb) (tb tb) (a a) (b b)
(ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
(precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra rb k)
(operation encryption-test (added-strand resp 2)
(enc a ra tb (ltk b ks)) (1 0))
(traces
((send (cat a ra)) (recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k))))
((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
((recv (cat a ra)) (send (cat b rb-1 (enc a ra tb (ltk b ks))))))
(label 25)
(parent 23)
(realized)
(shape)
(maps
((0) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (tkt tkt))))
(origs (k (1 1)) (ra (0 0))))
(comment "Nothing left to do")
(defprotocol neuman-stubblebine-reauth basic
(defrole init
(vars (a b ks name) (ra rb tb text) (k skey) (tkt mesg))
(trace (send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) tkt rb))
(send (cat tkt (enc rb k)))))
(defrole resp
(vars (a b ks name) (ra rb tb text) (k skey))
(trace (recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
(recv (cat (enc a k tb (ltk b ks)) (enc rb k)))))
(defrole init-reauth
(vars (a b ks name) (ra ra-prime rb-prime text) (k skey) (tb text)
(tkt mesg))
(trace (recv (cat (enc b ra k tb (ltk a ks)) tkt))
(send (cat tkt ra-prime)) (recv (cat rb-prime (enc ra-prime k)))
(send (enc rb-prime k))))
(defrole resp-reauth
(vars (a b ks name) (tb ra-prime rb-prime text) (k skey))
(trace (recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k))))
(defrole keyserver
(vars (a b ks name) (ra rb text) (k skey) (tb text))
(trace (recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
(uniq-orig k))
(defrule cakeRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (leads-to z0 i0 z1 i1)
(leads-to z0 i0 z2 i2) (prec z1 i1 z2 i2))
(false))))
(defrule no-interruption
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (leads-to z0 i0 z2 i2) (trans z1 i1)
(same-locn z0 i0 z1 i1) (prec z0 i0 z1 i1) (prec z1 i1 z2 i2))
(false))))
(defrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defrule scissorsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (leads-to z0 i0 z2 i2))
(and (= z1 z2) (= i1 i2)))))
(defrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1))))))
(defskeleton neuman-stubblebine-reauth
(vars (ra-prime rb-prime tb text) (a b ks name) (k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k))))
(label 26)
(unrealized (0 0))
(origs (rb-prime (0 1)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton neuman-stubblebine-reauth
(vars (tkt mesg) (ra-prime rb-prime tb ra rb rb-0 text) (a b ks name)
(k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init 3 (tkt tkt) (ra ra) (rb rb-prime) (tb tb) (a a) (b b)
(ks ks) (k k))
(precedes ((0 1) (3 1)) ((1 1) (0 0)) ((2 1) (1 0)) ((3 2) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(operation nonce-test
(contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-0 ra) (tb-0 tb)) k (3 1)
(enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
((send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) tkt rb-prime))
(send (cat tkt (enc rb-prime k)))))
(label 34)
(parent 26)
(realized)
(shape)
(maps
((0)
((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb))))
(origs (k (1 1)) (rb-prime (0 1))))
(defskeleton neuman-stubblebine-reauth
(vars (ra-prime rb-prime tb ra rb rb-0 rb-prime-0 text) (a b ks name)
(k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand resp-reauth 2 (tb tb) (ra-prime rb-prime)
(rb-prime rb-prime-0) (a a) (b b) (ks ks) (k k))
(precedes ((0 1) (3 0)) ((1 1) (0 0)) ((2 1) (1 0)) ((3 1) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (3 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
((recv (cat (enc a k tb (ltk b ks)) rb-prime))
(send (cat rb-prime-0 (enc rb-prime k)))))
(label 35)
(parent 26)
(realized)
(shape)
(maps
((0)
((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb))))
(origs (k (1 1)) (rb-prime (0 1))))
(defskeleton neuman-stubblebine-reauth
(vars (tkt mesg) (ra-prime rb-prime tb ra rb rb-0 text) (a b ks name)
(k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
(precedes ((0 1) (3 2)) ((1 1) (3 0)) ((2 1) (1 0)) ((3 1) (0 0))
((3 3) (0 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(operation encryption-test (displaced 4 0 resp-reauth 2)
(enc ra-prime-0 k) (3 2))
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
((recv (cat (enc b ra k tb (ltk a ks)) tkt))
(send (cat tkt ra-prime)) (recv (cat rb-prime (enc ra-prime k)))
(send (enc rb-prime k))))
(label 38)
(parent 26)
(realized)
(shape)
(maps
((0)
((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb))))
(origs (k (1 1)) (ra-prime (3 1)) (rb-prime (0 1))))
(defskeleton neuman-stubblebine-reauth
(vars (tkt tkt-0 mesg)
(ra-prime rb-prime tb ra rb rb-0 ra-prime-0 text) (a b ks name)
(k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init 3 (tkt tkt-0) (ra ra) (rb ra-prime-0) (tb tb) (a a)
(b b) (ks ks) (k k))
(precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 1))
((2 1) (1 0)) ((3 3) (0 2)) ((4 2) (3 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(operation nonce-test
(contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-0 ra) (tb-0 tb)) k (4 1)
(enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
((recv (cat (enc b ra k tb (ltk a ks)) tkt))
(send (cat tkt ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) tkt-0 ra-prime-0))
(send (cat tkt-0 (enc ra-prime-0 k)))))
(label 42)
(parent 26)
(realized)
(shape)
(maps
((0)
((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb))))
(origs (k (1 1)) (rb-prime (0 1))))
(defskeleton neuman-stubblebine-reauth
(vars (tkt mesg)
(ra-prime rb-prime tb ra rb rb-0 ra-prime-0 rb-prime-0 text)
(a b ks name) (k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand resp-reauth 2 (tb tb) (ra-prime ra-prime-0)
(rb-prime rb-prime-0) (a a) (b b) (ks ks) (k k))
(precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
((2 1) (1 0)) ((3 3) (0 2)) ((4 1) (3 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (4 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
((recv (cat (enc b ra k tb (ltk a ks)) tkt))
(send (cat tkt ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
(send (cat rb-prime-0 (enc ra-prime-0 k)))))
(label 43)
(parent 26)
(realized)
(shape)
(maps
((0)
((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb))))
(origs (k (1 1)) (rb-prime (0 1))))
(defskeleton neuman-stubblebine-reauth
(vars (tkt tkt-0 mesg)
(ra-prime rb-prime tb ra rb rb-0 ra-prime-0 text) (a b ks name)
(k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
(precedes ((0 1) (4 2)) ((1 1) (3 0)) ((1 1) (4 0)) ((2 1) (1 0))
((3 3) (0 2)) ((4 1) (0 0)) ((4 3) (3 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(operation encryption-test (displaced 5 0 resp-reauth 2)
(enc ra-prime-1 k) (4 2))
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
((recv (cat (enc b ra k tb (ltk a ks)) tkt))
(send (cat tkt ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
(send (cat tkt-0 ra-prime))
(recv (cat ra-prime-0 (enc ra-prime k)))
(send (enc ra-prime-0 k))))
(label 46)
(parent 26)
(realized)
(shape)
(maps
((0)
((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb))))
(origs (k (1 1)) (ra-prime (4 1)) (rb-prime (0 1))))
(defskeleton neuman-stubblebine-reauth
(vars (tkt tkt-0 tkt-1 mesg)
(ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name) (k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init 3 (tkt tkt-1) (ra ra) (rb ra-prime-1) (tb tb) (a a)
(b b) (ks ks) (k k))
(precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
((1 1) (5 1)) ((2 1) (1 0)) ((3 3) (0 2)) ((4 3) (3 2))
((5 2) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(operation nonce-test
(contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-0 ra) (tb-0 tb)) k (5 1)
(enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
((recv (cat (enc b ra k tb (ltk a ks)) tkt))
(send (cat tkt ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
(send (cat tkt-0 ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) tkt-1 ra-prime-1))
(send (cat tkt-1 (enc ra-prime-1 k)))))
(label 50)
(parent 26)
(realized)
(shape)
(maps
((0)
((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb))))
(origs (k (1 1)) (rb-prime (0 1))))
(defskeleton neuman-stubblebine-reauth
(vars (tkt tkt-0 mesg)
(ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 rb-prime-0
text) (a b ks name) (k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand resp-reauth 2 (tb tb) (ra-prime ra-prime-1)
(rb-prime rb-prime-0) (a a) (b b) (ks ks) (k k))
(precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
((1 1) (5 0)) ((2 1) (1 0)) ((3 3) (0 2)) ((4 3) (3 2))
((5 1) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (5 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
((recv (cat (enc b ra k tb (ltk a ks)) tkt))
(send (cat tkt ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
(send (cat tkt-0 ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-1))
(send (cat rb-prime-0 (enc ra-prime-1 k)))))
(label 51)
(parent 26)
(realized)
(shape)
(maps
((0)
((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb))))
(origs (k (1 1)) (rb-prime (0 1))))
(defskeleton neuman-stubblebine-reauth
(vars (tkt tkt-0 tkt-1 mesg)
(ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 text)
(a b ks name) (k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init-reauth 4 (tkt tkt-1) (ra ra) (ra-prime ra-prime)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks) (k k))
(precedes ((0 1) (5 2)) ((1 1) (3 0)) ((1 1) (4 0)) ((1 1) (5 0))
((2 1) (1 0)) ((3 3) (0 2)) ((4 3) (3 2)) ((5 1) (0 0))
((5 3) (4 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(operation encryption-test (displaced 6 0 resp-reauth 2)
(enc ra-prime-2 k) (5 2))
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
((recv (cat (enc b ra k tb (ltk a ks)) tkt))
(send (cat tkt ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
(send (cat tkt-0 ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc b ra k tb (ltk a ks)) tkt-1))
(send (cat tkt-1 ra-prime))
(recv (cat ra-prime-1 (enc ra-prime k)))
(send (enc ra-prime-1 k))))
(label 54)
(parent 26)
(realized)
(shape)
(maps
((0)
((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb))))
(origs (k (1 1)) (ra-prime (5 1)) (rb-prime (0 1))))
(defskeleton neuman-stubblebine-reauth
(vars (tkt tkt-0 tkt-1 tkt-2 mesg)
(ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 ra-prime-2
text) (a b ks name) (k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init-reauth 4 (tkt tkt-1) (ra ra) (ra-prime ra-prime-2)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init 3 (tkt tkt-2) (ra ra) (rb ra-prime-2) (tb tb) (a a)
(b b) (ks ks) (k k))
(precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
((1 1) (5 0)) ((1 1) (6 1)) ((2 1) (1 0)) ((3 3) (0 2))
((4 3) (3 2)) ((5 3) (4 2)) ((6 2) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(operation nonce-test
(contracted (a-0 a) (b-0 b) (ks-0 ks) (ra-0 ra) (tb-0 tb)) k (6 1)
(enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
((recv (cat (enc b ra k tb (ltk a ks)) tkt))
(send (cat tkt ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
(send (cat tkt-0 ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc b ra k tb (ltk a ks)) tkt-1))
(send (cat tkt-1 ra-prime-2))
(recv (cat ra-prime-1 (enc ra-prime-2 k)))
(send (enc ra-prime-1 k)))
((send (cat a ra))
(recv (cat (enc b ra k tb (ltk a ks)) tkt-2 ra-prime-2))
(send (cat tkt-2 (enc ra-prime-2 k)))))
(label 58)
(parent 26)
(realized)
(shape)
(maps
((0)
((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb))))
(origs (k (1 1)) (rb-prime (0 1))))
(defskeleton neuman-stubblebine-reauth
(vars (tkt tkt-0 tkt-1 mesg)
(ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 ra-prime-2
rb-prime-0 text) (a b ks name) (k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init-reauth 4 (tkt tkt-1) (ra ra) (ra-prime ra-prime-2)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand resp-reauth 2 (tb tb) (ra-prime ra-prime-2)
(rb-prime rb-prime-0) (a a) (b b) (ks ks) (k k))
(precedes ((0 1) (3 2)) ((1 1) (0 0)) ((1 1) (3 0)) ((1 1) (4 0))
((1 1) (5 0)) ((1 1) (6 0)) ((2 1) (1 0)) ((3 3) (0 2))
((4 3) (3 2)) ((5 3) (4 2)) ((6 1) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(operation nonce-test (contracted (a-0 a) (b-0 b) (ks-0 ks) (tb-0 tb))
k (6 0) (enc a k tb (ltk b ks)) (enc b ra k tb (ltk a ks)))
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
((recv (cat (enc b ra k tb (ltk a ks)) tkt))
(send (cat tkt ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
(send (cat tkt-0 ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc b ra k tb (ltk a ks)) tkt-1))
(send (cat tkt-1 ra-prime-2))
(recv (cat ra-prime-1 (enc ra-prime-2 k)))
(send (enc ra-prime-1 k)))
((recv (cat (enc a k tb (ltk b ks)) ra-prime-2))
(send (cat rb-prime-0 (enc ra-prime-2 k)))))
(label 59)
(parent 26)
(realized)
(shape)
(maps
((0)
((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb))))
(origs (k (1 1)) (rb-prime (0 1))))
(defskeleton neuman-stubblebine-reauth
(vars (tkt tkt-0 tkt-1 tkt-2 mesg)
(ra-prime rb-prime tb ra rb rb-0 ra-prime-0 ra-prime-1 ra-prime-2
text) (a b ks name) (k skey))
(defstrand resp-reauth 3 (tb tb) (ra-prime ra-prime)
(rb-prime rb-prime) (a a) (b b) (ks ks) (k k))
(defstrand keyserver 2 (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks)
(k k))
(defstrand resp 2 (ra ra) (rb rb-0) (tb tb) (a a) (b b) (ks ks))
(defstrand init-reauth 4 (tkt tkt) (ra ra) (ra-prime ra-prime-0)
(rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init-reauth 4 (tkt tkt-0) (ra ra) (ra-prime ra-prime-1)
(rb-prime ra-prime-0) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init-reauth 4 (tkt tkt-1) (ra ra) (ra-prime ra-prime-2)
(rb-prime ra-prime-1) (tb tb) (a a) (b b) (ks ks) (k k))
(defstrand init-reauth 4 (tkt tkt-2) (ra ra) (ra-prime ra-prime)
(rb-prime ra-prime-2) (tb tb) (a a) (b b) (ks ks) (k k))
(precedes ((0 1) (6 2)) ((1 1) (3 0)) ((1 1) (4 0)) ((1 1) (5 0))
((1 1) (6 0)) ((2 1) (1 0)) ((3 3) (0 2)) ((4 3) (3 2))
((5 3) (4 2)) ((6 1) (0 0)) ((6 3) (5 2)))
(non-orig (ltk a ks) (ltk b ks))
(uniq-orig ra-prime rb-prime k)
(operation encryption-test (displaced 7 0 resp-reauth 2)
(enc ra-prime-3 k) (6 2))
(traces
((recv (cat (enc a k tb (ltk b ks)) ra-prime))
(send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))
((recv (cat b rb (enc a ra tb (ltk b ks))))
(send
(cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
((recv (cat a ra)) (send (cat b rb-0 (enc a ra tb (ltk b ks)))))
((recv (cat (enc b ra k tb (ltk a ks)) tkt))
(send (cat tkt ra-prime-0))
(recv (cat rb-prime (enc ra-prime-0 k))) (send (enc rb-prime k)))
((recv (cat (enc b ra k tb (ltk a ks)) tkt-0))
(send (cat tkt-0 ra-prime-1))
(recv (cat ra-prime-0 (enc ra-prime-1 k)))
(send (enc ra-prime-0 k)))
((recv (cat (enc b ra k tb (ltk a ks)) tkt-1))
(send (cat tkt-1 ra-prime-2))
(recv (cat ra-prime-1 (enc ra-prime-2 k)))
(send (enc ra-prime-1 k)))
((recv (cat (enc b ra k tb (ltk a ks)) tkt-2))
(send (cat tkt-2 ra-prime))
(recv (cat ra-prime-2 (enc ra-prime k)))
(send (enc ra-prime-2 k))))
(label 62)
(parent 26)
(realized)
(shape)
(maps
((0)
((a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime)
(tb tb))))
(origs (k (1 1)) (ra-prime (6 1)) (rb-prime (0 1))))
(comment "Strand bound exceeded--aborting run")