cpsa-4.4.4: tst/crushing_shapes.tst

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

(comment "CPSA 4.3.1")

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

(defprotocol crushing basic
  (defrole init
    (vars (k akey) (n n1 n2 n3 text))
    (trace (send (enc n k)) (recv (enc n n1 (invk k)))
      (recv (enc n n2 (invk k))) (recv (enc n n3 (invk k)))
      (send (enc n n1 n2 n3 (invk k)))
      (recv (enc n n1 n2 n3 n (invk k))))
    (non-orig (invk k))
    (uniq-orig n))
  (defrole adder
    (vars (k akey) (n new text))
    (trace (recv (enc n k)) (send (enc n new (invk k))))
    (uniq-orig new))
  (defrole twister
    (vars (k akey) (n n1 n2 n3 text))
    (trace (recv (enc n n1 n2 n3 (invk k)))
      (send (enc n n2 n3 n1 n (invk k)))))
  (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 crushing
  (vars (n n1 n2 n3 text) (k akey))
  (defstrand init 6 (n n) (n1 n1) (n2 n2) (n3 n3) (k k))
  (non-orig (invk k))
  (uniq-orig n n1 n2 n3)
  (traces
    ((send (enc n k)) (recv (enc n n1 (invk k)))
      (recv (enc n n2 (invk k))) (recv (enc n n3 (invk k)))
      (send (enc n n1 n2 n3 (invk k)))
      (recv (enc n n1 n2 n3 n (invk k)))))
  (label 0)
  (unrealized (0 1) (0 2) (0 3) (0 5))
  (origs (n (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton crushing
  (vars (n n1 text) (k akey))
  (defstrand init 6 (n n) (n1 n1) (n2 n1) (n3 n1) (k k))
  (defstrand adder 2 (n n) (new n1) (k k))
  (defstrand twister 2 (n n) (n1 n1) (n2 n1) (n3 n1) (k k))
  (precedes ((0 0) (1 0)) ((0 4) (2 0)) ((1 1) (0 1)) ((2 1) (0 5)))
  (non-orig (invk k))
  (uniq-orig n n1)
  (operation encryption-test (displaced 3 0 init 5)
    (enc n n1 n1 n1 (invk k)) (2 0))
  (traces
    ((send (enc n k)) (recv (enc n n1 (invk k)))
      (recv (enc n n1 (invk k))) (recv (enc n n1 (invk k)))
      (send (enc n n1 n1 n1 (invk k)))
      (recv (enc n n1 n1 n1 n (invk k))))
    ((recv (enc n k)) (send (enc n n1 (invk k))))
    ((recv (enc n n1 n1 n1 (invk k)))
      (send (enc n n1 n1 n1 n (invk k)))))
  (label 14)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((k k) (n n) (n1 n1) (n2 n1) (n3 n1))))
  (origs (n (0 0)) (n1 (1 1))))

(comment "Nothing left to do")