cpsa-4.4.4: tst/dy_shapes.tst

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

(herald "Example 1.3 from 1983 Dolev-Yao Paper" (bound 12))

(comment "CPSA 4.3.1")

(comment "All input read from tst/dy.lsp")

(comment "Strand count bounded at 12")

(defprotocol dy basic
  (defrole init
    (vars (a b name) (m text))
    (trace (send (enc (enc m (pubk b)) a (pubk b)))
      (recv (enc (enc m (pubk a)) b (pubk a)))))
  (defrole resp
    (vars (a b name) (m mesg))
    (trace (recv (enc (enc m (pubk b)) a (pubk b)))
      (send (enc (enc m (pubk a)) b (pubk a)))))
  (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 dy
  (vars (m text) (a b name))
  (defstrand init 1 (m m) (a a) (b b))
  (deflistener m)
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (traces ((send (enc (enc m (pubk b)) a (pubk b))))
    ((recv m) (send m)))
  (label 0)
  (unrealized (1 0))
  (preskeleton)
  (origs (m (0 0)))
  (comment "Not a skeleton"))

(defskeleton dy
  (vars (m text) (a b a-0 a-1 name))
  (defstrand init 1 (m m) (a a) (b b))
  (deflistener m)
  (defstrand resp 2 (m (cat (enc m (pubk b)) a)) (a a-0) (b b))
  (defstrand resp 2 (m m) (a a-1) (b b))
  (precedes ((0 0) (2 0)) ((2 1) (3 0)) ((3 1) (1 0)))
  (non-orig (privk a) (privk b))
  (uniq-orig m)
  (operation nonce-test (displaced 4 2 resp 2) m (3 0)
    (enc (enc m (pubk b)) a (pubk b)))
  (traces ((send (enc (enc m (pubk b)) a (pubk b)))) ((recv m) (send m))
    ((recv (enc (enc (enc m (pubk b)) a (pubk b)) a-0 (pubk b)))
      (send (enc (enc (enc m (pubk b)) a (pubk a-0)) b (pubk a-0))))
    ((recv (enc (enc m (pubk b)) a-1 (pubk b)))
      (send (enc (enc m (pubk a-1)) b (pubk a-1)))))
  (label 7)
  (parent 0)
  (realized)
  (shape)
  (maps ((0 1) ((a a) (b b) (m m))))
  (origs (m (0 0))))

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

(comment "Step limit exceeded--aborting run")