(herald
  "Electronic Purchase with Money Order Protocol Variant with Key Hashing"
  (comment "This version includes account numbers in exchanges"))

(comment "CPSA 2.2.11")
(comment "All input read from epmo_acctnum-key-hash.scm")

(defprotocol epmo_acctnum basic
  (defrole bank
    (vars (b c m name) (acctnum nc nm nb price text))
    (trace (recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    (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 name) (acctnum nb nc nm goods price text))
    (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" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb)))
    (non-orig (privk b))
    (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 name) (nb nc nm goods price text))
    (trace (recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    (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))))))

(defskeleton epmo_acctnum
  (vars (nm nc nb goods price text) (b m c name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (non-orig (privk b) (privk m) (privk c))
  (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" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m)))))
  (label 0)
  (unrealized (0 2))
  (origs (nm (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nc nb goods price acctnum text) (b m c name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nm nc nb)
  (operation encryption-test (added-strand bank 2)
    (enc (enc "hash" (cat c nc nb nm price)) (privk b)) (0 2))
  (traces
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))))
  (label 1)
  (parent 0)
  (unrealized (0 2) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nc nb goods price acctnum acctnum-0 goods-0 text)
    (b m c b-0 name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c))
  (defstrand customer 3 (acctnum acctnum-0) (nc nc) (nm nm)
    (goods goods-0) (price price) (b b-0) (c c) (m m))
  (precedes ((0 1) (2 1)) ((1 1) (0 2)) ((2 0) (0 0)) ((2 2) (1 0)))
  (non-orig (privk b) (privk m) (privk c) (privk b-0))
  (uniq-orig nm nc nb)
  (operation nonce-test (added-strand customer 3) nm (1 0)
    (enc nc nm m price (pubk c)))
  (traces
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c)))))
    ((send (enc c nc goods-0 (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum-0 price (pubk b-0)))))
  (label 2)
  (parent 1)
  (unrealized (0 0) (0 2) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nc nb goods price acctnum goods-0 text) (m c b name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c))
  (defstrand customer 3 (acctnum acctnum) (nc nc) (nm nm)
    (goods goods-0) (price price) (b b) (c c) (m m))
  (precedes ((0 1) (2 1)) ((1 1) (0 2)) ((2 0) (0 0)) ((2 2) (1 0)))
  (non-orig (privk m) (privk c) (privk b))
  (uniq-orig nm nc nb)
  (operation nonce-test (contracted (b-0 b) (acctnum-0 acctnum)) nm
    (1 0) (enc nc nm m price (pubk c))
    (enc c nc nm acctnum price (pubk b)))
  (traces
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c)))))
    ((send (enc c nc goods-0 (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum price (pubk b)))))
  (label 3)
  (parent 2)
  (unrealized (0 0) (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nc nb price acctnum goods text) (m c b name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c))
  (defstrand customer 3 (acctnum acctnum) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (precedes ((0 1) (2 1)) ((1 1) (0 2)) ((2 0) (0 0)) ((2 2) (1 0)))
  (non-orig (privk m) (privk c) (privk b))
  (uniq-orig nm nc nb)
  (operation nonce-test (contracted (goods-0 goods)) nc (0 0)
    (enc c nc goods (pubk m)))
  (traces
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (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)))))
  (label 4)
  (parent 3)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nc nb goods price acctnum goods-0 nm-0 price-0 text)
    (m c b name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c))
  (defstrand customer 3 (acctnum acctnum) (nc nc) (nm nm)
    (goods goods-0) (price price) (b b) (c c) (m m))
  (defstrand merchant 2 (nc nc) (nm nm-0) (goods goods-0)
    (price price-0) (c c) (m m))
  (precedes ((0 1) (2 1)) ((1 1) (0 2)) ((2 0) (3 0)) ((2 2) (1 0))
    ((3 1) (0 0)))
  (non-orig (privk m) (privk c) (privk b))
  (uniq-orig nm nc nb nm-0)
  (operation nonce-test (added-strand merchant 2) nc (0 0)
    (enc c nc goods-0 (pubk m)))
  (traces
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c)))))
    ((send (enc c nc goods-0 (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum price (pubk b))))
    ((recv (enc c nc goods-0 (pubk m)))
      (send (enc nc nm-0 m price-0 (pubk c)))))
  (label 5)
  (parent 3)
  (unrealized (0 0) (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nc nb acctnum nm goods price text) (c b m name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c))
  (defstrand customer 5 (acctnum acctnum) (nb nb) (nc nc) (nm nm)
    (goods goods) (price price) (b b) (c c) (m m))
  (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 b) (privk m))
  (uniq-orig nc nb nm)
  (operation nonce-test (displaced 2 3 customer 5) nb (0 2)
    (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" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (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" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))))
  (label 6)
  (parent 4)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((b b) (m m) (c c) (nm nm) (nc nc) (nb nb) (goods goods)
        (price price))))
  (origs (nc (2 0)) (nm (0 1)) (nb (1 1))))

(defskeleton epmo_acctnum
  (vars (nm nc nb price acctnum goods nm-0 price-0 text) (m c b name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c))
  (defstrand customer 3 (acctnum acctnum) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 2 (nc nc) (nm nm-0) (goods goods) (price price-0)
    (c c) (m m))
  (precedes ((0 1) (2 1)) ((1 1) (0 2)) ((2 0) (3 0)) ((2 2) (1 0))
    ((3 1) (0 0)))
  (non-orig (privk m) (privk c) (privk b))
  (uniq-orig nm nc nb nm-0)
  (operation nonce-test (contracted (goods-0 goods)) nc (0 0)
    (enc nc nm-0 m price-0 (pubk c)) (enc c nc goods (pubk m)))
  (traces
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (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 (enc c nc goods (pubk m)))
      (send (enc nc nm-0 m price-0 (pubk c)))))
  (label 7)
  (parent 5)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nc nb nm price acctnum nm-0 goods price-0 text) (c b m name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm-0) (goods goods)
    (price price-0) (b b) (c c) (m m))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm-0) (nb nb)
    (price price-0) (b b) (c c))
  (defstrand merchant 2 (nc nc) (nm nm) (goods goods) (price price)
    (c c) (m m))
  (defstrand customer 5 (acctnum acctnum) (nb nb) (nc nc) (nm nm-0)
    (goods goods) (price price-0) (b b) (c c) (m m))
  (precedes ((0 1) (3 1)) ((1 1) (3 3)) ((2 1) (0 0)) ((3 0) (2 0))
    ((3 2) (1 0)) ((3 4) (0 2)))
  (non-orig (privk c) (privk b) (privk m))
  (uniq-orig nc nb nm nm-0)
  (operation nonce-test (displaced 2 4 customer 5) nb (0 2)
    (enc nc nb (pubk c)))
  (traces
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm-0 m price-0 (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm-0 price-0)) (privk b))
          nb)) (send (enc (enc "hash" (cat b m nb nm-0)) (privk m))))
    ((recv (enc c nc nm-0 acctnum price-0 (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm-0 price-0)) (privk b))
          (enc nc nb (pubk c)))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c))))
    ((send (enc c nc goods (pubk m)))
      (recv (enc nc nm-0 m price-0 (pubk c)))
      (send (enc c nc nm-0 acctnum price-0 (pubk b)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm-0 price-0)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm-0 price-0)) (privk b))
          nb))))
  (label 8)
  (parent 7)
  (seen 6)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")

(defprotocol epmo_acctnum basic
  (defrole bank
    (vars (b c m name) (acctnum nc nm nb price text))
    (trace (recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    (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 name) (acctnum nb nc nm goods price text))
    (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" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb)))
    (non-orig (privk b))
    (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 name) (nb nc nm goods price text))
    (trace (recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    (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))))))

(defskeleton epmo_acctnum
  (vars (nm nb nc acctnum price text) (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nm nb nc)
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m)))))
  (label 9)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nb nc acctnum price nc-0 goods price-0 text)
    (b m c c-0 name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc-0) (nm nm) (goods goods)
    (price price-0) (b b) (c c-0) (m m))
  (precedes ((0 1) (1 2)) ((1 1) (0 0)) ((1 3) (0 2)))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nm nb nc)
  (operation encryption-test (added-strand merchant 4)
    (enc (enc "hash" (cat b m nb nm)) (privk m)) (0 2))
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c-0 nc-0 goods (pubk m)))
      (send (enc nc-0 nm m price-0 (pubk c-0)))
      (recv
        (cat (enc (enc "hash" (cat c-0 nc-0 nb nm price-0)) (privk b))
          nb)) (send (enc (enc "hash" (cat b m nb nm)) (privk m)))))
  (label 10)
  (parent 9)
  (unrealized (1 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nb nc acctnum price goods text) (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (precedes ((0 1) (1 2)) ((1 1) (0 0)) ((1 3) (0 2)))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nm nb nc)
  (operation encryption-test (displaced 2 0 bank 2)
    (enc (enc "hash" (cat c-0 nc-0 nb nm price-0)) (privk b)) (1 2))
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m)))))
  (label 11)
  (parent 10)
  (unrealized (0 0) (1 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars
    (nm nb nc acctnum price goods acctnum-0 nm-0 goods-0 price-0 text)
    (b m c b-0 m-0 name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum-0) (nb nb) (nc nc) (nm nm-0)
    (goods goods-0) (price price-0) (b b-0) (c c) (m m-0))
  (precedes ((0 1) (2 3)) ((1 1) (0 0)) ((1 3) (0 2)) ((2 0) (1 0))
    ((2 4) (1 2)))
  (non-orig (privk b) (privk m) (privk c) (privk b-0))
  (uniq-orig nm nb nc)
  (operation nonce-test (added-strand customer 5) nb (1 2)
    (enc nc nb (pubk c)))
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((send (enc c nc goods-0 (pubk m-0)))
      (recv (enc nc nm-0 m-0 price-0 (pubk c)))
      (send (enc c nc nm-0 acctnum-0 price-0 (pubk b-0)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm-0 price-0)) (privk b-0))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm-0 price-0)) (privk b-0))
          nb))))
  (label 12)
  (parent 11)
  (unrealized (0 0) (2 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nb nc acctnum price goods acctnum-0 goods-0 text)
    (b m c m-0 name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum-0) (nb nb) (nc nc) (nm nm)
    (goods goods-0) (price price) (b b) (c c) (m m-0))
  (precedes ((0 1) (2 3)) ((1 1) (0 0)) ((1 1) (2 1)) ((1 3) (0 2))
    ((2 0) (1 0)) ((2 4) (1 2)))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nm nb nc)
  (operation encryption-test (displaced 3 0 bank 2)
    (enc (enc "hash" (cat c nc nb nm-0 price-0)) (privk b-0)) (2 3))
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((send (enc c nc goods-0 (pubk m-0)))
      (recv (enc nc nm m-0 price (pubk c)))
      (send (enc c nc nm acctnum-0 price (pubk b)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))))
  (label 13)
  (parent 12)
  (unrealized (0 0) (2 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nb nc acctnum price goods acctnum-0 goods-0 text)
    (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum-0) (nb nb) (nc nc) (nm nm)
    (goods goods-0) (price price) (b b) (c c) (m m))
  (precedes ((0 1) (2 3)) ((1 1) (0 0)) ((1 1) (2 1)) ((1 3) (0 2))
    ((2 0) (1 0)) ((2 4) (1 2)))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nm nb nc)
  (operation nonce-test (contracted (m-0 m)) nm (2 1)
    (enc nc nm m price (pubk c)))
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((send (enc c nc goods-0 (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum-0 price (pubk b)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))))
  (label 14)
  (parent 13)
  (unrealized (0 0) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nb nc acctnum price acctnum-0 goods text) (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum-0) (nb nb) (nc nc) (nm nm)
    (goods goods) (price price) (b b) (c c) (m m))
  (precedes ((0 1) (2 3)) ((1 1) (0 0)) ((1 1) (2 1)) ((1 3) (0 2))
    ((2 0) (1 0)) ((2 4) (1 2)))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nm nb nc)
  (operation nonce-test (contracted (goods-0 goods)) nc (1 0)
    (enc c nc goods (pubk m)))
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((send (enc c nc goods (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum-0 price (pubk b)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))))
  (label 15)
  (parent 14)
  (unrealized (0 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton epmo_acctnum
  (vars
    (nm nb nc acctnum price goods acctnum-0 goods-0 nm-0 price-0 text)
    (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum-0) (nb nb) (nc nc) (nm nm)
    (goods goods-0) (price price) (b b) (c c) (m m))
  (defstrand merchant 2 (nc nc) (nm nm-0) (goods goods-0)
    (price price-0) (c c) (m m))
  (precedes ((0 1) (2 3)) ((1 1) (0 0)) ((1 1) (2 1)) ((1 3) (0 2))
    ((2 0) (3 0)) ((2 4) (1 2)) ((3 1) (1 0)))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nm nb nc nm-0)
  (operation nonce-test (added-strand merchant 2) nc (1 0)
    (enc c nc goods-0 (pubk m)))
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((send (enc c nc goods-0 (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum-0 price (pubk b)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb)))
    ((recv (enc c nc goods-0 (pubk m)))
      (send (enc nc nm-0 m price-0 (pubk c)))))
  (label 16)
  (parent 14)
  (unrealized (0 0) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nb nc acctnum price acctnum-0 goods text) (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm acctnum-0) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm acctnum-0) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum-0) (nb nb) (nc nc)
    (nm acctnum-0) (goods goods) (price price) (b b) (c c) (m m))
  (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))
  (uniq-orig nb nc acctnum-0)
  (operation nonce-test (displaced 3 2 customer 3) nm (0 0)
    (enc nc nm m price (pubk c)))
  (traces
    ((recv (enc c nc acctnum-0 acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb acctnum-0 price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb acctnum-0)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc acctnum-0 m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb acctnum-0 price)) (privk b))
          nb))
      (send (enc (enc "hash" (cat b m nb acctnum-0)) (privk m))))
    ((send (enc c nc goods (pubk m)))
      (recv (enc nc acctnum-0 m price (pubk c)))
      (send (enc c nc acctnum-0 acctnum-0 price (pubk b)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb acctnum-0 price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb acctnum-0 price)) (privk b))
          nb))))
  (label 17)
  (parent 15)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nb nc acctnum price acctnum-0 goods text) (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum-0) (nb nb) (nc nc) (nm nm)
    (goods goods) (price price) (b b) (c c) (m m))
  (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))
  (uniq-orig nm nb nc)
  (operation nonce-test (displaced 3 2 customer 3) nm (0 0)
    (enc nc nm m price (pubk c)))
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((send (enc c nc goods (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum-0 price (pubk b)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))))
  (label 18)
  (parent 15)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nb nc acctnum price acctnum-0 goods nm-0 price-0 text)
    (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum-0) (nb nb) (nc nc) (nm nm)
    (goods goods) (price price) (b b) (c c) (m m))
  (defstrand merchant 2 (nc nc) (nm nm-0) (goods goods) (price price-0)
    (c c) (m m))
  (precedes ((0 1) (2 3)) ((1 1) (0 0)) ((1 1) (2 1)) ((1 3) (0 2))
    ((2 0) (3 0)) ((2 4) (1 2)) ((3 1) (1 0)))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nm nb nc nm-0)
  (operation nonce-test (contracted (goods-0 goods)) nc (1 0)
    (enc nc nm-0 m price-0 (pubk c)) (enc c nc goods (pubk m)))
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((send (enc c nc goods (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum-0 price (pubk b)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb)))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm-0 m price-0 (pubk c)))))
  (label 19)
  (parent 16)
  (unrealized (0 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nb nc price acctnum goods text) (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm acctnum) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm acctnum) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum) (nb nb) (nc nc) (nm acctnum)
    (goods goods) (price price) (b b) (c c) (m m))
  (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))
  (uniq-orig nb nc acctnum)
  (operation nonce-test (contracted (acctnum-0 acctnum)) acctnum (0 0)
    (enc nc acctnum m price (pubk c))
    (enc c nc acctnum acctnum price (pubk b)))
  (traces
    ((recv (enc c nc acctnum acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb acctnum price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb acctnum)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc acctnum m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb acctnum price)) (privk b))
          nb)) (send (enc (enc "hash" (cat b m nb acctnum)) (privk m))))
    ((send (enc c nc goods (pubk m)))
      (recv (enc nc acctnum m price (pubk c)))
      (send (enc c nc acctnum acctnum price (pubk b)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb acctnum price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb acctnum price)) (privk b))
          nb))))
  (label 20)
  (parent 17)
  (seen 21)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nb nc price acctnum goods text) (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum) (nb nb) (nc nc) (nm nm)
    (goods goods) (price price) (b b) (c c) (m m))
  (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))
  (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" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (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" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))))
  (label 21)
  (parent 18)
  (unrealized)
  (shape)
  (maps
    ((0)
      ((b b) (m m) (c c) (nm nm) (nb nb) (nc nc) (acctnum acctnum)
        (price price))))
  (origs (nc (2 0)) (nm (1 1)) (nb (0 1))))

(defskeleton epmo_acctnum
  (vars (nb nc acctnum price acctnum-0 goods nm price-0 text)
    (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm acctnum-0) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm acctnum-0) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum-0) (nb nb) (nc nc)
    (nm acctnum-0) (goods goods) (price price) (b b) (c c) (m m))
  (defstrand merchant 2 (nc nc) (nm nm) (goods goods) (price price-0)
    (c c) (m m))
  (precedes ((0 1) (2 3)) ((1 1) (2 1)) ((1 3) (0 2)) ((2 0) (3 0))
    ((2 2) (0 0)) ((2 4) (1 2)) ((3 1) (1 0)))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nb nc acctnum-0 nm)
  (operation nonce-test (displaced 4 2 customer 3) nm-0 (0 0)
    (enc nc nm-0 m price (pubk c)))
  (traces
    ((recv (enc c nc acctnum-0 acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb acctnum-0 price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb acctnum-0)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc acctnum-0 m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb acctnum-0 price)) (privk b))
          nb))
      (send (enc (enc "hash" (cat b m nb acctnum-0)) (privk m))))
    ((send (enc c nc goods (pubk m)))
      (recv (enc nc acctnum-0 m price (pubk c)))
      (send (enc c nc acctnum-0 acctnum-0 price (pubk b)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb acctnum-0 price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb acctnum-0 price)) (privk b))
          nb)))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price-0 (pubk c)))))
  (label 22)
  (parent 19)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nb nc acctnum price acctnum-0 goods nm-0 price-0 text)
    (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum-0) (nb nb) (nc nc) (nm nm)
    (goods goods) (price price) (b b) (c c) (m m))
  (defstrand merchant 2 (nc nc) (nm nm-0) (goods goods) (price price-0)
    (c c) (m m))
  (precedes ((0 1) (2 3)) ((1 1) (2 1)) ((1 3) (0 2)) ((2 0) (3 0))
    ((2 2) (0 0)) ((2 4) (1 2)) ((3 1) (1 0)))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nm nb nc nm-0)
  (operation nonce-test (displaced 4 2 customer 3) nm (0 0)
    (enc nc nm m price (pubk c)))
  (traces
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((send (enc c nc goods (pubk m)))
      (recv (enc nc nm m price (pubk c)))
      (send (enc c nc nm acctnum-0 price (pubk b)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb)))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm-0 m price-0 (pubk c)))))
  (label 23)
  (parent 19)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nb nc price acctnum goods nm price-0 text) (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm acctnum) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm acctnum) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum) (nb nb) (nc nc) (nm acctnum)
    (goods goods) (price price) (b b) (c c) (m m))
  (defstrand merchant 2 (nc nc) (nm nm) (goods goods) (price price-0)
    (c c) (m m))
  (precedes ((0 1) (2 3)) ((1 1) (2 1)) ((1 3) (0 2)) ((2 0) (3 0))
    ((2 2) (0 0)) ((2 4) (1 2)) ((3 1) (1 0)))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nb nc acctnum nm)
  (operation nonce-test (contracted (acctnum-0 acctnum)) acctnum (0 0)
    (enc nc acctnum m price (pubk c))
    (enc c nc acctnum acctnum price (pubk b)))
  (traces
    ((recv (enc c nc acctnum acctnum price (pubk b)))
      (send
        (cat (enc (enc "hash" (cat c nc nb acctnum price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb acctnum)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc acctnum m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb acctnum price)) (privk b))
          nb)) (send (enc (enc "hash" (cat b m nb acctnum)) (privk m))))
    ((send (enc c nc goods (pubk m)))
      (recv (enc nc acctnum m price (pubk c)))
      (send (enc c nc acctnum acctnum price (pubk b)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb acctnum price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb acctnum price)) (privk b))
          nb)))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price-0 (pubk c)))))
  (label 24)
  (parent 22)
  (seen 20)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nb nc price acctnum goods nm-0 price-0 text) (b m c name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m))
  (defstrand customer 5 (acctnum acctnum) (nb nb) (nc nc) (nm nm)
    (goods goods) (price price) (b b) (c c) (m m))
  (defstrand merchant 2 (nc nc) (nm nm-0) (goods goods) (price price-0)
    (c c) (m m))
  (precedes ((0 1) (2 3)) ((1 1) (2 1)) ((1 3) (0 2)) ((2 0) (3 0))
    ((2 2) (0 0)) ((2 4) (1 2)) ((3 1) (1 0)))
  (non-orig (privk b) (privk m) (privk c))
  (uniq-orig nm nb nc nm-0)
  (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" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm m price (pubk c)))
      (recv
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb))
      (send (enc (enc "hash" (cat b m nb nm)) (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" (cat c nc nb nm price)) (privk b))
          (enc nc nb (pubk c))))
      (send
        (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb)))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm-0 m price-0 (pubk c)))))
  (label 25)
  (parent 23)
  (seen 21)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")