cpsa-4.4.4: tst/attest_shapes.tst
(comment "CPSA 4.3.1")
(comment "Extracted shapes")
(herald attest-door)
(comment "CPSA 4.3.1")
(comment "All input read from tst/attest.scm")
(defprotocol attest-door basic
(defrole appraise
(vars (d p a akey) (n text))
(trace (recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
(comment "The appraiser for the door"))
(defrole person
(vars (d p a akey) (k skey) (n t text))
(trace (send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
(uniq-orig k n)
(comment "Person requesting door entry"))
(defrole door
(vars (d p akey) (k skey) (t text))
(trace (recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))
(uniq-orig t))
(defrole squealer
(vars (d p akey) (k skey))
(trace (recv (enc (enc k (invk p)) d)) (send k))
(comment "Fake door"))
(defrule yes
(forall ((z strd) (a akey))
(implies
(and (p "appraise" z 2) (p "appraise" "a" z a) (non (invk a)))
(exists ((d akey))
(and (p "appraise" "d" z d) (non (invk d))))))
(comment "Appraisal succeeded"))
(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))))
(comment "Door attestations protocol"))
(defskeleton attest-door
(vars (k skey) (n t text) (p a d akey))
(defstrand person 5 (k k) (n n) (t t) (d d) (p p) (a a))
(non-orig (invk p) (invk a))
(uniq-orig k n)
(comment "Analyze from the person's perspective")
(traces
((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t)))
(label 0)
(unrealized (0 1))
(origs (k (0 2)) (n (0 0)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton attest-door
(vars (k skey) (n t text) (p a d akey))
(defstrand person 5 (k k) (n n) (t t) (d d) (p p) (a a))
(defstrand appraise 2 (n n) (d d) (p p) (a a))
(defstrand door 2 (k k) (t t) (d d) (p p))
(precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
(non-orig (invk p) (invk a) (invk d))
(uniq-orig k n t)
(operation nonce-test (contracted (d-0 d) (p-0 p)) k (2 0)
(enc (enc k (invk p)) d))
(traces
((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
((recv (enc (enc k (invk p)) d)) (send (enc t k))))
(label 4)
(parent 0)
(realized)
(shape)
(maps ((0) ((p p) (a a) (d d) (k k) (n n) (t t))))
(origs (t (2 1)) (k (0 2)) (n (0 0))))
(defskeleton attest-door
(vars (k skey) (n t text) (p a d akey))
(defstrand person 5 (k k) (n n) (t t) (d d) (p p) (a a))
(defstrand appraise 2 (n n) (d d) (p p) (a a))
(defstrand squealer 2 (k k) (d d) (p p))
(precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
(non-orig (invk p) (invk a) (invk d))
(uniq-orig k n)
(operation generalization deleted (2 0))
(traces
((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
((recv (enc (enc k (invk p)) d)) (send k)))
(label 8)
(parent 0)
(realized)
(shape)
(maps ((0) ((p p) (a a) (d d) (k k) (n n) (t t))))
(origs (k (0 2)) (n (0 0))))
(comment "Nothing left to do")
(defprotocol attest-door basic
(defrole appraise
(vars (d p a akey) (n text))
(trace (recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
(comment "The appraiser for the door"))
(defrole person
(vars (d p a akey) (k skey) (n t text))
(trace (send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
(uniq-orig k n)
(comment "Person requesting door entry"))
(defrole door
(vars (d p akey) (k skey) (t text))
(trace (recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))
(uniq-orig t))
(defrole squealer
(vars (d p akey) (k skey))
(trace (recv (enc (enc k (invk p)) d)) (send k))
(comment "Fake door"))
(defrule yes
(forall ((z strd) (a akey))
(implies
(and (p "appraise" z 2) (p "appraise" "a" z a) (non (invk a)))
(exists ((d akey))
(and (p "appraise" "d" z d) (non (invk d))))))
(comment "Appraisal succeeded"))
(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))))
(comment "Door attestations protocol"))
(defskeleton attest-door
(vars (k skey) (t text) (p d akey))
(defstrand door 3 (k k) (t t) (d d) (p p))
(non-orig (invk p) (invk d))
(uniq-orig t)
(comment "Analyze from the door's perspective")
(traces ((recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t)))
(label 9)
(unrealized (0 0))
(origs (t (0 1)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton attest-door
(vars (k skey) (t n text) (p d d-0 a akey))
(defstrand door 3 (k k) (t t) (d d) (p p))
(defstrand person 3 (k k) (n n) (d d-0) (p p) (a a))
(precedes ((1 2) (0 0)))
(non-orig (invk p) (invk d))
(uniq-orig k t n)
(operation encryption-test (added-strand person 3) (enc k (invk p))
(0 0))
(traces ((recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))
((send (enc (enc d-0 n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d-0))))
(label 10)
(parent 9)
(realized)
(shape)
(maps ((0) ((p p) (d d) (k k) (t t))))
(origs (n (1 0)) (k (1 2)) (t (0 1))))
(comment "Nothing left to do")
(defprotocol attest-door-trust basic
(defrole appraise
(vars (d p a akey) (n text))
(trace (recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
(comment "The appraiser for the door"))
(defrole person
(vars (d p a akey) (k skey) (n t text))
(trace (send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
(uniq-orig k n)
(comment "Person requesting door entry"))
(defrole door
(vars (d p akey) (k skey) (t text))
(trace (recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))
(uniq-orig t))
(defrole squealer
(vars (d p akey) (k skey))
(trace (recv (enc (enc k (invk p)) d)) (send k))
(comment "Fake door"))
(defrule yes
(forall ((z strd) (a akey))
(implies
(and (p "appraise" z 2) (p "appraise" "a" z a) (non (invk a)))
(exists ((d akey))
(and (p "appraise" "d" z d) (non (invk d))))))
(comment "Appraisal succeeded"))
(defrule trust
(forall ((z w strd) (d akey))
(implies
(and (p "appraise" z 2) (p "appraise" "d" z d)
(p "squealer" w 2) (p "squealer" "d" w d))
(false)))
(comment "Passing attestation means not a squealer"))
(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))))
(comment "Door attestations protocol with attestation"))
(defskeleton attest-door-trust
(vars (k skey) (n t text) (p a d akey))
(defstrand person 5 (k k) (n n) (t t) (d d) (p p) (a a))
(non-orig (invk p) (invk a))
(uniq-orig k n)
(comment "Analyze from the person's perspective")
(traces
((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t)))
(label 11)
(unrealized (0 1))
(origs (k (0 2)) (n (0 0)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton attest-door-trust
(vars (k skey) (n t text) (p a d akey))
(defstrand person 5 (k k) (n n) (t t) (d d) (p p) (a a))
(defstrand appraise 2 (n n) (d d) (p p) (a a))
(defstrand door 2 (k k) (t t) (d d) (p p))
(precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
(non-orig (invk p) (invk a) (invk d))
(uniq-orig k n t)
(operation nonce-test (contracted (d-0 d) (p-0 p)) k (2 0)
(enc (enc k (invk p)) d))
(traces
((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
((recv (enc (enc k (invk p)) d)) (send (enc t k))))
(label 15)
(parent 11)
(realized)
(shape)
(maps ((0) ((p p) (a a) (d d) (k k) (n n) (t t))))
(origs (t (2 1)) (k (0 2)) (n (0 0))))
(comment "Nothing left to do")
(defprotocol attest-door-trust basic
(defrole appraise
(vars (d p a akey) (n text))
(trace (recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
(comment "The appraiser for the door"))
(defrole person
(vars (d p a akey) (k skey) (n t text))
(trace (send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
(uniq-orig k n)
(comment "Person requesting door entry"))
(defrole door
(vars (d p akey) (k skey) (t text))
(trace (recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))
(uniq-orig t))
(defrole squealer
(vars (d p akey) (k skey))
(trace (recv (enc (enc k (invk p)) d)) (send k))
(comment "Fake door"))
(defrule yes
(forall ((z strd) (a akey))
(implies
(and (p "appraise" z 2) (p "appraise" "a" z a) (non (invk a)))
(exists ((d akey))
(and (p "appraise" "d" z d) (non (invk d))))))
(comment "Appraisal succeeded"))
(defrule trust
(forall ((z w strd) (d akey))
(implies
(and (p "appraise" z 2) (p "appraise" "d" z d)
(p "squealer" w 2) (p "squealer" "d" w d))
(false)))
(comment "Passing attestation means not a squealer"))
(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))))
(comment "Door attestations protocol with attestation"))
(defskeleton attest-door-trust
(vars (k skey) (t text) (p d akey))
(defstrand door 3 (k k) (t t) (d d) (p p))
(non-orig (invk p) (invk d))
(uniq-orig t)
(comment "Analyze from the door's perspective")
(traces ((recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t)))
(label 16)
(unrealized (0 0))
(origs (t (0 1)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton attest-door-trust
(vars (k skey) (t n text) (p d d-0 a akey))
(defstrand door 3 (k k) (t t) (d d) (p p))
(defstrand person 3 (k k) (n n) (d d-0) (p p) (a a))
(precedes ((1 2) (0 0)))
(non-orig (invk p) (invk d))
(uniq-orig k t n)
(operation encryption-test (added-strand person 3) (enc k (invk p))
(0 0))
(traces ((recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))
((send (enc (enc d-0 n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d-0))))
(label 17)
(parent 16)
(realized)
(shape)
(maps ((0) ((p p) (d d) (k k) (t t))))
(origs (n (1 0)) (k (1 2)) (t (0 1))))
(comment "Nothing left to do")
(defprotocol attest-door-trust-attest basic
(defrole appraise
(vars (d p a akey) (n text))
(trace (recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
(comment "The appraiser for the door"))
(defrole person
(vars (d p a akey) (k skey) (n t text))
(trace (send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
(uniq-orig k n)
(comment "Person requesting door entry"))
(defrole door
(vars (d p akey) (k skey) (t text))
(trace (recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))
(uniq-orig t))
(defrole squealer
(vars (d p akey) (k skey))
(trace (recv (enc (enc k (invk p)) d)) (send k))
(comment "Fake door"))
(defrule yes
(forall ((z strd) (a akey))
(implies
(and (p "appraise" z 2) (p "appraise" "a" z a) (non (invk a)))
(exists ((d akey))
(and (p "appraise" "d" z d) (non (invk d))))))
(comment "Appraisal succeeded"))
(defrule trust
(forall ((z w strd) (d akey))
(implies
(and (p "appraise" z 2) (p "appraise" "d" z d)
(p "squealer" w 2) (p "squealer" "d" w d))
(false)))
(comment "Passing attestation means not a squealer"))
(defrule uncompromised-people-choose-uncompromised-appraisers
(forall ((z strd) (a p akey))
(implies
(and (p "person" z 3) (p "person" "p" z p) (p "person" "a" z a)
(non (invk p)))
(non (invk a)))))
(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))))
(comment
"Door attestations protocol with attestation and reliable persons"))
(defskeleton attest-door-trust-attest
(vars (k skey) (n t text) (p a d akey))
(defstrand person 5 (k k) (n n) (t t) (d d) (p p) (a a))
(non-orig (invk p) (invk a))
(uniq-orig k n)
(comment "Analyze from the person's perspective")
(traces
((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t)))
(label 18)
(unrealized (0 1))
(origs (k (0 2)) (n (0 0)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton attest-door-trust-attest
(vars (k skey) (n t text) (p a d akey))
(defstrand person 5 (k k) (n n) (t t) (d d) (p p) (a a))
(defstrand appraise 2 (n n) (d d) (p p) (a a))
(defstrand door 2 (k k) (t t) (d d) (p p))
(precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
(non-orig (invk p) (invk a) (invk d))
(uniq-orig k n t)
(operation nonce-test (contracted (d-0 d) (p-0 p)) k (2 0)
(enc (enc k (invk p)) d))
(traces
((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
((recv (enc (enc k (invk p)) d)) (send (enc t k))))
(label 22)
(parent 18)
(realized)
(shape)
(maps ((0) ((p p) (a a) (d d) (k k) (n n) (t t))))
(origs (t (2 1)) (k (0 2)) (n (0 0))))
(comment "Nothing left to do")
(defprotocol attest-door-trust-attest basic
(defrole appraise
(vars (d p a akey) (n text))
(trace (recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
(comment "The appraiser for the door"))
(defrole person
(vars (d p a akey) (k skey) (n t text))
(trace (send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))
(uniq-orig k n)
(comment "Person requesting door entry"))
(defrole door
(vars (d p akey) (k skey) (t text))
(trace (recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))
(uniq-orig t))
(defrole squealer
(vars (d p akey) (k skey))
(trace (recv (enc (enc k (invk p)) d)) (send k))
(comment "Fake door"))
(defrule yes
(forall ((z strd) (a akey))
(implies
(and (p "appraise" z 2) (p "appraise" "a" z a) (non (invk a)))
(exists ((d akey))
(and (p "appraise" "d" z d) (non (invk d))))))
(comment "Appraisal succeeded"))
(defrule trust
(forall ((z w strd) (d akey))
(implies
(and (p "appraise" z 2) (p "appraise" "d" z d)
(p "squealer" w 2) (p "squealer" "d" w d))
(false)))
(comment "Passing attestation means not a squealer"))
(defrule uncompromised-people-choose-uncompromised-appraisers
(forall ((z strd) (a p akey))
(implies
(and (p "person" z 3) (p "person" "p" z p) (p "person" "a" z a)
(non (invk p)))
(non (invk a)))))
(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))))
(comment
"Door attestations protocol with attestation and reliable persons"))
(defskeleton attest-door-trust-attest
(vars (k skey) (t text) (p d akey))
(defstrand door 3 (k k) (t t) (d d) (p p))
(non-orig (invk p) (invk d))
(uniq-orig t)
(comment "Analyze from the door's perspective")
(traces ((recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t)))
(label 23)
(unrealized (0 0))
(origs (t (0 1)))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton attest-door-trust-attest
(vars (k skey) (t n text) (d p a akey))
(defstrand door 3 (k k) (t t) (d d) (p p))
(defstrand appraise 2 (n n) (d d) (p p) (a a))
(defstrand person 5 (k k) (n n) (t t) (d d) (p p) (a a))
(precedes ((0 1) (2 3)) ((1 1) (2 1)) ((2 0) (1 0)) ((2 2) (0 0))
((2 4) (0 2)))
(non-orig (invk d) (invk p) (invk a))
(uniq-orig k t n)
(operation nonce-test (displaced 1 3 person 5) t (0 2) (enc t k))
(traces ((recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))
((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))
((send (enc (enc d n (invk p)) a)) (recv (enc n a p))
(send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t)))
(label 27)
(parent 23)
(realized)
(shape)
(maps ((0) ((p p) (d d) (k k) (t t))))
(origs (n (2 0)) (k (2 2)) (t (0 1))))
(comment "Nothing left to do")