cpsa-4.4.4: tst/bug_example_shapes.tst

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

(herald bug_example (bound 20))

(comment "CPSA 4.3.1")

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

(comment "Strand count bounded at 20")

(defprotocol bug_example basic
  (defrole init
    (vars (x y akey))
    (trace (send (enc y (hash x (invk y)))))
    (non-orig (invk x) (invk y)))
  (defrole resp
    (vars (x y akey))
    (trace (recv (enc y (hash (invk x) y))))
    (non-orig (invk x) (invk y)))
  (defrole flip
    (vars (k k1 k2 akey))
    (trace (recv (enc k (hash k1 k2)))
      (send (enc k (hash (invk k1) (invk k2))))))
  (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 bug_example
  (vars (x y akey))
  (defstrand resp 1 (x x) (y y))
  (non-orig (invk x) (invk y))
  (traces ((recv (enc y (hash (invk x) y)))))
  (label 0)
  (unrealized (0 0))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton bug_example
  (vars (x k2 akey))
  (defstrand resp 1 (x x) (y (invk k2)))
  (defstrand flip 2 (k (invk k2)) (k1 x) (k2 k2))
  (defstrand init 1 (x x) (y (invk k2)))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig k2 (invk x))
  (operation encryption-test (added-strand init 1)
    (enc (invk k2) (hash x k2)) (1 0))
  (traces ((recv (enc (invk k2) (hash (invk x) (invk k2)))))
    ((recv (enc (invk k2) (hash x k2)))
      (send (enc (invk k2) (hash (invk x) (invk k2)))))
    ((send (enc (invk k2) (hash x k2)))))
  (label 3)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((x x) (y (invk k2)))))
  (origs))

(comment "Nothing left to do")

(defprotocol bug_example basic
  (defrole init
    (vars (x y akey))
    (trace (send (enc y (hash x (invk y)))))
    (non-orig (invk x) (invk y)))
  (defrole resp
    (vars (x y akey))
    (trace (recv (enc y (hash (invk x) y))))
    (non-orig (invk x) (invk y)))
  (defrole flip1
    (vars (k k1 k2 akey))
    (trace (recv (enc k (hash (invk k1) k2)))
      (send (enc k (hash k1 (invk k2))))))
  (defrole flip2
    (vars (k k1 k2 akey))
    (trace (recv (enc k (hash k1 (invk k2))))
      (send (enc k (hash (invk k1) k2)))))
  (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 bug_example
  (vars (x y akey))
  (defstrand resp 1 (x x) (y y))
  (non-orig (invk x) (invk y))
  (traces ((recv (enc y (hash (invk x) y)))))
  (label 8)
  (unrealized (0 0))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton bug_example
  (vars (x y akey))
  (defstrand resp 1 (x x) (y y))
  (defstrand flip2 2 (k y) (k1 x) (k2 y))
  (defstrand init 1 (x x) (y y))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig (invk x) (invk y))
  (operation encryption-test (added-strand init 1)
    (enc y (hash x (invk y))) (1 0))
  (traces ((recv (enc y (hash (invk x) y))))
    ((recv (enc y (hash x (invk y)))) (send (enc y (hash (invk x) y))))
    ((send (enc y (hash x (invk y))))))
  (label 11)
  (parent 8)
  (realized)
  (shape)
  (maps ((0) ((x x) (y y))))
  (origs))

(comment "Nothing left to do")