cpsa-4.4.4: tst/ns-rebinding_shapes.tst

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

(herald "ALternate Needham-Schroeder Public-Key Protocol Variants")

(comment "CPSA 4.3.1")

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

(defprotocol ns basic
  (defrole init
    (vars (a b name) (n1 n2 text))
    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    (facts (rel1 n1 n2) (rel2 n1 n2)))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b)))))
  (defrule rebind-x
    (forall ((x y text))
      (implies
        (fact rel1 x y)
        (exists ((x-0 name)) (fact rel2 x-0 y)))))
  (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))))
  (defgenrule fact-init-rel11
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel1 n1 n2))))
  (defgenrule fact-init-rel20
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel2 n1 n2))))
  (comment "Needham-Schroeder with no role origination assumptions"))

(defskeleton ns
  (vars (n1 n2 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (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 (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b)))))
  (label 0)
  (unrealized (0 1))
  (origs (n1 (0 0)))
  (comment "Not closed under rules"))

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

(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 n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    (facts (rel1 n1 n2) (rel2 n1 n2)))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b)))))
  (defrule rebind-x
    (forall ((x y text))
      (implies
        (fact rel1 x y)
        (exists ((x-0 name)) (fact rel2 x-0 y)))))
  (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))))
  (defgenrule fact-init-rel11
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel1 n1 n2))))
  (defgenrule fact-init-rel20
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel2 n1 n2))))
  (comment "Needham-Schroeder with no role origination assumptions"))

(defskeleton ns
  (vars (n1 n2 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (facts (rel n1 n1))
  (comment "Initiator point-of-view")
  (traces
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b)))))
  (label 4)
  (unrealized (0 1))
  (origs (n1 (0 0)))
  (comment "Not closed under rules"))

(defskeleton ns
  (vars (x name) (n1 n2 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (facts (rel2 x n2) (rel1 n1 n2) (rel2 n1 n2) (rel n1 n1))
  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
    (enc n1 a (pubk b)) (enc n1 n2 b (pubk a)))
  (traces
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))))
  (label 7)
  (parent 4)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
  (origs (n1 (0 0))))

(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 n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    (facts (rel1 n1 n2) (rel2 n1 n2)))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b)))))
  (defrule rebind-x
    (forall ((x y text))
      (implies
        (fact rel1 x y)
        (exists ((x-0 name)) (fact rel2 x-0 y)))))
  (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))))
  (defgenrule fact-init-rel11
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel1 n1 n2))))
  (defgenrule fact-init-rel20
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel2 n1 n2))))
  (comment "Needham-Schroeder with no role origination assumptions"))

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

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

(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 n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    (facts (rel1 n1 n2) (rel2 n1 n2)))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b)))))
  (defrule rebind-x
    (forall ((x y text))
      (implies
        (fact rel1 x y)
        (exists ((x-0 name)) (fact rel2 x-0 y)))))
  (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))))
  (defgenrule fact-init-rel11
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel1 n1 n2))))
  (defgenrule fact-init-rel20
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel2 n1 n2))))
  (comment "Needham-Schroeder with no role origination assumptions"))

(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")
  (traces
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b)))) ((recv n1) (send n1)))
  (label 11)
  (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 n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    (facts (rel1 n1 n2) (rel2 n1 n2)))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b)))))
  (defrule rebind-x
    (forall ((x y text))
      (implies
        (fact rel1 x y)
        (exists ((x-0 name)) (fact rel2 x-0 y)))))
  (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))))
  (defgenrule fact-init-rel11
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel1 n1 n2))))
  (defgenrule fact-init-rel20
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel2 n1 n2))))
  (comment "Needham-Schroeder with no role origination assumptions"))

(defskeleton ns
  (vars (n1 n1-0 n2 n2-0 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))
  (non-orig (privk a) (privk b))
  (uniq-orig n1 n1-0)
  (comment "Double initiator point-of-view")
  (traces
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 b (pubk a)))
      (send (enc n2-0 (pubk b)))))
  (label 17)
  (unrealized (0 1) (1 1))
  (origs (n1 (0 0)) (n1-0 (1 0)))
  (comment "Not closed under rules"))

(defskeleton ns
  (vars (x x-0 name) (n1 n2 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (facts (rel2 x-0 n2) (rel2 x n2) (rel1 n1 n2) (rel2 n1 n2))
  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
    (enc n1 a (pubk b)) (enc n1 n2 b (pubk a)))
  (traces
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))))
  (label 23)
  (parent 17)
  (realized)
  (shape)
  (maps ((0 0) ((a a) (b b) (n1 n1) (n1-0 n1) (n2 n2) (n2-0 n2))))
  (origs (n1 (0 0))))

(defskeleton ns
  (vars (x x-0 name) (n1 n1-0 n2 n2-0 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2-0) (a a) (b b))
  (defstrand init 3 (n1 n1-0) (n2 n2) (a a) (b b))
  (defstrand resp 2 (n2 n2) (n1 n1-0) (b b) (a a))
  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))
  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig n1 n1-0)
  (facts (rel2 x-0 n2) (rel2 x n2-0) (rel1 n1-0 n2) (rel1 n1 n2-0)
    (rel2 n1-0 n2) (rel2 n1 n2-0))
  (operation nonce-test (contracted (n2-1 n2-0)) n1 (0 1)
    (enc n1 a (pubk b)) (enc n1 n2-0 b (pubk a)))
  (traces
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2-0 b (pubk a)))
      (send (enc n2-0 (pubk b))))
    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2 b (pubk a))))
    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 b (pubk a)))))
  (label 25)
  (parent 17)
  (realized)
  (shape)
  (maps ((0 1) ((a a) (b b) (n1 n1) (n1-0 n1-0) (n2 n2-0) (n2-0 n2))))
  (origs (n1 (0 0)) (n1-0 (1 0))))

(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 n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    (facts (rel1 n1 n2) (rel2 n1 n2)))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b)))))
  (defrule rebind-x
    (forall ((x y text))
      (implies
        (fact rel1 x y)
        (exists ((x-0 name)) (fact rel2 x-0 y)))))
  (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))))
  (defgenrule fact-init-rel11
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel1 n1 n2))))
  (defgenrule fact-init-rel20
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel2 n1 n2))))
  (comment "Needham-Schroeder with no role origination assumptions"))

(defskeleton ns
  (vars (n1 n2 n2-0 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (defstrand init 3 (n1 n1) (n2 n2-0) (a a) (b b))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (comment "Double initiator point-of-view, same nonce")
  (traces
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2-0 b (pubk a)))
      (send (enc n2-0 (pubk b)))))
  (label 26)
  (realized)
  (preskeleton)
  (origs (n1 (1 0)) (n1 (0 0)))
  (comment "Not a skeleton"))

(defskeleton ns
  (vars (x name) (n1 n2 text) (a b name))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b))
  (uniq-orig n1)
  (facts (rel2 x n2) (rel1 n1 n2) (rel2 n1 n2))
  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
    (enc n1 a (pubk b)) (enc n1 n2 b (pubk a)))
  (traces
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))))
  (label 30)
  (parent 26)
  (realized)
  (shape)
  (maps ((0 0) ((a a) (b b) (n1 n1) (n2 n2))))
  (origs (n1 (0 0))))

(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 n1 n2 b (pubk a)))
      (send (enc n2 (pubk b))))
    (facts (rel1 n1 n2) (rel2 n1 n2)))
  (defrole resp
    (vars (b a name) (n2 n1 text))
    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b)))))
  (defrule rebind-x
    (forall ((x y text))
      (implies
        (fact rel1 x y)
        (exists ((x-0 name)) (fact rel2 x-0 y)))))
  (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))))
  (defgenrule fact-init-rel11
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel1 n1 n2))))
  (defgenrule fact-init-rel20
    (forall ((z strd) (n2 n1 text))
      (implies
        (and (p "init" z 2) (p "init" "n2" z n2) (p "init" "n1" z n1))
        (fact rel2 n1 n2))))
  (comment "Needham-Schroeder with no role origination assumptions"))

(defskeleton ns
  (vars (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (non-orig (privk a))
  (uniq-orig n2)
  (comment "Responder point-of-view")
  (traces
    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b)))))
  (label 31)
  (unrealized (0 2))
  (origs (n2 (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton ns
  (vars (x name) (n2 n1 text) (a b name))
  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))
  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))
  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  (non-orig (privk a))
  (uniq-orig n2)
  (facts (rel2 x n2) (rel1 n1 n2) (rel2 n1 n2))
  (rule rebind-x fact-init-rel11 fact-init-rel20)
  (operation nonce-test (added-strand init 3) n2 (0 2)
    (enc n1 n2 b (pubk a)))
  (traces
    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
      (recv (enc n2 (pubk b))))
    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
      (send (enc n2 (pubk b)))))
  (label 32)
  (parent 31)
  (realized)
  (shape)
  (maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))
  (origs (n2 (0 1))))

(comment "Nothing left to do")