cpsa-4.4.4: tst/ns-l_shapes.tst

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

(herald "Needham-Schroeder-Low Public-Key Protocol"
  (comment "With deflistener's"))

(comment "CPSA 4.3.1")

(comment "All input read from tst/ns-l.scm")

(defprotocol ns basic
  (defrole init
    (vars (a b name) (n1 n2 text))
    (trace (send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))
      (send (enc n2 (pubk b)))))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc b n1 n2 (pubk a)))
      (recv (enc n2 (pubk 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))))
  (comment "Needham-Schroeder"))

(defskeleton ns
  (vars (n1 n2 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (deflistener n1)
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (comment "Initiator point-of-view with a listener")
  (traces
    ((send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))
      (send (enc n2 (pubk b)))) ((recv n1) (send n1)))
  (label 0)
  (unrealized (0 1) (1 0))
  (preskeleton)
  (origs (n1 (0 0)))
  (comment "Not a skeleton"))

(comment "Nothing left to do")

(defprotocol ns basic
  (defrole init
    (vars (a b name) (n1 n2 text))
    (trace (send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))
      (send (enc n2 (pubk b)))))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc b n1 n2 (pubk a)))
      (recv (enc n2 (pubk 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))))
  (comment "Needham-Schroeder"))

(defskeleton ns
  (vars (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (deflistener n2)
  (non-orig (privk a))
  (uniq-orig n2)
  (comment "Responder point-of-view with a listener")
  (traces
    ((recv (enc n1 a (pubk b))) (send (enc b n1 n2 (pubk a)))
      (recv (enc n2 (pubk b)))) ((recv n2) (send n2)))
  (label 5)
  (unrealized (0 2) (1 0))
  (preskeleton)
  (origs (n2 (0 1)))
  (comment "Not a skeleton"))

(defskeleton ns
  (vars (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (deflistener n2)
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (precedes ((0 1) (2 1)) ((2 2) (0 2)) ((2 2) (1 0)))
  (non-orig (privk a))
  (uniq-orig n2)
  (operation nonce-test (displaced 3 2 init 3) n2 (0 2)
    (enc b n1 n2 (pubk a)))
  (traces
    ((recv (enc n1 a (pubk b))) (send (enc b n1 n2 (pubk a)))
      (recv (enc n2 (pubk b)))) ((recv n2) (send n2))
    ((send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))
      (send (enc n2 (pubk b)))))
  (label 8)
  (parent 5)
  (realized)
  (shape)
  (maps ((0 1) ((a a) (n2 n2) (b b) (n1 n1))))
  (origs (n2 (0 1))))

(defskeleton ns
  (vars (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (deflistener n2)
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (precedes ((0 1) (2 1)) ((0 1) (3 1)) ((2 2) (1 0)) ((3 2) (0 2)))
  (non-orig (privk a))
  (uniq-orig n2)
  (operation nonce-test (added-strand init 3) n2 (0 2)
    (enc b n1 n2 (pubk a)))
  (traces
    ((recv (enc n1 a (pubk b))) (send (enc b n1 n2 (pubk a)))
      (recv (enc n2 (pubk b)))) ((recv n2) (send n2))
    ((send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))
      (send (enc n2 (pubk b))))
    ((send (enc n1 a (pubk b))) (recv (enc b n1 n2 (pubk a)))
      (send (enc n2 (pubk b)))))
  (label 9)
  (parent 5)
  (realized)
  (shape)
  (maps ((0 1) ((a a) (n2 n2) (b b) (n1 n1))))
  (origs (n2 (0 1))))

(comment "Nothing left to do")