cpsa-2.2.2: tst/blanchet.tst

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

(comment "CPSA 2.2.2")
(comment "All input read")

(defprotocol blanchet basic
  (defrole init
    (vars (a b name) (s skey) (d text))
    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d text))
    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (non-orig (privk a) (privk b))
  (uniq-orig s)
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))
  (label 0)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton blanchet
  (vars (d text) (a b a-0 b-0 name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (defstrand resp 2 (d d) (a a-0) (b b-0) (s s))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig s)
  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv (enc (enc s (privk a-0)) (pubk b-0))) (send (enc d s))))
  (label 1)
  (parent 0)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (deflistener s)
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig s)
  (operation encryption-test (added-listener s) (enc d s) (0 1))
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv s) (send s)))
  (label 2)
  (parent 0)
  (unrealized (1 0))
  (comment "empty cohort"))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (defstrand resp 2 (d d) (a a) (b b) (s s))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (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 1)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol blanchet basic
  (defrole init
    (vars (a b name) (s skey) (d text))
    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d text))
    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (non-orig (privk a) (privk b))
  (uniq-orig d s)
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv d) (send d)))
  (label 4)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton blanchet
  (vars (d text) (a b a-0 b-0 name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (defstrand resp 2 (d d) (a a-0) (b b-0) (s s))
  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig d s)
  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv d) (send d))
    ((recv (enc (enc s (privk a-0)) (pubk b-0))) (send (enc d s))))
  (label 5)
  (parent 4)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (deflistener s)
  (precedes ((0 0) (2 0)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig d s)
  (operation encryption-test (added-listener s) (enc d s) (0 1))
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv d) (send d)) ((recv s) (send s)))
  (label 6)
  (parent 4)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (defstrand resp 2 (d d) (a a) (b b) (s s))
  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig d s)
  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (2 0)
    (enc (enc s (privk a)) (pubk b)))
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv d) (send d))
    ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))
  (label 7)
  (parent 5)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (defstrand resp 2 (d d) (a a) (b b) (s s))
  (deflistener s)
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((2 1) (0 1)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig d s)
  (operation nonce-test (added-listener s) d (1 0) (enc d s))
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv d) (send d))
    ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))
    ((recv s) (send s)))
  (label 8)
  (parent 7)
  (unrealized (3 0))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol blanchet basic
  (defrole init
    (vars (a b name) (s skey) (d text))
    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d text))
    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))))

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

(defskeleton blanchet
  (vars (d text) (a b b-0 name) (s skey))
  (defstrand resp 2 (d d) (a a) (b b) (s s))
  (defstrand init 1 (a a) (b b-0) (s s))
  (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)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol blanchet basic
  (defrole init
    (vars (a b name) (s skey) (d text))
    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d text))
    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand resp 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (non-orig (privk a) (privk b))
  (uniq-orig d s)
  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))
    ((recv d) (send d)))
  (label 11)
  (unrealized (0 0) (1 0)))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand resp 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (precedes ((0 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig d s)
  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))
    ((recv d) (send d)))
  (label 12)
  (parent 11)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton blanchet
  (vars (d text) (a b b-0 name) (s skey))
  (defstrand resp 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (defstrand init 1 (a a) (b b-0) (s s))
  (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 12)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol blanchet basic
  (defrole init
    (vars (a b name) (s skey) (d text))
    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d text))
    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand resp 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (non-orig (privk a))
  (uniq-orig d s)
  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))
    ((recv d) (send d)))
  (label 14)
  (unrealized (0 0) (1 0)))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand resp 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (precedes ((0 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig d s)
  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))
    ((recv d) (send d)))
  (label 15)
  (parent 14)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton blanchet
  (vars (d text) (a b b-0 name) (s skey))
  (defstrand resp 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (defstrand init 1 (a a) (b b-0) (s s))
  (precedes ((0 1) (1 0)) ((2 0) (0 0)))
  (non-orig (privk a))
  (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 16)
  (parent 15)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol blanchet basic
  (defrole init
    (vars (a b name) (s skey) (d text))
    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))
  (defrole resp
    (vars (a b name) (s skey) (d text))
    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (non-orig (privk b))
  (uniq-orig d s)
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv d) (send d)))
  (label 17)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton blanchet
  (vars (d text) (a b a-0 b-0 name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (defstrand resp 2 (d d) (a a-0) (b b-0) (s s))
  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk b))
  (uniq-orig d s)
  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv d) (send d))
    ((recv (enc (enc s (privk a-0)) (pubk b-0))) (send (enc d s))))
  (label 18)
  (parent 17)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (deflistener s)
  (precedes ((0 0) (2 0)) ((2 1) (0 1)))
  (non-orig (privk b))
  (uniq-orig d s)
  (operation encryption-test (added-listener s) (enc d s) (0 1))
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv d) (send d)) ((recv s) (send s)))
  (label 19)
  (parent 17)
  (unrealized (2 0))
  (comment "empty cohort"))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (defstrand resp 2 (d d) (a a) (b b) (s s))
  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk b))
  (uniq-orig d s)
  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (2 0)
    (enc (enc s (privk a)) (pubk b)))
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv d) (send d))
    ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))
  (label 20)
  (parent 18)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton blanchet
  (vars (d text) (a b name) (s skey))
  (defstrand init 2 (d d) (a a) (b b) (s s))
  (deflistener d)
  (defstrand resp 2 (d d) (a a) (b b) (s s))
  (deflistener s)
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((2 1) (0 1)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk b))
  (uniq-orig d s)
  (operation nonce-test (added-listener s) d (1 0) (enc d s))
  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))
    ((recv d) (send d))
    ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))
    ((recv s) (send s)))
  (label 21)
  (parent 20)
  (unrealized (3 0))
  (comment "empty cohort"))

(comment "Nothing left to do")