cpsa-4.4.4: tst/blanchet_shapes.tst

(comment "CPSA 4.3.1")
(comment "Extracted shapes")

(herald "Blanchet's Simple Example Protocol"
  (comment "There is a flaw in this protocol by design"))

(comment "CPSA 4.3.1")

(comment "All input read from tst/blanchet.scm")

(defprotocol blanchet basic
  (defrole init
    (vars (a b name) (s skey) (d data))
    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d data))
    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))
  (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 "Blanchet's protocol using named asymmetric keys"))

(defskeleton blanchet
  (vars (d data) (s skey) (a b name))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (non-orig (privk b))
  (uniq-orig s)
  (comment "Analyze from the initiator's perspective")
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))
  (label 0)
  (unrealized (0 1))
  (origs (s (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton blanchet
  (vars (d data) (s skey) (a b name))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk b))
  (uniq-orig s)
  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (1 0)
    (enc (enc s (privk a)) (pubk b)))
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))
  (label 3)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (d d))))
  (origs (s (0 0))))

(comment "Nothing left to do")

(defprotocol blanchet basic
  (defrole init
    (vars (a b name) (s skey) (d data))
    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d data))
    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))
  (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 "Blanchet's protocol using named asymmetric keys"))

(defskeleton blanchet
  (vars (d data) (s skey) (a b name))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (non-orig (privk b))
  (uniq-orig d s)
  (comment "From the initiator's perspective, is the secret leaked?")
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv d) (send d)))
  (label 4)
  (unrealized (0 1))
  (origs (s (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

(comment "Nothing left to do")

(defprotocol blanchet basic
  (defrole init
    (vars (a b name) (s skey) (d data))
    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d data))
    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))
  (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 "Blanchet's protocol using named asymmetric keys"))

(defskeleton blanchet
  (vars (d data) (s skey) (a b name))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (non-orig (privk a) (privk b))
  (uniq-orig s)
  (comment "Analyze from the responder's perspective")
  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))
  (label 9)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton blanchet
  (vars (d data) (s skey) (a b b-0 name))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (defstrand init 1 (s s) (a a) (b b-0))
  (precedes ((1 0) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig s)
  (operation encryption-test (added-strand init 1) (enc s (privk a))
    (0 0))
  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))
    ((send (enc (enc s (privk a)) (pubk b-0)))))
  (label 10)
  (parent 9)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (d d))))
  (origs (s (1 0))))

(comment "Nothing left to do")

(defprotocol blanchet basic
  (defrole init
    (vars (a b name) (s skey) (d data))
    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d data))
    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))
  (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 "Blanchet's protocol using named asymmetric keys"))

(defskeleton blanchet
  (vars (d data) (s skey) (a b name))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (non-orig (privk a) (privk b))
  (uniq-orig d s)
  (comment "From the responders's perspective, is the secret leaked?")
  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))
    ((recv d) (send d)))
  (label 11)
  (unrealized (0 0) (1 0))
  (preskeleton)
  (origs (d (0 1)))
  (comment "Not a skeleton"))

(defskeleton blanchet
  (vars (d data) (s skey) (a b b-0 name))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (defstrand init 1 (s s) (a a) (b b-0))
  (precedes ((0 1) (1 0)) ((2 0) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig d s)
  (operation encryption-test (added-strand init 1) (enc s (privk a))
    (0 0))
  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))
    ((recv d) (send d)) ((send (enc (enc s (privk a)) (pubk b-0)))))
  (label 13)
  (parent 11)
  (realized)
  (shape)
  (maps ((0 1) ((a a) (b b) (s s) (d d))))
  (origs (s (2 0)) (d (0 1))))

(comment "Nothing left to do")

(defprotocol blanchet-akey basic
  (defrole init
    (vars (a b akey) (s skey) (d data))
    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s))))
  (defrole resp
    (vars (a b akey) (s skey) (d data))
    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))
  (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 "Blanchet's protocol using unnamed asymmetric keys"))

(defskeleton blanchet-akey
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (non-orig (invk b))
  (uniq-orig s)
  (comment "Analyze from the initiator's perspective")
  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s))))
  (label 14)
  (unrealized (0 1))
  (origs (s (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton blanchet-akey
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk b))
  (uniq-orig s)
  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (1 0)
    (enc (enc s (invk a)) b))
  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))
    ((recv (enc (enc s (invk a)) b)) (send (enc d s))))
  (label 17)
  (parent 14)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (d d))))
  (origs (s (0 0))))

(comment "Nothing left to do")

(defprotocol blanchet-akey basic
  (defrole init
    (vars (a b akey) (s skey) (d data))
    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s))))
  (defrole resp
    (vars (a b akey) (s skey) (d data))
    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))
  (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 "Blanchet's protocol using unnamed asymmetric keys"))

(defskeleton blanchet-akey
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (non-orig (invk b))
  (uniq-orig d s)
  (comment "From the initiator's perspective, is the secret leaked?")
  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))
    ((recv d) (send d)))
  (label 18)
  (unrealized (0 1))
  (origs (s (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

(comment "Nothing left to do")

(defprotocol blanchet-akey basic
  (defrole init
    (vars (a b akey) (s skey) (d data))
    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s))))
  (defrole resp
    (vars (a b akey) (s skey) (d data))
    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))
  (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 "Blanchet's protocol using unnamed asymmetric keys"))

(defskeleton blanchet-akey
  (vars (d data) (s skey) (a b akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (non-orig (invk a) (invk b))
  (uniq-orig s)
  (comment "Analyze from the responder's perspective")
  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s))))
  (label 23)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton blanchet-akey
  (vars (d data) (s skey) (a b b-0 akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (defstrand init 1 (s s) (a a) (b b-0))
  (precedes ((1 0) (0 0)))
  (non-orig (invk a) (invk b))
  (uniq-orig s)
  (operation encryption-test (added-strand init 1) (enc s (invk a))
    (0 0))
  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s)))
    ((send (enc (enc s (invk a)) b-0))))
  (label 24)
  (parent 23)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (d d))))
  (origs (s (1 0))))

(comment "Nothing left to do")

(defprotocol blanchet-akey basic
  (defrole init
    (vars (a b akey) (s skey) (d data))
    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s))))
  (defrole resp
    (vars (a b akey) (s skey) (d data))
    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))
  (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 "Blanchet's protocol using unnamed asymmetric keys"))

(defskeleton blanchet-akey
  (vars (d data) (s skey) (a b akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (non-orig (invk a) (invk b))
  (uniq-orig d s)
  (comment "From the responders's perspective, is the secret leaked?")
  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s)))
    ((recv d) (send d)))
  (label 25)
  (unrealized (0 0) (1 0))
  (preskeleton)
  (origs (d (0 1)))
  (comment "Not a skeleton"))

(defskeleton blanchet-akey
  (vars (d data) (s skey) (a b b-0 akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (defstrand init 1 (s s) (a a) (b b-0))
  (precedes ((0 1) (1 0)) ((2 0) (0 0)))
  (non-orig (invk a) (invk b))
  (uniq-orig d s)
  (operation encryption-test (added-strand init 1) (enc s (invk a))
    (0 0))
  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s)))
    ((recv d) (send d)) ((send (enc (enc s (invk a)) b-0))))
  (label 27)
  (parent 25)
  (realized)
  (shape)
  (maps ((0 1) ((a a) (b b) (s s) (d d))))
  (origs (s (2 0)) (d (0 1))))

(comment "Nothing left to do")

(defprotocol blanchet-fixed basic
  (defrole init
    (vars (a b name) (s skey) (d data))
    (trace (send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d data))
    (trace (recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))
  (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 "Fixed Blanchet's protocol using named asymmetric keys"))

(defskeleton blanchet-fixed
  (vars (d data) (s skey) (a b name))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (non-orig (privk b))
  (uniq-orig s)
  (comment "Analyze from the initiator's perspective")
  (traces ((send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s))))
  (label 28)
  (unrealized (0 1))
  (origs (s (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton blanchet-fixed
  (vars (d data) (s skey) (a b name))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk b))
  (uniq-orig s)
  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (1 0)
    (enc (enc s b (privk a)) (pubk b)))
  (traces ((send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s)))
    ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))
  (label 31)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (d d))))
  (origs (s (0 0))))

(comment "Nothing left to do")

(defprotocol blanchet-fixed basic
  (defrole init
    (vars (a b name) (s skey) (d data))
    (trace (send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d data))
    (trace (recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))
  (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 "Fixed Blanchet's protocol using named asymmetric keys"))

(defskeleton blanchet-fixed
  (vars (d data) (s skey) (a b name))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (non-orig (privk b))
  (uniq-orig d s)
  (comment "From the initiator's perspective, is the secret leaked?")
  (traces ((send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s)))
    ((recv d) (send d)))
  (label 32)
  (unrealized (0 1))
  (origs (s (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

(comment "Nothing left to do")

(defprotocol blanchet-fixed basic
  (defrole init
    (vars (a b name) (s skey) (d data))
    (trace (send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d data))
    (trace (recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))
  (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 "Fixed Blanchet's protocol using named asymmetric keys"))

(defskeleton blanchet-fixed
  (vars (d data) (s skey) (a b name))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (non-orig (privk a) (privk b))
  (uniq-orig s)
  (comment "Analyze from the responder's perspective")
  (traces ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))
  (label 37)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton blanchet-fixed
  (vars (d data) (s skey) (a b name))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (defstrand init 1 (s s) (a a) (b b))
  (precedes ((1 0) (0 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig s)
  (operation encryption-test (added-strand init 1) (enc s b (privk a))
    (0 0))
  (traces ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s)))
    ((send (enc (enc s b (privk a)) (pubk b)))))
  (label 38)
  (parent 37)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (d d))))
  (origs (s (1 0))))

(comment "Nothing left to do")

(defprotocol blanchet-fixed basic
  (defrole init
    (vars (a b name) (s skey) (d data))
    (trace (send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d data))
    (trace (recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))
  (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 "Fixed Blanchet's protocol using named asymmetric keys"))

(defskeleton blanchet-fixed
  (vars (d data) (s skey) (a b name))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (non-orig (privk a) (privk b))
  (uniq-orig d s)
  (comment "From the responders's perspective, is the secret leaked?")
  (traces ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s)))
    ((recv d) (send d)))
  (label 39)
  (unrealized (0 0) (1 0))
  (preskeleton)
  (origs (d (0 1)))
  (comment "Not a skeleton"))

(comment "Nothing left to do")