cpsa-4.4.4: tst/sorted_epmo_acctnum_shapes.tst

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

(herald "Electronic Purchase with Money Order Protocol Variant"
  (bound 12)
  (comment "This version includes account numbers in exchanges"
    "This version uses sorts to avoid confusion"
    "between a nonce and other data"))

(comment "CPSA 4.3.1")

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

(comment "Strand count bounded at 12")

(defprotocol sorted_epmo_acctnum basic
  (defrole bank
    (vars (b c m name) (acctnum price text) (hash name) (nc nm nb data))
    (trace (recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" b m nb nm (pubk hash)) (privk m))))
    (non-orig (privk hash))
    (annotations b
      (1
        (forall ((pm name))
          (implies
            (and (authtransfer c acctnum b price pm nm)
              (reqtransfer pm b price pm nm))
            (dotransfer acctnum b price pm nm))))
      (2
        (and (says c (authtransfer c acctnum b price m nm))
          (says m (reqtransfer m b price m nm))))))
  (defrole customer
    (vars (b c m hash name) (acctnum goods price text) (nc nm nb data))
    (trace (send (enc c nc goods (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum price (pubk b)))
      (recv
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          nb)))
    (non-orig (privk b) (privk hash))
    (uniq-orig nc)
    (annotations c
      (1
        (says m
          (implies
            (exists ((acctnum2 text))
              (dotransfer acctnum2 b price m nm)) (doship m goods c))))
      (3
        (says b
          (forall ((pm name))
            (implies
              (and (authtransfer c acctnum b price m nm)
                (reqtransfer pm b price pm nm))
              (dotransfer acctnum b price pm nm)))))
      (4 (authtransfer c acctnum b price m nm))))
  (defrole merchant
    (vars (b c m hash name) (goods price text) (nc nm nb data))
    (trace (recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          nb))
      (send (enc (enc "hash" b m nb nm (pubk hash)) (privk m))))
    (non-orig (privk hash))
    (uniq-orig nm)
    (annotations m
      (1
        (implies
          (exists ((acctnum2 text)) (dotransfer acctnum2 b price m nm))
          (doship m goods c)))
      (2
        (and
          (says b
            (forall ((pm name))
              (exists ((acctnum2 text))
                (implies
                  (and (authtransfer c acctnum2 b price m nm)
                    (reqtransfer pm b price pm nm))
                  (dotransfer acctnum2 b price pm nm)))))
          (says c
            (exists ((acctnum2 text))
              (authtransfer c acctnum2 b price m nm)))))
      (3 (and (reqtransfer m b price m nm) (doship m goods c)))))
  (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 sorted_epmo_acctnum
  (vars (nm nc nb data) (goods price text) (b m c hash name))
  (defstrand merchant 4 (nc nc) (nm nm) (nb nb) (goods goods)
    (price price) (b b) (c c) (m m) (hash hash))
  (non-orig (privk b) (privk m) (privk c) (privk hash))
  (uniq-orig nm nc nb)
  (traces
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          nb))
      (send (enc (enc "hash" b m nb nm (pubk hash)) (privk m)))))
  (label 0)
  (unrealized (0 2))
  (origs (nm (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton sorted_epmo_acctnum
  (vars (nm nc nb data) (price acctnum goods text) (c hash b m name))
  (defstrand merchant 4 (nc nc) (nm nm) (nb nb) (goods goods)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand bank 2 (nc nc) (nm nm) (nb nb) (acctnum acctnum)
    (price price) (b b) (c c) (hash hash))
  (defstrand customer 5 (nc nc) (nm nm) (nb nb) (acctnum acctnum)
    (goods goods) (price price) (b b) (c c) (m m) (hash hash))
  (precedes ((0 1) (2 1)) ((1 1) (2 3)) ((2 0) (0 0)) ((2 2) (1 0))
    ((2 4) (0 2)))
  (non-orig (privk c) (privk hash) (privk b) (privk m))
  (uniq-orig nm nc nb)
  (operation nonce-test (displaced 2 3 customer 5) nb (0 2)
    (enc "hash" c nc nb nm price (pubk hash)) (enc nc nb (pubk c)))
  (traces
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          nb))
      (send (enc (enc "hash" b m nb nm (pubk hash)) (privk m))))
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          (enc nc nb (pubk c)))))
    ((send (enc c nc goods (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum price (pubk b)))
      (recv
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          nb))))
  (label 8)
  (parent 0)
  (realized)
  (shape)
  (maps
    ((0)
      ((b b) (m m) (c c) (nm nm) (nc nc) (nb nb) (hash hash)
        (goods goods) (price price))))
  (origs (nc (2 0)) (nm (0 1)) (nb (1 1))))

(comment "Nothing left to do")

(defprotocol sorted_epmo_acctnum basic
  (defrole bank
    (vars (b c m name) (acctnum price text) (hash name) (nc nm nb data))
    (trace (recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" b m nb nm (pubk hash)) (privk m))))
    (non-orig (privk hash))
    (annotations b
      (1
        (forall ((pm name))
          (implies
            (and (authtransfer c acctnum b price pm nm)
              (reqtransfer pm b price pm nm))
            (dotransfer acctnum b price pm nm))))
      (2
        (and (says c (authtransfer c acctnum b price m nm))
          (says m (reqtransfer m b price m nm))))))
  (defrole customer
    (vars (b c m hash name) (acctnum goods price text) (nc nm nb data))
    (trace (send (enc c nc goods (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum price (pubk b)))
      (recv
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          nb)))
    (non-orig (privk b) (privk hash))
    (uniq-orig nc)
    (annotations c
      (1
        (says m
          (implies
            (exists ((acctnum2 text))
              (dotransfer acctnum2 b price m nm)) (doship m goods c))))
      (3
        (says b
          (forall ((pm name))
            (implies
              (and (authtransfer c acctnum b price m nm)
                (reqtransfer pm b price pm nm))
              (dotransfer acctnum b price pm nm)))))
      (4 (authtransfer c acctnum b price m nm))))
  (defrole merchant
    (vars (b c m hash name) (goods price text) (nc nm nb data))
    (trace (recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          nb))
      (send (enc (enc "hash" b m nb nm (pubk hash)) (privk m))))
    (non-orig (privk hash))
    (uniq-orig nm)
    (annotations m
      (1
        (implies
          (exists ((acctnum2 text)) (dotransfer acctnum2 b price m nm))
          (doship m goods c)))
      (2
        (and
          (says b
            (forall ((pm name))
              (exists ((acctnum2 text))
                (implies
                  (and (authtransfer c acctnum2 b price m nm)
                    (reqtransfer pm b price pm nm))
                  (dotransfer acctnum2 b price pm nm)))))
          (says c
            (exists ((acctnum2 text))
              (authtransfer c acctnum2 b price m nm)))))
      (3 (and (reqtransfer m b price m nm) (doship m goods c)))))
  (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 sorted_epmo_acctnum
  (vars (nm nb nc data) (acctnum price text) (b m c hash name))
  (defstrand bank 3 (nc nc) (nm nm) (nb nb) (acctnum acctnum)
    (price price) (b b) (c c) (m m) (hash hash))
  (non-orig (privk b) (privk m) (privk c) (privk hash))
  (uniq-orig nm nb nc)
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" b m nb nm (pubk hash)) (privk m)))))
  (label 186)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton sorted_epmo_acctnum
  (vars (nm nb nc data) (price acctnum goods text) (b m c hash name))
  (defstrand bank 3 (nc nc) (nm nm) (nb nb) (acctnum acctnum)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand merchant 4 (nc nc) (nm nm) (nb nb) (goods goods)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand customer 5 (nc nc) (nm nm) (nb nb) (acctnum acctnum)
    (goods goods) (price price) (b b) (c c) (m m) (hash hash))
  (precedes ((0 1) (2 3)) ((1 1) (2 1)) ((1 3) (0 2)) ((2 0) (1 0))
    ((2 2) (0 0)) ((2 4) (1 2)))
  (non-orig (privk b) (privk m) (privk c) (privk hash))
  (uniq-orig nm nb nc)
  (operation nonce-test (contracted (acctnum-0 acctnum)) nm (0 0)
    (enc nc nm m price (pubk c)) (enc c nc nm acctnum price (pubk b)))
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" b m nb nm (pubk hash)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          nb))
      (send (enc (enc "hash" b m nb nm (pubk hash)) (privk m))))
    ((send (enc c nc goods (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum price (pubk b)))
      (recv
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" c nc nb nm price (pubk hash)) (privk b))
          nb))))
  (label 196)
  (parent 186)
  (realized)
  (shape)
  (maps
    ((0)
      ((b b) (m m) (c c) (nm nm) (nb nb) (nc nc) (hash hash)
        (acctnum acctnum) (price price))))
  (origs (nc (2 0)) (nm (1 1)) (nb (0 1))))

(comment "Nothing left to do")