cpsa-4.4.4: tst/thisthat_shapes.tst

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

(herald "Needham-Schroeder Public-Key Protocol This-That Variant")

(comment "CPSA 4.3.1")

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

(defprotocol thisthat basic
  (defrole init
    (vars (a b name) (n1 n2 n3 text))
    (trace (send (enc n1 a (pubk b)))
      (recv (cat (enc n1 n2 (pubk a)) (enc n1 n3 (pubk a))))
      (recv (cat (enc "this" n2 (pubk b)) (enc "that" n3 (pubk b))))))
  (defrole this
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
      (send (enc "this" n2 (pubk b))))
    (uniq-orig n2))
  (defrole that
    (vars (b a name) (n3 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n3 (pubk a)))
      (send (enc "that" n3 (pubk b))))
    (uniq-orig n3))
  (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 thisthat
  (vars (n1 n2 n3 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (n3 n3) (a a) (b b))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (comment "Initiator point-of-view")
  (traces
    ((send (enc n1 a (pubk b)))
      (recv (cat (enc n1 n2 (pubk a)) (enc n1 n3 (pubk a))))
      (recv (cat (enc "this" n2 (pubk b)) (enc "that" n3 (pubk b))))))
  (label 0)
  (unrealized (0 1))
  (origs (n1 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton thisthat
  (vars (n1 n3 n3-0 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n3-0) (n3 n3) (a a) (b b))
  (defstrand that 3 (n3 n3) (n1 n1) (b b) (a a))
  (defstrand this 3 (n2 n3-0) (n1 n1) (b b) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((1 2) (0 2))
    ((2 1) (0 1)) ((2 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig n1 n3 n3-0)
  (operation nonce-test (displaced 1 3 this 3) n3-0 (0 2)
    (enc n1 n3-0 (pubk a)))
  (traces
    ((send (enc n1 a (pubk b)))
      (recv (cat (enc n1 n3-0 (pubk a)) (enc n1 n3 (pubk a))))
      (recv (cat (enc "this" n3-0 (pubk b)) (enc "that" n3 (pubk b)))))
    ((recv (enc n1 a (pubk b))) (send (enc n1 n3 (pubk a)))
      (send (enc "that" n3 (pubk b))))
    ((recv (enc n1 a (pubk b))) (send (enc n1 n3-0 (pubk a)))
      (send (enc "this" n3-0 (pubk b)))))
  (label 15)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (n1 n1) (n2 n3-0) (n3 n3))))
  (origs (n3-0 (2 1)) (n3 (1 1)) (n1 (0 0))))

(comment "Nothing left to do")