cpsa-4.4.4: tst/reflect_shapes.tst

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

(herald reflect)

(comment "CPSA 4.3.1")

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

(defprotocol reflect basic
  (defrole init
    (vars (a b akey))
    (trace (send (enc b (invk a))) (recv (enc a (invk b)))))
  (defrole resp
    (vars (a b akey))
    (trace (recv (enc b (invk a))) (send (enc a (invk b)))))
  (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)))))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 1 (a a) (b b))
  (non-orig (invk a) (invk b))
  (traces ((recv (enc b (invk a)))))
  (label 0)
  (unrealized (0 0))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 1 (a a) (b b))
  (defstrand init 1 (a a) (b b))
  (precedes ((1 0) (0 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand init 1) (enc b (invk a))
    (0 0))
  (traces ((recv (enc b (invk a)))) ((send (enc b (invk a)))))
  (label 1)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b))))
  (origs))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 1 (a a) (b b))
  (defstrand resp 2 (a b) (b a))
  (defstrand init 1 (a b) (b a))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand init 1) (enc a (invk b))
    (1 0))
  (traces ((recv (enc b (invk a))))
    ((recv (enc a (invk b))) (send (enc b (invk a))))
    ((send (enc a (invk b)))))
  (label 3)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b))))
  (origs))

(comment "Nothing left to do")

(defprotocol reflect basic
  (defrole init
    (vars (a b akey))
    (trace (send (enc b (invk a))) (recv (enc a (invk b)))))
  (defrole resp
    (vars (a b akey))
    (trace (recv (enc b (invk a))) (send (enc a (invk b)))))
  (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)))))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (non-orig (invk a) (invk b))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b)))))
  (label 8)
  (unrealized (0 1))
  (origs)
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton reflect
  (vars (b akey))
  (defstrand init 2 (a b) (b b))
  (non-orig (invk b))
  (operation encryption-test (displaced 1 0 init 1) (enc a (invk b))
    (0 1))
  (traces ((send (enc b (invk b))) (recv (enc b (invk b)))))
  (label 9)
  (parent 8)
  (realized)
  (shape)
  (maps ((0) ((a b) (b b))))
  (origs))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (defstrand init 1 (a b) (b a))
  (precedes ((1 0) (0 1)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand init 1) (enc a (invk b))
    (0 1))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b))))
    ((send (enc a (invk b)))))
  (label 10)
  (parent 8)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b))))
  (origs))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (defstrand resp 2 (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (displaced 2 0 init 1) (enc b (invk a))
    (1 0))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b))))
    ((recv (enc b (invk a))) (send (enc a (invk b)))))
  (label 12)
  (parent 8)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b))))
  (origs))

(defskeleton reflect
  (vars (a b akey))
  (defstrand init 2 (a a) (b b))
  (defstrand resp 2 (a a) (b b))
  (defstrand init 1 (a a) (b b))
  (precedes ((1 1) (0 1)) ((2 0) (1 0)))
  (non-orig (invk a) (invk b))
  (operation encryption-test (added-strand init 1) (enc b (invk a))
    (1 0))
  (traces ((send (enc b (invk a))) (recv (enc a (invk b))))
    ((recv (enc b (invk a))) (send (enc a (invk b))))
    ((send (enc b (invk a)))))
  (label 13)
  (parent 8)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b))))
  (origs))

(comment "Nothing left to do")

(defprotocol reflect basic
  (defrole init
    (vars (a b akey))
    (trace (send (enc b (invk a))) (recv (enc a (invk b)))))
  (defrole resp
    (vars (a b akey))
    (trace (recv (enc b (invk a))) (send (enc a (invk b)))))
  (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)))))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 1 (a a) (b (invk b)))
  (non-orig b (invk a))
  (traces ((recv (enc (invk b) (invk a)))))
  (label 19)
  (unrealized (0 0))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton reflect
  (vars (a b akey))
  (defstrand resp 1 (a a) (b (invk b)))
  (defstrand init 1 (a a) (b (invk b)))
  (precedes ((1 0) (0 0)))
  (non-orig b (invk a))
  (operation encryption-test (added-strand init 1)
    (enc (invk b) (invk a)) (0 0))
  (traces ((recv (enc (invk b) (invk a))))
    ((send (enc (invk b) (invk a)))))
  (label 20)
  (parent 19)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b))))
  (origs))

(defskeleton reflect
  (vars (a a-0 akey))
  (defstrand resp 1 (a a) (b a-0))
  (defstrand resp 2 (a a-0) (b a))
  (defstrand init 1 (a a-0) (b a))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig (invk a) (invk a-0))
  (operation encryption-test (added-strand init 1) (enc a (invk a-0))
    (1 0))
  (traces ((recv (enc a-0 (invk a))))
    ((recv (enc a (invk a-0))) (send (enc a-0 (invk a))))
    ((send (enc a (invk a-0)))))
  (label 22)
  (parent 19)
  (realized)
  (shape)
  (maps ((0) ((a a) (b (invk a-0)))))
  (origs))

(comment "Nothing left to do")