cpsa-4.4.9: tst/devlocn.tst
(herald "Dev and Locn"
(comment
"This tests the feature that allows loads and stors to have any message in their location position."))
(comment "CPSA 4.4.9")
(comment "All input read from tst/devlocn.scm")
(defprotocol devlocn basic
(defrole init
(vars (d dev) (l1 l2 locn) (n1 n2 data) (k skey))
(trace (stor (cat d l1) n1) (stor (cat d l2) n2) (send (enc d l1 k))
(send (enc d l2 k)))
(uniq-orig n1 n2 d))
(defrole resp
(vars (d dev) (l locn) (m mesg) (k skey))
(trace (recv (enc d l k)) (load (cat d l) m) (send m))
(non-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))))
(defgenrule 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)))))
(defgenrule 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))))
(defgenrule 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))))
(defgenrule discreteAfter
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (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)))))
(defgenrule discreteBefore
(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)))))
(defgenrule trRl_init-at-1
(forall ((z strd))
(implies (p "init" z (idx 2)) (trans z (idx 1)))))
(defgenrule trRl_init-at-0
(forall ((z strd))
(implies (p "init" z (idx 1)) (trans z (idx 0)))))
(defgenrule eff-init-0
(forall ((i indx) (z1 z strd))
(implies (and (p "init" z (idx 1)) (prec z (idx 0) z1 i))
(or (= z z1)
(and (p "init" z (idx 2)) (prec z (idx 1) z1 i))))))
(defgenrule eff-resp-2
(forall ((i indx) (z1 z strd))
(implies (and (p "resp" z (idx 3)) (prec z (idx 2) z1 i))
(or (= z z1)
(and (p "resp" z (idx 2)) (prec z (idx 1) z1 i)))))))
(defskeleton devlocn
(vars (n1 n2 data) (d dev) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 2 (n1 n1) (n2 n2) (d d) (l1 l1) (l2 l2))
(deflistener n1)
(deflistener n2)
(uniq-orig n1 n2)
(traces
((stor (cat d l1) (cat pt n1)) (stor (cat d l2) (cat pt-0 n2)))
((recv n1) (send n1)) ((recv n2) (send n2)))
(label 0)
(unrealized (1 0) (2 0))
(preskeleton)
(maps ((0 1 2) ((n1 n1) (n2 n2) (d d) (l1 l1) (l2 l2))))
(origs (pt-0 (0 1)) (pt (0 0)) (n2 (0 1)) (n1 (0 0)))
(comment "Not a skeleton"))
(defskeleton devlocn
(vars (n1 n2 data) (d dev) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 2 (n1 n1) (n2 n2) (d d) (l1 l1) (l2 l2))
(deflistener n1)
(deflistener n2)
(precedes ((0 0) (1 0)) ((0 1) (2 0)))
(uniq-orig n1 n2)
(traces
((stor (cat d l1) (cat pt n1)) (stor (cat d l2) (cat pt-0 n2)))
((recv n1) (send n1)) ((recv n2) (send n2)))
(label 1)
(parent 0)
(unrealized (1 0) (2 0))
(maps ((0 1 2) ((n1 n1) (n2 n2) (d d) (l1 l1) (l2 l2))))
(origs (pt-0 (0 1)) (pt (0 0)) (n2 (0 1)) (n1 (0 0)))
(comment "Not closed under rules"))
(defskeleton devlocn
(vars (n1 n2 data) (d dev) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 2 (n1 n1) (n2 n2) (d d) (l1 l1) (l2 l2))
(deflistener n1)
(deflistener n2)
(precedes ((0 1) (1 0)) ((0 1) (2 0)))
(uniq-orig n1 n2)
(rule eff-init-0 trRl_init-at-0 trRl_init-at-1)
(traces
((stor (cat d l1) (cat pt n1)) (stor (cat d l2) (cat pt-0 n2)))
((recv n1) (send n1)) ((recv n2) (send n2)))
(label 2)
(parent 1)
(unrealized (1 0) (2 0))
(maps ((0 1 2) ((n1 n1) (n2 n2) (d d) (l1 l1) (l2 l2))))
(origs (n1 (0 0)) (n2 (0 1)) (pt (0 0)) (pt-0 (0 1)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n2 data) (d dev) (k skey) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 2 (n1 n1) (n2 n2) (d d) (l1 l1) (l2 l2))
(deflistener n1)
(deflistener n2)
(defstrand resp 3 (m n2) (d d) (k k) (l l2))
(precedes ((0 1) (1 0)) ((0 1) (3 1)) ((3 2) (2 0)))
(non-orig k)
(uniq-orig n1 n2)
(leads-to ((0 1) (3 1)))
(operation nonce-test (added-strand resp 3) n2 (2 0)
(ch-msg (cat d l2) (cat pt-0 n2)))
(strand-map 0 1 2)
(traces
((stor (cat d l1) (cat pt n1)) (stor (cat d l2) (cat pt-0 n2)))
((recv n1) (send n1)) ((recv n2) (send n2))
((recv (enc d l2 k)) (load (cat d l2) (cat pt-0 n2)) (send n2)))
(label 3)
(parent 2)
(unrealized (1 0) (3 0))
(maps ((0 1 2) ((n1 n1) (n2 n2) (d d) (l1 l1) (l2 l2))))
(comment "2 in cohort - 2 not yet seen"))
(defskeleton devlocn
(vars (n1 n2 data) (d dev) (k skey) (pt pt-0 pval) (l2 l1 locn))
(deflistener n1)
(deflistener n2)
(defstrand resp 3 (m n2) (d d) (k k) (l l2))
(defstrand init 4 (n1 n1) (n2 n2) (d d) (k k) (l1 l1) (l2 l2))
(precedes ((2 2) (1 0)) ((3 1) (0 0)) ((3 3) (2 0)))
(non-orig k)
(uniq-orig n1 n2 d)
(leads-to ((3 1) (2 1)))
(rule discreteBefore trRl_init-at-0 trRl_init-at-1)
(operation encryption-test (added-strand init 4) (enc d l2 k) (3 0))
(strand-map 1 2 3 0)
(traces ((recv n1) (send n1)) ((recv n2) (send n2))
((recv (enc d l2 k)) (load (cat d l2) (cat pt-0 n2)) (send n2))
((stor (cat d l1) (cat pt n1)) (stor (cat d l2) (cat pt-0 n2))
(send (enc d l1 k)) (send (enc d l2 k))))
(label 4)
(parent 3)
(unrealized (0 0))
(maps ((3 0 1) ((n1 n1) (n2 n2) (d d) (l1 l1) (l2 l2))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n2 data) (d dev) (k skey) (pt pt-0 pval) (l2 locn))
(deflistener n1)
(deflistener n2)
(defstrand resp 3 (m n2) (d d) (k k) (l l2))
(defstrand init 3 (n1 n1) (n2 n2) (d d) (k k) (l1 l2) (l2 l2))
(precedes ((2 2) (1 0)) ((3 1) (0 0)) ((3 2) (2 0)))
(non-orig k)
(uniq-orig n1 n2 d)
(leads-to ((3 1) (2 1)))
(operation encryption-test (displaced 0 4 init 3) (enc d l2-0 k)
(3 0))
(strand-map 3 0 1 2)
(traces ((recv n1) (send n1)) ((recv n2) (send n2))
((recv (enc d l2 k)) (load (cat d l2) (cat pt-0 n2)) (send n2))
((stor (cat d l2) (cat pt n1)) (stor (cat d l2) (cat pt-0 n2))
(send (enc d l2 k))))
(label 5)
(parent 3)
(unrealized (0 0))
(dead)
(maps ((3 0 1) ((n1 n1) (n2 n2) (d d) (l1 l2) (l2 l2))))
(comment "empty cohort"))
(defskeleton devlocn
(vars (n1 n2 data) (d dev) (k k-0 skey) (pt pt-0 pval) (l2 l1 locn))
(deflistener n1)
(deflistener n2)
(defstrand resp 3 (m n2) (d d) (k k) (l l2))
(defstrand init 4 (n1 n1) (n2 n2) (d d) (k k) (l1 l1) (l2 l2))
(defstrand resp 3 (m n1) (d d) (k k-0) (l l1))
(precedes ((2 2) (1 0)) ((3 2) (4 0)) ((3 3) (2 0)) ((4 2) (0 0)))
(non-orig k k-0)
(uniq-orig n1 n2 d)
(leads-to ((3 0) (4 1)) ((3 1) (2 1)))
(operation nonce-test (added-strand resp 3) n1 (0 0)
(ch-msg (cat d l1) (cat pt n1)))
(strand-map 0 1 2 3)
(traces ((recv n1) (send n1)) ((recv n2) (send n2))
((recv (enc d l2 k)) (load (cat d l2) (cat pt-0 n2)) (send n2))
((stor (cat d l1) (cat pt n1)) (stor (cat d l2) (cat pt-0 n2))
(send (enc d l1 k)) (send (enc d l2 k)))
((recv (enc d l1 k-0)) (load (cat d l1) (cat pt n1)) (send n1)))
(label 6)
(parent 4)
(unrealized (4 0))
(maps ((3 0 1) ((n1 n1) (n2 n2) (d d) (l1 l1) (l2 l2))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n2 data) (d dev) (k skey) (pt pt-0 pval) (l2 l1 locn))
(deflistener n1)
(deflistener n2)
(defstrand resp 3 (m n2) (d d) (k k) (l l2))
(defstrand init 4 (n1 n1) (n2 n2) (d d) (k k) (l1 l1) (l2 l2))
(defstrand resp 3 (m n1) (d d) (k k) (l l1))
(precedes ((2 2) (1 0)) ((3 2) (4 0)) ((3 3) (2 0)) ((4 2) (0 0)))
(non-orig k)
(uniq-orig n1 n2 d)
(leads-to ((3 0) (4 1)) ((3 1) (2 1)))
(operation encryption-test (displaced 5 3 init 3) (enc d l1 k-0)
(4 0))
(strand-map 0 1 2 3 4)
(traces ((recv n1) (send n1)) ((recv n2) (send n2))
((recv (enc d l2 k)) (load (cat d l2) (cat pt-0 n2)) (send n2))
((stor (cat d l1) (cat pt n1)) (stor (cat d l2) (cat pt-0 n2))
(send (enc d l1 k)) (send (enc d l2 k)))
((recv (enc d l1 k)) (load (cat d l1) (cat pt n1)) (send n1)))
(label 7)
(parent 6)
(realized)
(shape)
(maps ((3 0 1) ((n1 n1) (n2 n2) (d d) (l1 l1) (l2 l2))))
(origs (n1 (3 0)) (n2 (3 1)) (d (3 2)) (pt (3 0)) (pt-0 (3 1))))
(comment "Nothing left to do")
(defprotocol devlocn basic
(defrole init
(vars (d dev) (l1 locn) (n1 data) (k skey))
(trace (stor (cat d l1) n1) (send (enc d l1 k)))
(uniq-orig n1 l1))
(defrole resp
(vars (d dev) (l locn) (m mesg) (k skey))
(trace (recv (enc d l k)) (load (cat d l) m) (send m))
(non-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))))
(defgenrule 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)))))
(defgenrule 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))))
(defgenrule 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))))
(defgenrule discreteAfter
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (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)))))
(defgenrule discreteBefore
(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)))))
(defgenrule trRl_init-at-0
(forall ((z strd))
(implies (p "init" z (idx 1)) (trans z (idx 0)))))
(defgenrule eff-resp-2
(forall ((i indx) (z1 z strd))
(implies (and (p "resp" z (idx 3)) (prec z (idx 2) z1 i))
(or (= z z1)
(and (p "resp" z (idx 2)) (prec z (idx 1) z1 i)))))))
(defskeleton devlocn
(vars (n1 n2 data) (d d-0 dev) (pt pt-0 pval) (l1 l1-0 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(defstrand init 1 (n1 n2) (d d-0) (l1 l1-0))
(deflistener n1)
(deflistener n2)
(uniq-orig n1 n2)
(traces ((stor (cat d l1) (cat pt n1)))
((stor (cat d-0 l1-0) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2)))
(label 8)
(unrealized (2 0) (3 0))
(preskeleton)
(maps
((0 1 2 3) ((n1 n1) (n2 n2) (d d) (l1 l1) (d-0 d-0) (l1-0 l1-0))))
(origs (pt-0 (1 0)) (n2 (1 0)) (pt (0 0)) (n1 (0 0)))
(comment "Not a skeleton"))
(defskeleton devlocn
(vars (n1 n2 data) (d d-0 dev) (pt pt-0 pval) (l1 l1-0 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(defstrand init 1 (n1 n2) (d d-0) (l1 l1-0))
(deflistener n1)
(deflistener n2)
(precedes ((0 0) (2 0)) ((1 0) (3 0)))
(uniq-orig n1 n2)
(traces ((stor (cat d l1) (cat pt n1)))
((stor (cat d-0 l1-0) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2)))
(label 9)
(parent 8)
(unrealized (2 0) (3 0))
(maps
((0 1 2 3) ((n1 n1) (n2 n2) (d d) (l1 l1) (d-0 d-0) (l1-0 l1-0))))
(origs (pt-0 (1 0)) (n2 (1 0)) (pt (0 0)) (n1 (0 0)))
(comment "Not closed under rules"))
(defskeleton devlocn
(vars (n1 n2 data) (d d-0 dev) (pt pt-0 pval) (l1 l1-0 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(defstrand init 1 (n1 n2) (d d-0) (l1 l1-0))
(deflistener n1)
(deflistener n2)
(precedes ((0 0) (2 0)) ((1 0) (3 0)))
(uniq-orig n1 n2)
(rule trRl_init-at-0)
(traces ((stor (cat d l1) (cat pt n1)))
((stor (cat d-0 l1-0) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2)))
(label 10)
(parent 9)
(unrealized (2 0) (3 0))
(maps
((0 1 2 3) ((n1 n1) (n2 n2) (d d) (l1 l1) (d-0 d-0) (l1-0 l1-0))))
(origs (pt-0 (1 0)) (n2 (1 0)) (pt (0 0)) (n1 (0 0)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 data) (d dev) (pt pval) (l1 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(deflistener n1)
(deflistener n1)
(precedes ((0 0) (1 0)) ((0 0) (2 0)))
(uniq-orig n1)
(operation collapsed 1 0)
(strand-map 0 0 1 2)
(traces ((stor (cat d l1) (cat pt n1))) ((recv n1) (send n1))
((recv n1) (send n1)))
(label 11)
(parent 10)
(unrealized (1 0) (2 0))
(maps ((0 0 1 2) ((n1 n1) (n2 n1) (d d) (l1 l1) (d-0 d) (l1-0 l1))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 data) (d dev) (pt pval) (l1 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(deflistener n1)
(precedes ((0 0) (1 0)))
(uniq-orig n1)
(operation collapsed 2 1)
(strand-map 0 1 1)
(traces ((stor (cat d l1) (cat pt n1))) ((recv n1) (send n1)))
(label 12)
(parent 11)
(unrealized (1 0))
(maps ((0 0 1 1) ((n1 n1) (n2 n1) (d d) (l1 l1) (d-0 d) (l1-0 l1))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n2 data) (d d-0 dev) (k skey) (pt pt-0 pval) (l1 l1-0 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(defstrand init 1 (n1 n2) (d d-0) (l1 l1-0))
(deflistener n1)
(deflistener n2)
(defstrand resp 3 (m n2) (d d-0) (k k) (l l1-0))
(precedes ((0 0) (2 0)) ((1 0) (4 1)) ((4 2) (3 0)))
(non-orig k)
(uniq-orig n1 n2)
(leads-to ((1 0) (4 1)))
(operation nonce-test (added-strand resp 3) n2 (3 0)
(ch-msg (cat d-0 l1-0) (cat pt-0 n2)))
(strand-map 0 1 2 3)
(traces ((stor (cat d l1) (cat pt n1)))
((stor (cat d-0 l1-0) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2))
((recv (enc d-0 l1-0 k)) (load (cat d-0 l1-0) (cat pt-0 n2))
(send n2)))
(label 13)
(parent 10)
(unrealized (2 0) (4 0))
(maps
((0 1 2 3) ((n1 n1) (n2 n2) (d d) (l1 l1) (d-0 d-0) (l1-0 l1-0))))
(comment "2 in cohort - 2 not yet seen"))
(defskeleton devlocn
(vars (n1 data) (d dev) (k skey) (pt pval) (l1 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(deflistener n1)
(deflistener n1)
(defstrand resp 3 (m n1) (d d) (k k) (l l1))
(precedes ((0 0) (1 0)) ((0 0) (3 1)) ((3 2) (2 0)))
(non-orig k)
(uniq-orig n1)
(leads-to ((0 0) (3 1)))
(operation nonce-test (added-strand resp 3) n1 (2 0)
(ch-msg (cat d l1) (cat pt n1)))
(strand-map 0 1 2)
(traces ((stor (cat d l1) (cat pt n1))) ((recv n1) (send n1))
((recv n1) (send n1))
((recv (enc d l1 k)) (load (cat d l1) (cat pt n1)) (send n1)))
(label 14)
(parent 11)
(seen 16)
(seen-ops
(16
(operation encryption-test (added-strand init 2) (enc d l1 k)
(3 0)) (strand-map 1 2 3 0)))
(unrealized (1 0) (3 0))
(maps ((0 0 1 2) ((n1 n1) (n2 n1) (d d) (l1 l1) (d-0 d) (l1-0 l1))))
(origs (pt (0 0)) (n1 (0 0)))
(comment "1 in cohort - 0 not yet seen"))
(defskeleton devlocn
(vars (n1 data) (d dev) (k skey) (pt pval) (l1 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(deflistener n1)
(defstrand resp 3 (m n1) (d d) (k k) (l l1))
(precedes ((0 0) (2 1)) ((2 2) (1 0)))
(non-orig k)
(uniq-orig n1)
(leads-to ((0 0) (2 1)))
(operation nonce-test (added-strand resp 3) n1 (1 0)
(ch-msg (cat d l1) (cat pt n1)))
(strand-map 0 1)
(traces ((stor (cat d l1) (cat pt n1))) ((recv n1) (send n1))
((recv (enc d l1 k)) (load (cat d l1) (cat pt n1)) (send n1)))
(label 15)
(parent 12)
(unrealized (2 0))
(maps ((0 0 1 1) ((n1 n1) (n2 n1) (d d) (l1 l1) (d-0 d) (l1-0 l1))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 data) (d dev) (k skey) (pt pval) (l1 locn))
(deflistener n1)
(deflistener n1)
(defstrand resp 3 (m n1) (d d) (k k) (l l1))
(defstrand init 2 (n1 n1) (d d) (k k) (l1 l1))
(precedes ((2 2) (1 0)) ((3 0) (0 0)) ((3 1) (2 0)))
(non-orig k)
(uniq-orig n1 l1)
(leads-to ((3 0) (2 1)))
(rule discreteBefore)
(operation encryption-test (displaced 0 5 init 2) (enc d l1 k) (4 0))
(strand-map 3 3 0 1 2)
(traces ((recv n1) (send n1)) ((recv n1) (send n1))
((recv (enc d l1 k)) (load (cat d l1) (cat pt n1)) (send n1))
((stor (cat d l1) (cat pt n1)) (send (enc d l1 k))))
(label 16)
(parent 13)
(unrealized (0 0))
(maps ((3 3 0 1) ((n1 n1) (n2 n1) (d d) (l1 l1) (d-0 d) (l1-0 l1))))
(origs (n1 (3 0)) (l1 (3 1)) (pt (3 0)))
(comment "2 in cohort - 2 not yet seen"))
(defskeleton devlocn
(vars (n1 n1-0 data) (d d-0 dev) (k skey) (pt pt-0 pval)
(l1 l1-0 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(deflistener n1)
(deflistener n1-0)
(defstrand resp 3 (m n1-0) (d d-0) (k k) (l l1-0))
(defstrand init 2 (n1 n1-0) (d d-0) (k k) (l1 l1-0))
(precedes ((0 0) (1 0)) ((3 2) (2 0)) ((4 1) (3 0)))
(non-orig k)
(uniq-orig n1 n1-0 l1-0)
(leads-to ((4 0) (3 1)))
(rule discreteBefore trRl_init-at-0)
(operation encryption-test (added-strand init 2) (enc d-0 l1-0 k)
(4 0))
(strand-map 0 2 3 4 1)
(traces ((stor (cat d l1) (cat pt n1))) ((recv n1) (send n1))
((recv n1-0) (send n1-0))
((recv (enc d-0 l1-0 k)) (load (cat d-0 l1-0) (cat pt-0 n1-0))
(send n1-0))
((stor (cat d-0 l1-0) (cat pt-0 n1-0)) (send (enc d-0 l1-0 k))))
(label 17)
(parent 13)
(unrealized (1 0))
(maps
((0 4 1 2) ((n1 n1) (n2 n1-0) (d d) (l1 l1) (d-0 d-0) (l1-0 l1-0))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 data) (d dev) (k skey) (pt pval) (l1 locn))
(deflistener n1)
(defstrand resp 3 (m n1) (d d) (k k) (l l1))
(defstrand init 2 (n1 n1) (d d) (k k) (l1 l1))
(precedes ((1 2) (0 0)) ((2 1) (1 0)))
(non-orig k)
(uniq-orig n1 l1)
(leads-to ((2 0) (1 1)))
(rule discreteBefore trRl_init-at-0)
(operation encryption-test (added-strand init 2) (enc d l1 k) (2 0))
(strand-map 1 2 0)
(traces ((recv n1) (send n1))
((recv (enc d l1 k)) (load (cat d l1) (cat pt n1)) (send n1))
((stor (cat d l1) (cat pt n1)) (send (enc d l1 k))))
(label 18)
(parent 15)
(realized)
(shape)
(maps ((2 2 0 0) ((n1 n1) (n2 n1) (d d) (l1 l1) (d-0 d) (l1-0 l1))))
(origs (n1 (2 0)) (l1 (2 1)) (pt (2 0))))
(defskeleton devlocn
(vars (n1 data) (d dev) (k skey) (pt pval) (l1 locn))
(deflistener n1)
(deflistener n1)
(defstrand resp 3 (m n1) (d d) (k k) (l l1))
(defstrand init 2 (n1 n1) (d d) (k k) (l1 l1))
(precedes ((2 2) (0 0)) ((2 2) (1 0)) ((3 1) (2 0)))
(non-orig k)
(uniq-orig n1 l1)
(leads-to ((3 0) (2 1)))
(operation nonce-test (displaced 4 2 resp 3) n1 (0 0)
(ch-msg (cat d l1) (cat pt n1)))
(strand-map 0 1 2 3)
(traces ((recv n1) (send n1)) ((recv n1) (send n1))
((recv (enc d l1 k)) (load (cat d l1) (cat pt n1)) (send n1))
((stor (cat d l1) (cat pt n1)) (send (enc d l1 k))))
(label 19)
(parent 16)
(realized)
(shape)
(maps ((3 3 0 1) ((n1 n1) (n2 n1) (d d) (l1 l1) (d-0 d) (l1-0 l1))))
(origs (n1 (3 0)) (l1 (3 1)) (pt (3 0))))
(defskeleton devlocn
(vars (n1 data) (d dev) (k k-0 skey) (pt pval) (l1 locn))
(deflistener n1)
(deflistener n1)
(defstrand resp 3 (m n1) (d d) (k k) (l l1))
(defstrand init 2 (n1 n1) (d d) (k k) (l1 l1))
(defstrand resp 3 (m n1) (d d) (k k-0) (l l1))
(precedes ((2 2) (1 0)) ((3 1) (2 0)) ((3 1) (4 0)) ((4 2) (0 0)))
(non-orig k k-0)
(uniq-orig n1 l1)
(leads-to ((3 0) (2 1)) ((3 0) (4 1)))
(operation nonce-test (added-strand resp 3) n1 (0 0)
(ch-msg (cat d l1) (cat pt n1)))
(strand-map 0 1 2 3)
(traces ((recv n1) (send n1)) ((recv n1) (send n1))
((recv (enc d l1 k)) (load (cat d l1) (cat pt n1)) (send n1))
((stor (cat d l1) (cat pt n1)) (send (enc d l1 k)))
((recv (enc d l1 k-0)) (load (cat d l1) (cat pt n1)) (send n1)))
(label 20)
(parent 16)
(unrealized (4 0))
(maps ((3 3 0 1) ((n1 n1) (n2 n1) (d d) (l1 l1) (d-0 d) (l1-0 l1))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n1-0 data) (d d-0 dev) (k k-0 skey) (pt pt-0 pval)
(l1 l1-0 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(deflistener n1)
(deflistener n1-0)
(defstrand resp 3 (m n1-0) (d d-0) (k k) (l l1-0))
(defstrand init 2 (n1 n1-0) (d d-0) (k k) (l1 l1-0))
(defstrand resp 3 (m n1) (d d) (k k-0) (l l1))
(precedes ((0 0) (5 1)) ((3 2) (2 0)) ((4 1) (3 0)) ((5 2) (1 0)))
(non-orig k k-0)
(uniq-orig n1 n1-0 l1-0)
(leads-to ((0 0) (5 1)) ((4 0) (3 1)))
(operation nonce-test (added-strand resp 3) n1 (1 0)
(ch-msg (cat d l1) (cat pt n1)))
(strand-map 0 1 2 3 4)
(traces ((stor (cat d l1) (cat pt n1))) ((recv n1) (send n1))
((recv n1-0) (send n1-0))
((recv (enc d-0 l1-0 k)) (load (cat d-0 l1-0) (cat pt-0 n1-0))
(send n1-0))
((stor (cat d-0 l1-0) (cat pt-0 n1-0)) (send (enc d-0 l1-0 k)))
((recv (enc d l1 k-0)) (load (cat d l1) (cat pt n1)) (send n1)))
(label 21)
(parent 17)
(seen 22)
(seen-ops
(22
(operation encryption-test (displaced 6 4 init 2)
(enc d-0 l1-0 k-0) (5 0)) (strand-map 3 0 1 2 3 4)))
(unrealized (5 0))
(maps
((0 4 1 2) ((n1 n1) (n2 n1-0) (d d) (l1 l1) (d-0 d-0) (l1-0 l1-0))))
(comment "2 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 data) (d dev) (k skey) (pt pval) (l1 locn))
(deflistener n1)
(deflistener n1)
(defstrand resp 3 (m n1) (d d) (k k) (l l1))
(defstrand init 2 (n1 n1) (d d) (k k) (l1 l1))
(defstrand resp 3 (m n1) (d d) (k k) (l l1))
(precedes ((2 2) (1 0)) ((3 1) (2 0)) ((3 1) (4 0)) ((4 2) (0 0)))
(non-orig k)
(uniq-orig n1 l1)
(leads-to ((3 0) (2 1)) ((3 0) (4 1)))
(operation encryption-test (displaced 5 3 init 2) (enc d l1 k-0)
(4 0))
(strand-map 0 1 2 3 4)
(traces ((recv n1) (send n1)) ((recv n1) (send n1))
((recv (enc d l1 k)) (load (cat d l1) (cat pt n1)) (send n1))
((stor (cat d l1) (cat pt n1)) (send (enc d l1 k)))
((recv (enc d l1 k)) (load (cat d l1) (cat pt n1)) (send n1)))
(label 22)
(parent 20)
(realized)
(shape)
(maps ((3 3 0 1) ((n1 n1) (n2 n1) (d d) (l1 l1) (d-0 d) (l1-0 l1))))
(origs (n1 (3 0)) (l1 (3 1)) (pt (3 0))))
(defskeleton devlocn
(vars (n1 n1-0 data) (d d-0 dev) (k k-0 skey) (pt pt-0 pval)
(l1 l1-0 locn))
(deflistener n1-0)
(deflistener n1)
(defstrand resp 3 (m n1) (d d-0) (k k) (l l1-0))
(defstrand init 2 (n1 n1) (d d-0) (k k) (l1 l1-0))
(defstrand resp 3 (m n1-0) (d d) (k k-0) (l l1))
(defstrand init 2 (n1 n1-0) (d d) (k k-0) (l1 l1))
(precedes ((2 2) (1 0)) ((3 1) (2 0)) ((4 2) (0 0)) ((5 1) (4 0)))
(non-orig k k-0)
(uniq-orig n1 n1-0 l1 l1-0)
(leads-to ((3 0) (2 1)) ((5 0) (4 1)))
(rule discreteBefore trRl_init-at-0)
(operation encryption-test (added-strand init 2) (enc d l1 k-0) (5 0))
(strand-map 1 2 3 4 5 0)
(traces ((recv n1-0) (send n1-0)) ((recv n1) (send n1))
((recv (enc d-0 l1-0 k)) (load (cat d-0 l1-0) (cat pt n1))
(send n1))
((stor (cat d-0 l1-0) (cat pt n1)) (send (enc d-0 l1-0 k)))
((recv (enc d l1 k-0)) (load (cat d l1) (cat pt-0 n1-0))
(send n1-0))
((stor (cat d l1) (cat pt-0 n1-0)) (send (enc d l1 k-0))))
(label 23)
(parent 21)
(realized)
(shape)
(maps
((5 3 0 1) ((n1 n1-0) (n2 n1) (d d) (l1 l1) (d-0 d-0) (l1-0 l1-0))))
(origs (n1-0 (5 0)) (l1 (5 1)) (pt-0 (5 0)) (n1 (3 0)) (l1-0 (3 1))
(pt (3 0))))
(comment "Nothing left to do")
(defprotocol devlocn basic
(defrole init
(vars (d dev) (l1 locn) (n1 data) (k skey))
(trace (stor (cat d l1) n1) (send (enc d l1 k)))
(uniq-orig n1 l1))
(defrole resp
(vars (d dev) (l locn) (m mesg) (k skey))
(trace (recv (enc d l k)) (load (cat d l) m) (send m))
(non-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))))
(defgenrule 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)))))
(defgenrule 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))))
(defgenrule 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))))
(defgenrule discreteAfter
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (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)))))
(defgenrule discreteBefore
(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)))))
(defgenrule trRl_init-at-0
(forall ((z strd))
(implies (p "init" z (idx 1)) (trans z (idx 0)))))
(defgenrule eff-resp-2
(forall ((i indx) (z1 z strd))
(implies (and (p "resp" z (idx 3)) (prec z (idx 2) z1 i))
(or (= z z1)
(and (p "resp" z (idx 2)) (prec z (idx 1) z1 i)))))))
(defskeleton devlocn
(vars (n1 n2 data) (d1 d2 dev) (pt pt-0 pval) (l1 l1-0 locn))
(defstrand init 1 (n1 n1) (d d1) (l1 l1))
(defstrand init 1 (n1 n2) (d d2) (l1 l1-0))
(deflistener n1)
(deflistener n2)
(uniq-orig n1 n2)
(facts (neq d1 d2))
(comment "With different devices they cannot have the same source.")
(traces ((stor (cat d1 l1) (cat pt n1)))
((stor (cat d2 l1-0) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2)))
(label 24)
(unrealized (2 0) (3 0))
(preskeleton)
(maps
((0 1 2 3) ((n1 n1) (n2 n2) (d1 d1) (d2 d2) (l1 l1) (l1-0 l1-0))))
(origs (pt-0 (1 0)) (n2 (1 0)) (pt (0 0)) (n1 (0 0)))
(comment "Not a skeleton"))
(defskeleton devlocn
(vars (n1 n2 data) (d1 d2 dev) (pt pt-0 pval) (l1 l1-0 locn))
(defstrand init 1 (n1 n1) (d d1) (l1 l1))
(defstrand init 1 (n1 n2) (d d2) (l1 l1-0))
(deflistener n1)
(deflistener n2)
(precedes ((0 0) (2 0)) ((1 0) (3 0)))
(uniq-orig n1 n2)
(facts (neq d1 d2))
(comment "With different devices they cannot have the same source.")
(traces ((stor (cat d1 l1) (cat pt n1)))
((stor (cat d2 l1-0) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2)))
(label 25)
(parent 24)
(unrealized (2 0) (3 0))
(maps
((0 1 2 3) ((n1 n1) (n2 n2) (d1 d1) (d2 d2) (l1 l1) (l1-0 l1-0))))
(origs (pt-0 (1 0)) (n2 (1 0)) (pt (0 0)) (n1 (0 0)))
(comment "Not closed under rules"))
(defskeleton devlocn
(vars (n1 n2 data) (d1 d2 dev) (pt pt-0 pval) (l1 l1-0 locn))
(defstrand init 1 (n1 n1) (d d1) (l1 l1))
(defstrand init 1 (n1 n2) (d d2) (l1 l1-0))
(deflistener n1)
(deflistener n2)
(precedes ((0 0) (2 0)) ((1 0) (3 0)))
(uniq-orig n1 n2)
(facts (neq d1 d2))
(comment "With different devices they cannot have the same source.")
(rule trRl_init-at-0)
(traces ((stor (cat d1 l1) (cat pt n1)))
((stor (cat d2 l1-0) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2)))
(label 26)
(parent 25)
(unrealized (2 0) (3 0))
(maps
((0 1 2 3) ((n1 n1) (n2 n2) (d1 d1) (d2 d2) (l1 l1) (l1-0 l1-0))))
(origs (pt-0 (1 0)) (n2 (1 0)) (pt (0 0)) (n1 (0 0)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n2 data) (d1 d2 dev) (k skey) (pt pt-0 pval) (l1 l1-0 locn))
(defstrand init 1 (n1 n1) (d d1) (l1 l1))
(defstrand init 1 (n1 n2) (d d2) (l1 l1-0))
(deflistener n1)
(deflistener n2)
(defstrand resp 3 (m n2) (d d2) (k k) (l l1-0))
(precedes ((0 0) (2 0)) ((1 0) (4 1)) ((4 2) (3 0)))
(non-orig k)
(uniq-orig n1 n2)
(facts (neq d1 d2))
(leads-to ((1 0) (4 1)))
(comment "With different devices they cannot have the same source.")
(operation nonce-test (added-strand resp 3) n2 (3 0)
(ch-msg (cat d2 l1-0) (cat pt-0 n2)))
(strand-map 0 1 2 3)
(traces ((stor (cat d1 l1) (cat pt n1)))
((stor (cat d2 l1-0) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2))
((recv (enc d2 l1-0 k)) (load (cat d2 l1-0) (cat pt-0 n2))
(send n2)))
(label 27)
(parent 26)
(unrealized (2 0) (4 0))
(maps
((0 1 2 3) ((n1 n1) (n2 n2) (d1 d1) (d2 d2) (l1 l1) (l1-0 l1-0))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n1-0 data) (d1 d2 dev) (k skey) (pt pt-0 pval)
(l1 l1-0 locn))
(defstrand init 1 (n1 n1) (d d1) (l1 l1))
(deflistener n1)
(deflistener n1-0)
(defstrand resp 3 (m n1-0) (d d2) (k k) (l l1-0))
(defstrand init 2 (n1 n1-0) (d d2) (k k) (l1 l1-0))
(precedes ((0 0) (1 0)) ((3 2) (2 0)) ((4 1) (3 0)))
(non-orig k)
(uniq-orig n1 n1-0 l1-0)
(facts (neq d1 d2))
(leads-to ((4 0) (3 1)))
(comment "With different devices they cannot have the same source.")
(rule discreteBefore trRl_init-at-0)
(operation encryption-test (added-strand init 2) (enc d2 l1-0 k)
(4 0))
(strand-map 0 2 3 4 1)
(traces ((stor (cat d1 l1) (cat pt n1))) ((recv n1) (send n1))
((recv n1-0) (send n1-0))
((recv (enc d2 l1-0 k)) (load (cat d2 l1-0) (cat pt-0 n1-0))
(send n1-0))
((stor (cat d2 l1-0) (cat pt-0 n1-0)) (send (enc d2 l1-0 k))))
(label 28)
(parent 27)
(unrealized (1 0))
(maps
((0 4 1 2) ((n1 n1) (n2 n1-0) (d1 d1) (d2 d2) (l1 l1) (l1-0 l1-0))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n1-0 data) (d1 d2 dev) (k k-0 skey) (pt pt-0 pval)
(l1 l1-0 locn))
(defstrand init 1 (n1 n1) (d d1) (l1 l1))
(deflistener n1)
(deflistener n1-0)
(defstrand resp 3 (m n1-0) (d d2) (k k) (l l1-0))
(defstrand init 2 (n1 n1-0) (d d2) (k k) (l1 l1-0))
(defstrand resp 3 (m n1) (d d1) (k k-0) (l l1))
(precedes ((0 0) (5 1)) ((3 2) (2 0)) ((4 1) (3 0)) ((5 2) (1 0)))
(non-orig k k-0)
(uniq-orig n1 n1-0 l1-0)
(facts (neq d1 d2))
(leads-to ((0 0) (5 1)) ((4 0) (3 1)))
(comment "With different devices they cannot have the same source.")
(operation nonce-test (added-strand resp 3) n1 (1 0)
(ch-msg (cat d1 l1) (cat pt n1)))
(strand-map 0 1 2 3 4)
(traces ((stor (cat d1 l1) (cat pt n1))) ((recv n1) (send n1))
((recv n1-0) (send n1-0))
((recv (enc d2 l1-0 k)) (load (cat d2 l1-0) (cat pt-0 n1-0))
(send n1-0))
((stor (cat d2 l1-0) (cat pt-0 n1-0)) (send (enc d2 l1-0 k)))
((recv (enc d1 l1 k-0)) (load (cat d1 l1) (cat pt n1)) (send n1)))
(label 29)
(parent 28)
(unrealized (5 0))
(maps
((0 4 1 2) ((n1 n1) (n2 n1-0) (d1 d1) (d2 d2) (l1 l1) (l1-0 l1-0))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n1-0 data) (d1 d2 dev) (k k-0 skey) (pt pt-0 pval)
(l1 l1-0 locn))
(deflistener n1-0)
(deflistener n1)
(defstrand resp 3 (m n1) (d d2) (k k) (l l1-0))
(defstrand init 2 (n1 n1) (d d2) (k k) (l1 l1-0))
(defstrand resp 3 (m n1-0) (d d1) (k k-0) (l l1))
(defstrand init 2 (n1 n1-0) (d d1) (k k-0) (l1 l1))
(precedes ((2 2) (1 0)) ((3 1) (2 0)) ((4 2) (0 0)) ((5 1) (4 0)))
(non-orig k k-0)
(uniq-orig n1 n1-0 l1 l1-0)
(facts (neq d1 d2))
(leads-to ((3 0) (2 1)) ((5 0) (4 1)))
(comment "With different devices they cannot have the same source.")
(rule discreteBefore trRl_init-at-0)
(operation encryption-test (added-strand init 2) (enc d1 l1 k-0)
(5 0))
(strand-map 1 2 3 4 5 0)
(traces ((recv n1-0) (send n1-0)) ((recv n1) (send n1))
((recv (enc d2 l1-0 k)) (load (cat d2 l1-0) (cat pt n1)) (send n1))
((stor (cat d2 l1-0) (cat pt n1)) (send (enc d2 l1-0 k)))
((recv (enc d1 l1 k-0)) (load (cat d1 l1) (cat pt-0 n1-0))
(send n1-0))
((stor (cat d1 l1) (cat pt-0 n1-0)) (send (enc d1 l1 k-0))))
(label 30)
(parent 29)
(realized)
(shape)
(maps
((5 3 0 1) ((n1 n1-0) (n2 n1) (d1 d1) (d2 d2) (l1 l1) (l1-0 l1-0))))
(origs (n1-0 (5 0)) (l1 (5 1)) (pt-0 (5 0)) (n1 (3 0)) (l1-0 (3 1))
(pt (3 0))))
(comment "Nothing left to do")
(defprotocol devlocn basic
(defrole init
(vars (d dev) (l1 locn) (n1 data) (k skey))
(trace (stor (cat d l1) n1) (send (enc d l1 k)))
(uniq-orig n1 l1))
(defrole resp
(vars (d dev) (l locn) (m mesg) (k skey))
(trace (recv (enc d l k)) (load (cat d l) m) (send m))
(non-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))))
(defgenrule 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)))))
(defgenrule 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))))
(defgenrule 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))))
(defgenrule discreteAfter
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (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)))))
(defgenrule discreteBefore
(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)))))
(defgenrule trRl_init-at-0
(forall ((z strd))
(implies (p "init" z (idx 1)) (trans z (idx 0)))))
(defgenrule eff-resp-2
(forall ((i indx) (z1 z strd))
(implies (and (p "resp" z (idx 3)) (prec z (idx 2) z1 i))
(or (= z z1)
(and (p "resp" z (idx 2)) (prec z (idx 1) z1 i)))))))
(defskeleton devlocn
(vars (n1 n2 data) (d d-0 dev) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(defstrand init 1 (n1 n2) (d d-0) (l1 l2))
(deflistener n1)
(deflistener n2)
(uniq-orig n1 n2)
(facts (neq l1 l2))
(comment "With different locns they cannot have the same source.")
(traces ((stor (cat d l1) (cat pt n1)))
((stor (cat d-0 l2) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2)))
(label 31)
(unrealized (2 0) (3 0))
(preskeleton)
(maps ((0 1 2 3) ((n1 n1) (n2 n2) (l1 l1) (l2 l2) (d d) (d-0 d-0))))
(origs (pt-0 (1 0)) (n2 (1 0)) (pt (0 0)) (n1 (0 0)))
(comment "Not a skeleton"))
(defskeleton devlocn
(vars (n1 n2 data) (d d-0 dev) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(defstrand init 1 (n1 n2) (d d-0) (l1 l2))
(deflistener n1)
(deflistener n2)
(precedes ((0 0) (2 0)) ((1 0) (3 0)))
(uniq-orig n1 n2)
(facts (neq l1 l2))
(comment "With different locns they cannot have the same source.")
(traces ((stor (cat d l1) (cat pt n1)))
((stor (cat d-0 l2) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2)))
(label 32)
(parent 31)
(unrealized (2 0) (3 0))
(maps ((0 1 2 3) ((n1 n1) (n2 n2) (l1 l1) (l2 l2) (d d) (d-0 d-0))))
(origs (pt-0 (1 0)) (n2 (1 0)) (pt (0 0)) (n1 (0 0)))
(comment "Not closed under rules"))
(defskeleton devlocn
(vars (n1 n2 data) (d d-0 dev) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(defstrand init 1 (n1 n2) (d d-0) (l1 l2))
(deflistener n1)
(deflistener n2)
(precedes ((0 0) (2 0)) ((1 0) (3 0)))
(uniq-orig n1 n2)
(facts (neq l1 l2))
(comment "With different locns they cannot have the same source.")
(rule trRl_init-at-0)
(traces ((stor (cat d l1) (cat pt n1)))
((stor (cat d-0 l2) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2)))
(label 33)
(parent 32)
(unrealized (2 0) (3 0))
(maps ((0 1 2 3) ((n1 n1) (n2 n2) (l1 l1) (l2 l2) (d d) (d-0 d-0))))
(origs (pt-0 (1 0)) (n2 (1 0)) (pt (0 0)) (n1 (0 0)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n2 data) (d d-0 dev) (k skey) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(defstrand init 1 (n1 n2) (d d-0) (l1 l2))
(deflistener n1)
(deflistener n2)
(defstrand resp 3 (m n2) (d d-0) (k k) (l l2))
(precedes ((0 0) (2 0)) ((1 0) (4 1)) ((4 2) (3 0)))
(non-orig k)
(uniq-orig n1 n2)
(facts (neq l1 l2))
(leads-to ((1 0) (4 1)))
(comment "With different locns they cannot have the same source.")
(operation nonce-test (added-strand resp 3) n2 (3 0)
(ch-msg (cat d-0 l2) (cat pt-0 n2)))
(strand-map 0 1 2 3)
(traces ((stor (cat d l1) (cat pt n1)))
((stor (cat d-0 l2) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2))
((recv (enc d-0 l2 k)) (load (cat d-0 l2) (cat pt-0 n2)) (send n2)))
(label 34)
(parent 33)
(unrealized (2 0) (4 0))
(maps ((0 1 2 3) ((n1 n1) (n2 n2) (l1 l1) (l2 l2) (d d) (d-0 d-0))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n1-0 data) (d d-0 dev) (k skey) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(deflistener n1)
(deflistener n1-0)
(defstrand resp 3 (m n1-0) (d d-0) (k k) (l l2))
(defstrand init 2 (n1 n1-0) (d d-0) (k k) (l1 l2))
(precedes ((0 0) (1 0)) ((3 2) (2 0)) ((4 1) (3 0)))
(non-orig k)
(uniq-orig n1 n1-0 l2)
(facts (neq l1 l2))
(leads-to ((4 0) (3 1)))
(comment "With different locns they cannot have the same source.")
(rule discreteBefore trRl_init-at-0)
(operation encryption-test (added-strand init 2) (enc d-0 l2 k) (4 0))
(strand-map 0 2 3 4 1)
(traces ((stor (cat d l1) (cat pt n1))) ((recv n1) (send n1))
((recv n1-0) (send n1-0))
((recv (enc d-0 l2 k)) (load (cat d-0 l2) (cat pt-0 n1-0))
(send n1-0))
((stor (cat d-0 l2) (cat pt-0 n1-0)) (send (enc d-0 l2 k))))
(label 35)
(parent 34)
(unrealized (1 0))
(maps ((0 4 1 2) ((n1 n1) (n2 n1-0) (l1 l1) (l2 l2) (d d) (d-0 d-0))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n1-0 data) (d d-0 dev) (k k-0 skey) (pt pt-0 pval)
(l1 l2 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(deflistener n1)
(deflistener n1-0)
(defstrand resp 3 (m n1-0) (d d-0) (k k) (l l2))
(defstrand init 2 (n1 n1-0) (d d-0) (k k) (l1 l2))
(defstrand resp 3 (m n1) (d d) (k k-0) (l l1))
(precedes ((0 0) (5 1)) ((3 2) (2 0)) ((4 1) (3 0)) ((5 2) (1 0)))
(non-orig k k-0)
(uniq-orig n1 n1-0 l2)
(facts (neq l1 l2))
(leads-to ((0 0) (5 1)) ((4 0) (3 1)))
(comment "With different locns they cannot have the same source.")
(operation nonce-test (added-strand resp 3) n1 (1 0)
(ch-msg (cat d l1) (cat pt n1)))
(strand-map 0 1 2 3 4)
(traces ((stor (cat d l1) (cat pt n1))) ((recv n1) (send n1))
((recv n1-0) (send n1-0))
((recv (enc d-0 l2 k)) (load (cat d-0 l2) (cat pt-0 n1-0))
(send n1-0))
((stor (cat d-0 l2) (cat pt-0 n1-0)) (send (enc d-0 l2 k)))
((recv (enc d l1 k-0)) (load (cat d l1) (cat pt n1)) (send n1)))
(label 36)
(parent 35)
(unrealized (5 0))
(maps ((0 4 1 2) ((n1 n1) (n2 n1-0) (l1 l1) (l2 l2) (d d) (d-0 d-0))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n1-0 data) (d d-0 dev) (k k-0 skey) (pt pt-0 pval)
(l1 l2 locn))
(deflistener n1-0)
(deflistener n1)
(defstrand resp 3 (m n1) (d d-0) (k k) (l l2))
(defstrand init 2 (n1 n1) (d d-0) (k k) (l1 l2))
(defstrand resp 3 (m n1-0) (d d) (k k-0) (l l1))
(defstrand init 2 (n1 n1-0) (d d) (k k-0) (l1 l1))
(precedes ((2 2) (1 0)) ((3 1) (2 0)) ((4 2) (0 0)) ((5 1) (4 0)))
(non-orig k k-0)
(uniq-orig n1 n1-0 l1 l2)
(facts (neq l1 l2))
(leads-to ((3 0) (2 1)) ((5 0) (4 1)))
(comment "With different locns they cannot have the same source.")
(rule discreteBefore trRl_init-at-0)
(operation encryption-test (added-strand init 2) (enc d l1 k-0) (5 0))
(strand-map 1 2 3 4 5 0)
(traces ((recv n1-0) (send n1-0)) ((recv n1) (send n1))
((recv (enc d-0 l2 k)) (load (cat d-0 l2) (cat pt n1)) (send n1))
((stor (cat d-0 l2) (cat pt n1)) (send (enc d-0 l2 k)))
((recv (enc d l1 k-0)) (load (cat d l1) (cat pt-0 n1-0))
(send n1-0))
((stor (cat d l1) (cat pt-0 n1-0)) (send (enc d l1 k-0))))
(label 37)
(parent 36)
(realized)
(shape)
(maps ((5 3 0 1) ((n1 n1-0) (n2 n1) (l1 l1) (l2 l2) (d d) (d-0 d-0))))
(origs (n1-0 (5 0)) (l1 (5 1)) (pt-0 (5 0)) (n1 (3 0)) (l2 (3 1))
(pt (3 0))))
(comment "Nothing left to do")
(defprotocol devlocn basic
(defrole init
(vars (d dev) (l1 locn) (n1 data) (k skey))
(trace (stor (cat d l1) n1) (send (enc d l1 k)))
(uniq-orig n1 l1))
(defrole resp
(vars (d dev) (l locn) (m mesg) (k skey))
(trace (recv (enc d l k)) (load (cat d l) m) (send m))
(non-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))))
(defgenrule 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)))))
(defgenrule 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))))
(defgenrule 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))))
(defgenrule discreteAfter
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (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)))))
(defgenrule discreteBefore
(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)))))
(defgenrule trRl_init-at-0
(forall ((z strd))
(implies (p "init" z (idx 1)) (trans z (idx 0)))))
(defgenrule eff-resp-2
(forall ((i indx) (z1 z strd))
(implies (and (p "resp" z (idx 3)) (prec z (idx 2) z1 i))
(or (= z z1)
(and (p "resp" z (idx 2)) (prec z (idx 1) z1 i)))))))
(defskeleton devlocn
(vars (n1 n2 data) (d dev) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(defstrand init 1 (n1 n2) (d d) (l1 l2))
(deflistener n1)
(deflistener n2)
(uniq-orig n1 n2)
(facts (neq l1 l2))
(comment
"With different locns they cannot have the same source even if the devs are the same.")
(traces ((stor (cat d l1) (cat pt n1)))
((stor (cat d l2) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2)))
(label 38)
(unrealized (2 0) (3 0))
(preskeleton)
(maps ((0 1 2 3) ((n1 n1) (n2 n2) (l1 l1) (l2 l2) (d d))))
(origs (pt-0 (1 0)) (n2 (1 0)) (pt (0 0)) (n1 (0 0)))
(comment "Not a skeleton"))
(defskeleton devlocn
(vars (n1 n2 data) (d dev) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(defstrand init 1 (n1 n2) (d d) (l1 l2))
(deflistener n1)
(deflistener n2)
(precedes ((0 0) (2 0)) ((1 0) (3 0)))
(uniq-orig n1 n2)
(facts (neq l1 l2))
(comment
"With different locns they cannot have the same source even if the devs are the same.")
(traces ((stor (cat d l1) (cat pt n1)))
((stor (cat d l2) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2)))
(label 39)
(parent 38)
(unrealized (2 0) (3 0))
(maps ((0 1 2 3) ((n1 n1) (n2 n2) (l1 l1) (l2 l2) (d d))))
(origs (pt-0 (1 0)) (n2 (1 0)) (pt (0 0)) (n1 (0 0)))
(comment "Not closed under rules"))
(defskeleton devlocn
(vars (n1 n2 data) (d dev) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(defstrand init 1 (n1 n2) (d d) (l1 l2))
(deflistener n1)
(deflistener n2)
(precedes ((0 0) (2 0)) ((1 0) (3 0)))
(uniq-orig n1 n2)
(facts (neq l1 l2))
(comment
"With different locns they cannot have the same source even if the devs are the same.")
(rule trRl_init-at-0)
(traces ((stor (cat d l1) (cat pt n1)))
((stor (cat d l2) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2)))
(label 40)
(parent 39)
(unrealized (2 0) (3 0))
(maps ((0 1 2 3) ((n1 n1) (n2 n2) (l1 l1) (l2 l2) (d d))))
(origs (pt-0 (1 0)) (n2 (1 0)) (pt (0 0)) (n1 (0 0)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n2 data) (d dev) (k skey) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(defstrand init 1 (n1 n2) (d d) (l1 l2))
(deflistener n1)
(deflistener n2)
(defstrand resp 3 (m n2) (d d) (k k) (l l2))
(precedes ((0 0) (2 0)) ((1 0) (4 1)) ((4 2) (3 0)))
(non-orig k)
(uniq-orig n1 n2)
(facts (neq l1 l2))
(leads-to ((1 0) (4 1)))
(comment
"With different locns they cannot have the same source even if the devs are the same.")
(operation nonce-test (added-strand resp 3) n2 (3 0)
(ch-msg (cat d l2) (cat pt-0 n2)))
(strand-map 0 1 2 3)
(traces ((stor (cat d l1) (cat pt n1)))
((stor (cat d l2) (cat pt-0 n2))) ((recv n1) (send n1))
((recv n2) (send n2))
((recv (enc d l2 k)) (load (cat d l2) (cat pt-0 n2)) (send n2)))
(label 41)
(parent 40)
(unrealized (2 0) (4 0))
(maps ((0 1 2 3) ((n1 n1) (n2 n2) (l1 l1) (l2 l2) (d d))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n1-0 data) (d dev) (k skey) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(deflistener n1)
(deflistener n1-0)
(defstrand resp 3 (m n1-0) (d d) (k k) (l l2))
(defstrand init 2 (n1 n1-0) (d d) (k k) (l1 l2))
(precedes ((0 0) (1 0)) ((3 2) (2 0)) ((4 1) (3 0)))
(non-orig k)
(uniq-orig n1 n1-0 l2)
(facts (neq l1 l2))
(leads-to ((4 0) (3 1)))
(comment
"With different locns they cannot have the same source even if the devs are the same.")
(rule discreteBefore trRl_init-at-0)
(operation encryption-test (added-strand init 2) (enc d l2 k) (4 0))
(strand-map 0 2 3 4 1)
(traces ((stor (cat d l1) (cat pt n1))) ((recv n1) (send n1))
((recv n1-0) (send n1-0))
((recv (enc d l2 k)) (load (cat d l2) (cat pt-0 n1-0)) (send n1-0))
((stor (cat d l2) (cat pt-0 n1-0)) (send (enc d l2 k))))
(label 42)
(parent 41)
(unrealized (1 0))
(maps ((0 4 1 2) ((n1 n1) (n2 n1-0) (l1 l1) (l2 l2) (d d))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n1-0 data) (d dev) (k k-0 skey) (pt pt-0 pval) (l1 l2 locn))
(defstrand init 1 (n1 n1) (d d) (l1 l1))
(deflistener n1)
(deflistener n1-0)
(defstrand resp 3 (m n1-0) (d d) (k k) (l l2))
(defstrand init 2 (n1 n1-0) (d d) (k k) (l1 l2))
(defstrand resp 3 (m n1) (d d) (k k-0) (l l1))
(precedes ((0 0) (5 1)) ((3 2) (2 0)) ((4 1) (3 0)) ((5 2) (1 0)))
(non-orig k k-0)
(uniq-orig n1 n1-0 l2)
(facts (neq l1 l2))
(leads-to ((0 0) (5 1)) ((4 0) (3 1)))
(comment
"With different locns they cannot have the same source even if the devs are the same.")
(operation nonce-test (added-strand resp 3) n1 (1 0)
(ch-msg (cat d l1) (cat pt n1)))
(strand-map 0 1 2 3 4)
(traces ((stor (cat d l1) (cat pt n1))) ((recv n1) (send n1))
((recv n1-0) (send n1-0))
((recv (enc d l2 k)) (load (cat d l2) (cat pt-0 n1-0)) (send n1-0))
((stor (cat d l2) (cat pt-0 n1-0)) (send (enc d l2 k)))
((recv (enc d l1 k-0)) (load (cat d l1) (cat pt n1)) (send n1)))
(label 43)
(parent 42)
(unrealized (5 0))
(maps ((0 4 1 2) ((n1 n1) (n2 n1-0) (l1 l1) (l2 l2) (d d))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 n1-0 data) (d dev) (k k-0 skey) (pt pt-0 pval) (l1 l2 locn))
(deflistener n1-0)
(deflistener n1)
(defstrand resp 3 (m n1) (d d) (k k) (l l2))
(defstrand init 2 (n1 n1) (d d) (k k) (l1 l2))
(defstrand resp 3 (m n1-0) (d d) (k k-0) (l l1))
(defstrand init 2 (n1 n1-0) (d d) (k k-0) (l1 l1))
(precedes ((2 2) (1 0)) ((3 1) (2 0)) ((4 2) (0 0)) ((5 1) (4 0)))
(non-orig k k-0)
(uniq-orig n1 n1-0 l1 l2)
(facts (neq l1 l2))
(leads-to ((3 0) (2 1)) ((5 0) (4 1)))
(comment
"With different locns they cannot have the same source even if the devs are the same.")
(rule discreteBefore trRl_init-at-0)
(operation encryption-test (added-strand init 2) (enc d l1 k-0) (5 0))
(strand-map 1 2 3 4 5 0)
(traces ((recv n1-0) (send n1-0)) ((recv n1) (send n1))
((recv (enc d l2 k)) (load (cat d l2) (cat pt n1)) (send n1))
((stor (cat d l2) (cat pt n1)) (send (enc d l2 k)))
((recv (enc d l1 k-0)) (load (cat d l1) (cat pt-0 n1-0))
(send n1-0))
((stor (cat d l1) (cat pt-0 n1-0)) (send (enc d l1 k-0))))
(label 44)
(parent 43)
(realized)
(shape)
(maps ((5 3 0 1) ((n1 n1-0) (n2 n1) (l1 l1) (l2 l2) (d d))))
(origs (n1-0 (5 0)) (l1 (5 1)) (pt-0 (5 0)) (n1 (3 0)) (l2 (3 1))
(pt (3 0))))
(comment "Nothing left to do")
(defprotocol devlocn basic
(defrole init
(vars (d dev) (l1 locn) (n1 data) (k skey))
(trace (stor (cat d l1) n1) (send (enc d l1 k)))
(uniq-orig n1 l1))
(defrole resp
(vars (dl m mesg) (k skey))
(trace (recv (enc dl k)) (load dl m) (send m))
(non-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))))
(defgenrule 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)))))
(defgenrule 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))))
(defgenrule 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))))
(defgenrule discreteAfter
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (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)))))
(defgenrule discreteBefore
(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)))))
(defgenrule trRl_init-at-0
(forall ((z strd))
(implies (p "init" z (idx 1)) (trans z (idx 0)))))
(defgenrule eff-resp-2
(forall ((i indx) (z1 z strd))
(implies (and (p "resp" z (idx 3)) (prec z (idx 2) z1 i))
(or (= z z1)
(and (p "resp" z (idx 2)) (prec z (idx 1) z1 i))))))
(comment
"Notice the mesg var dl as location for load. Only allowed because it is acquired."))
(defskeleton devlocn
(vars (m dl mesg) (k skey) (pt pval))
(defstrand resp 2 (dl dl) (m m) (k k))
(non-orig k)
(gen-st m)
(traces ((recv (enc dl k)) (load dl (cat pt m))))
(label 45)
(unrealized (0 0) (0 1))
(maps ((0) ((m m) (dl dl) (k k))))
(origs)
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (m mesg) (n1 data) (d dev) (k skey) (pt pt-0 pval) (l1 locn))
(defstrand resp 2 (dl (cat d l1)) (m m) (k k))
(defstrand init 2 (n1 n1) (d d) (k k) (l1 l1))
(precedes ((1 1) (0 0)))
(non-orig k)
(uniq-orig n1 l1)
(gen-st m)
(rule trRl_init-at-0)
(operation encryption-test (added-strand init 2) (enc d l1 k) (0 0))
(strand-map 0)
(traces ((recv (enc d l1 k)) (load (cat d l1) (cat pt m)))
((stor (cat d l1) (cat pt-0 n1)) (send (enc d l1 k))))
(label 46)
(parent 45)
(unrealized (0 1))
(maps ((0) ((m m) (dl (cat d l1)) (k k))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n1 data) (d dev) (k skey) (pt pval) (l1 locn))
(defstrand resp 2 (dl (cat d l1)) (m n1) (k k))
(defstrand init 2 (n1 n1) (d d) (k k) (l1 l1))
(precedes ((1 1) (0 0)))
(non-orig k)
(uniq-orig n1 l1)
(gen-st n1)
(leads-to ((1 0) (0 1)))
(rule discreteBefore trRl_init-at-0)
(operation channel-test (added-strand init 1)
(ch-msg (cat d l1) (cat pt n1)) (0 1))
(strand-map 0 1)
(traces ((recv (enc d l1 k)) (load (cat d l1) (cat pt n1)))
((stor (cat d l1) (cat pt n1)) (send (enc d l1 k))))
(label 47)
(parent 46)
(realized)
(shape)
(maps ((0) ((m n1) (dl (cat d l1)) (k k))))
(origs (n1 (1 0)) (pt (1 0)) (l1 (1 1))))
(comment "Nothing left to do")
(defprotocol devlocn basic
(defrole init
(vars (d dev) (l1 locn) (n1 data) (k skey))
(trace (stor (cat d l1) n1) (send (enc d l1 k)))
(uniq-orig n1 l1))
(defrole resp
(vars (dl m mesg) (k skey))
(trace (recv (enc dl k)) (load dl m) (send m))
(non-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))))
(defgenrule 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)))))
(defgenrule 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))))
(defgenrule 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))))
(defgenrule discreteAfter
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (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)))))
(defgenrule discreteBefore
(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)))))
(defgenrule trRl_init-at-0
(forall ((z strd))
(implies (p "init" z (idx 1)) (trans z (idx 0)))))
(defgenrule eff-resp-2
(forall ((i indx) (z1 z strd))
(implies (and (p "resp" z (idx 3)) (prec z (idx 2) z1 i))
(or (= z z1)
(and (p "resp" z (idx 2)) (prec z (idx 1) z1 i))))))
(comment
"Notice the mesg var dl as location for load. Only allowed because it is acquired."))
(defskeleton devlocn
(vars (m dl mesg) (k skey) (pt pval))
(defstrand resp 2 (dl dl) (m m) (k k))
(non-orig k)
(comment
"Possibly strange interpretation. Init has uniq-orig n1 and l1. Resp doesn't necessarily retrieve n1, even though nobody but Init should know l1, so nobody else could stor into it.")
(traces ((recv (enc dl k)) (load dl (cat pt m))))
(label 48)
(unrealized (0 0))
(maps ((0) ((m m) (dl dl) (k k))))
(origs)
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (m mesg) (n1 data) (d dev) (k skey) (pt pt-0 pval) (l1 locn))
(defstrand resp 2 (dl (cat d l1)) (m m) (k k))
(defstrand init 2 (n1 n1) (d d) (k k) (l1 l1))
(precedes ((1 1) (0 0)))
(non-orig k)
(uniq-orig n1 l1)
(comment
"Possibly strange interpretation. Init has uniq-orig n1 and l1. Resp doesn't necessarily retrieve n1, even though nobody but Init should know l1, so nobody else could stor into it.")
(rule trRl_init-at-0)
(operation encryption-test (added-strand init 2) (enc d l1 k) (0 0))
(strand-map 0)
(traces ((recv (enc d l1 k)) (load (cat d l1) (cat pt m)))
((stor (cat d l1) (cat pt-0 n1)) (send (enc d l1 k))))
(label 49)
(parent 48)
(realized)
(shape)
(maps ((0) ((m m) (dl (cat d l1)) (k k))))
(origs (n1 (1 0)) (l1 (1 1)) (pt-0 (1 0))))
(comment "Nothing left to do")
(defprotocol devlocn basic
(defrole init
(vars (d dev) (l1 locn) (n1 data) (k skey))
(trace (stor (cat d l1) n1) (send (enc d l1 k)))
(uniq-orig n1 l1))
(defrole resp
(vars (dl m mesg) (k skey))
(trace (recv (enc dl k)) (load dl m) (send m))
(non-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))))
(defgenrule 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)))))
(defgenrule 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))))
(defgenrule 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))))
(defgenrule discreteAfter
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (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)))))
(defgenrule discreteBefore
(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)))))
(defgenrule trRl_init-at-0
(forall ((z strd))
(implies (p "init" z (idx 1)) (trans z (idx 0)))))
(defgenrule eff-resp-2
(forall ((i indx) (z1 z strd))
(implies (and (p "resp" z (idx 3)) (prec z (idx 2) z1 i))
(or (= z z1)
(and (p "resp" z (idx 2)) (prec z (idx 1) z1 i))))))
(comment
"Notice the mesg var dl as location for load. Only allowed because it is acquired."))
(defskeleton devlocn
(vars (dl mesg) (n data) (d dev) (k k-0 skey) (pt pt-0 pval)
(l1 locn))
(defstrand resp 2 (dl dl) (m n) (k k))
(defstrand init 2 (n1 n) (d d) (k k-0) (l1 l1))
(non-orig k)
(uniq-orig n l1)
(comment
"Even if loaded value is not gen-st, since it's uniq-orig, nonce-test still applies.")
(traces ((recv (enc dl k)) (load dl (cat pt n)))
((stor (cat d l1) (cat pt-0 n)) (send (enc d l1 k-0))))
(label 50)
(unrealized (0 0) (0 1))
(preskeleton)
(maps ((0 1) ((n n) (dl dl) (k k) (d d) (l1 l1) (k-0 k-0))))
(origs (pt-0 (1 0)) (l1 (1 1)) (n (1 0)))
(comment "Not a skeleton"))
(defskeleton devlocn
(vars (dl mesg) (n data) (d dev) (k k-0 skey) (pt pt-0 pval)
(l1 locn))
(defstrand resp 2 (dl dl) (m n) (k k))
(defstrand init 2 (n1 n) (d d) (k k-0) (l1 l1))
(precedes ((1 0) (0 1)))
(non-orig k)
(uniq-orig n l1)
(comment
"Even if loaded value is not gen-st, since it's uniq-orig, nonce-test still applies.")
(traces ((recv (enc dl k)) (load dl (cat pt n)))
((stor (cat d l1) (cat pt-0 n)) (send (enc d l1 k-0))))
(label 51)
(parent 50)
(unrealized (0 0) (0 1))
(maps ((0 1) ((n n) (dl dl) (k k) (d d) (l1 l1) (k-0 k-0))))
(origs (pt-0 (1 0)) (l1 (1 1)) (n (1 0)))
(comment "Not closed under rules"))
(defskeleton devlocn
(vars (dl mesg) (n data) (d dev) (k k-0 skey) (pt pt-0 pval)
(l1 locn))
(defstrand resp 2 (dl dl) (m n) (k k))
(defstrand init 2 (n1 n) (d d) (k k-0) (l1 l1))
(precedes ((1 0) (0 1)))
(non-orig k)
(uniq-orig n l1)
(comment
"Even if loaded value is not gen-st, since it's uniq-orig, nonce-test still applies.")
(rule trRl_init-at-0)
(traces ((recv (enc dl k)) (load dl (cat pt n)))
((stor (cat d l1) (cat pt-0 n)) (send (enc d l1 k-0))))
(label 52)
(parent 51)
(unrealized (0 0) (0 1))
(maps ((0 1) ((n n) (dl dl) (k k) (d d) (l1 l1) (k-0 k-0))))
(origs (pt-0 (1 0)) (l1 (1 1)) (n (1 0)))
(comment "2 in cohort - 2 not yet seen"))
(defskeleton devlocn
(vars (n data) (d dev) (k skey) (pt pt-0 pval) (l1 locn))
(defstrand resp 2 (dl (cat d l1)) (m n) (k k))
(defstrand init 2 (n1 n) (d d) (k k) (l1 l1))
(precedes ((1 1) (0 0)))
(non-orig k)
(uniq-orig n l1)
(comment
"Even if loaded value is not gen-st, since it's uniq-orig, nonce-test still applies.")
(operation encryption-test (displaced 2 1 init 2) (enc d-0 l1-0 k-0)
(0 0))
(strand-map 0 1)
(traces ((recv (enc d l1 k)) (load (cat d l1) (cat pt n)))
((stor (cat d l1) (cat pt-0 n)) (send (enc d l1 k))))
(label 53)
(parent 52)
(unrealized (0 1))
(maps ((0 1) ((n n) (dl (cat d l1)) (k k) (d d) (l1 l1) (k-0 k))))
(origs (n (1 0)) (l1 (1 1)) (pt-0 (1 0)))
(comment "2 in cohort - 2 not yet seen"))
(defskeleton devlocn
(vars (n n1 data) (d d-0 dev) (k k-0 skey) (pt pt-0 pt-1 pval)
(l1 l1-0 locn))
(defstrand resp 2 (dl (cat d-0 l1-0)) (m n) (k k))
(defstrand init 2 (n1 n) (d d) (k k-0) (l1 l1))
(defstrand init 2 (n1 n1) (d d-0) (k k) (l1 l1-0))
(precedes ((1 0) (0 1)) ((2 1) (0 0)))
(non-orig k)
(uniq-orig n n1 l1 l1-0)
(comment
"Even if loaded value is not gen-st, since it's uniq-orig, nonce-test still applies.")
(rule trRl_init-at-0)
(operation encryption-test (added-strand init 2) (enc d-0 l1-0 k)
(0 0))
(strand-map 0 1)
(traces ((recv (enc d-0 l1-0 k)) (load (cat d-0 l1-0) (cat pt n)))
((stor (cat d l1) (cat pt-0 n)) (send (enc d l1 k-0)))
((stor (cat d-0 l1-0) (cat pt-1 n1)) (send (enc d-0 l1-0 k))))
(label 54)
(parent 52)
(unrealized (0 1))
(maps
((0 1) ((n n) (dl (cat d-0 l1-0)) (k k) (d d) (l1 l1) (k-0 k-0))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n data) (d dev) (k skey) (pt pval) (l1 locn))
(defstrand resp 2 (dl (cat d l1)) (m n) (k k))
(defstrand init 2 (n1 n) (d d) (k k) (l1 l1))
(precedes ((1 1) (0 0)))
(non-orig k)
(uniq-orig n l1)
(leads-to ((1 0) (0 1)))
(comment
"Even if loaded value is not gen-st, since it's uniq-orig, nonce-test still applies.")
(operation nonce-test (contracted (pt-0 pt)) n (0 1)
(ch-msg (cat d l1) (cat pt n)))
(strand-map 0 1)
(traces ((recv (enc d l1 k)) (load (cat d l1) (cat pt n)))
((stor (cat d l1) (cat pt n)) (send (enc d l1 k))))
(label 55)
(parent 53)
(realized)
(shape)
(maps ((0 1) ((n n) (dl (cat d l1)) (k k) (d d) (l1 l1) (k-0 k))))
(origs (n (1 0)) (l1 (1 1)) (pt (1 0))))
(defskeleton devlocn
(vars (n data) (d dev) (k k-0 skey) (pt pt-0 pval) (l1 locn))
(defstrand resp 2 (dl (cat d l1)) (m n) (k k))
(defstrand init 2 (n1 n) (d d) (k k) (l1 l1))
(defstrand resp 3 (dl (cat d l1)) (m n) (k k-0))
(precedes ((1 1) (0 0)) ((1 1) (2 0)) ((2 2) (0 1)))
(non-orig k k-0)
(uniq-orig n l1)
(leads-to ((1 0) (2 1)))
(comment
"Even if loaded value is not gen-st, since it's uniq-orig, nonce-test still applies.")
(operation nonce-test (added-strand resp 3) n (0 1)
(ch-msg (cat d l1) (cat pt-0 n)))
(strand-map 0 1)
(traces ((recv (enc d l1 k)) (load (cat d l1) (cat pt n)))
((stor (cat d l1) (cat pt-0 n)) (send (enc d l1 k)))
((recv (enc d l1 k-0)) (load (cat d l1) (cat pt-0 n)) (send n)))
(label 56)
(parent 53)
(unrealized (2 0))
(maps ((0 1) ((n n) (dl (cat d l1)) (k k) (d d) (l1 l1) (k-0 k))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n n1 data) (d d-0 dev) (k k-0 k-1 skey) (pt pt-0 pt-1 pval)
(l1 l1-0 locn))
(defstrand resp 2 (dl (cat d-0 l1-0)) (m n) (k k))
(defstrand init 2 (n1 n) (d d) (k k-0) (l1 l1))
(defstrand init 2 (n1 n1) (d d-0) (k k) (l1 l1-0))
(defstrand resp 3 (dl (cat d l1)) (m n) (k k-1))
(precedes ((1 1) (3 0)) ((2 1) (0 0)) ((3 2) (0 1)))
(non-orig k k-1)
(uniq-orig n n1 l1 l1-0)
(leads-to ((1 0) (3 1)))
(comment
"Even if loaded value is not gen-st, since it's uniq-orig, nonce-test still applies.")
(operation nonce-test (added-strand resp 3) n (0 1)
(ch-msg (cat d l1) (cat pt-0 n)))
(strand-map 0 1 2)
(traces ((recv (enc d-0 l1-0 k)) (load (cat d-0 l1-0) (cat pt n)))
((stor (cat d l1) (cat pt-0 n)) (send (enc d l1 k-0)))
((stor (cat d-0 l1-0) (cat pt-1 n1)) (send (enc d-0 l1-0 k)))
((recv (enc d l1 k-1)) (load (cat d l1) (cat pt-0 n)) (send n)))
(label 57)
(parent 54)
(unrealized (3 0))
(maps
((0 1) ((n n) (dl (cat d-0 l1-0)) (k k) (d d) (l1 l1) (k-0 k-0))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton devlocn
(vars (n data) (d dev) (k skey) (pt pt-0 pval) (l1 locn))
(defstrand resp 2 (dl (cat d l1)) (m n) (k k))
(defstrand init 2 (n1 n) (d d) (k k) (l1 l1))
(defstrand resp 3 (dl (cat d l1)) (m n) (k k))
(precedes ((1 1) (0 0)) ((1 1) (2 0)) ((2 2) (0 1)))
(non-orig k)
(uniq-orig n l1)
(leads-to ((1 0) (2 1)))
(comment
"Even if loaded value is not gen-st, since it's uniq-orig, nonce-test still applies.")
(operation encryption-test (displaced 3 1 init 2) (enc d l1 k-0)
(2 0))
(strand-map 0 1 2)
(traces ((recv (enc d l1 k)) (load (cat d l1) (cat pt n)))
((stor (cat d l1) (cat pt-0 n)) (send (enc d l1 k)))
((recv (enc d l1 k)) (load (cat d l1) (cat pt-0 n)) (send n)))
(label 58)
(parent 56)
(realized)
(shape)
(maps ((0 1) ((n n) (dl (cat d l1)) (k k) (d d) (l1 l1) (k-0 k))))
(origs (n (1 0)) (l1 (1 1)) (pt-0 (1 0))))
(defskeleton devlocn
(vars (n n1 data) (d d-0 dev) (k k-0 skey) (pt pt-0 pt-1 pval)
(l1 l1-0 locn))
(defstrand resp 2 (dl (cat d-0 l1-0)) (m n) (k k))
(defstrand init 2 (n1 n) (d d) (k k-0) (l1 l1))
(defstrand init 2 (n1 n1) (d d-0) (k k) (l1 l1-0))
(defstrand resp 3 (dl (cat d l1)) (m n) (k k-0))
(precedes ((1 1) (3 0)) ((2 1) (0 0)) ((3 2) (0 1)))
(non-orig k k-0)
(uniq-orig n n1 l1 l1-0)
(leads-to ((1 0) (3 1)))
(comment
"Even if loaded value is not gen-st, since it's uniq-orig, nonce-test still applies.")
(operation encryption-test (displaced 4 1 init 2) (enc d l1 k-1)
(3 0))
(strand-map 0 1 2 3)
(traces ((recv (enc d-0 l1-0 k)) (load (cat d-0 l1-0) (cat pt n)))
((stor (cat d l1) (cat pt-0 n)) (send (enc d l1 k-0)))
((stor (cat d-0 l1-0) (cat pt-1 n1)) (send (enc d-0 l1-0 k)))
((recv (enc d l1 k-0)) (load (cat d l1) (cat pt-0 n)) (send n)))
(label 59)
(parent 57)
(realized)
(shape)
(maps
((0 1) ((n n) (dl (cat d-0 l1-0)) (k k) (d d) (l1 l1) (k-0 k-0))))
(origs (n (1 0)) (l1 (1 1)) (pt-0 (1 0)) (n1 (2 0)) (l1-0 (2 1))
(pt-1 (2 0))))
(comment "Nothing left to do")