(comment "CPSA 2.1.0")
(comment "All input read")

(defprotocol epmo_acctnum basic
  (defrole bank
    (vars (b c m name) (acctnum text) (hash name) (nc nm nb price text))
    (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 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" 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) (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" 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))))))

(defskeleton epmo_acctnum
  (vars (nm nc nb goods price text) (b m c hash name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (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))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton epmo_acctnum
  (vars (nm nc nb goods price acctnum text) (b m c hash name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (hash hash))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk b) (privk m) (privk c) (privk hash))
  (uniq-orig nm nc nb)
  (operation encryption-test (added-strand bank 2)
    (enc (enc "hash" c nc nb nm price (pubk hash)) (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" 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))))))
  (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 hash b-0 name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (hash hash))
  (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 hash) (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" 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-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 "2 in cohort - 2 not yet seen"))

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

(defskeleton epmo_acctnum
  (vars (nm nc nb price acctnum goods text) (m c hash b name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (hash hash))
  (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 hash) (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" 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)))))
  (label 5)
  (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 hash b name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (hash hash))
  (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 hash) (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" 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-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 6)
  (parent 3)
  (unrealized (0 0) (0 2))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton epmo_acctnum
  (vars (nm nc nb price acctnum goods text) (c hash b m name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (hash hash))
  (defstrand customer 5 (acctnum acctnum) (nb nb) (nc nc) (nm nm)
    (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 (added-strand 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 5)
  (unrealized)
  (shape))

(defskeleton epmo_acctnum
  (vars (nm nc nb price acctnum goods nm-0 price-0 text)
    (m c hash b name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (hash hash))
  (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 hash) (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" 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 (enc c nc goods (pubk m)))
      (send (enc nc nm-0 m price-0 (pubk c)))))
  (label 9)
  (parent 6)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

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

(defskeleton epmo_acctnum
  (vars (nm nc nb price nm-0 price-0 acctnum goods text)
    (c hash b m name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (hash hash))
  (defstrand merchant 2 (nc nc) (nm nm-0) (goods goods) (price price-0)
    (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) (hash hash))
  (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 hash) (privk b) (privk m))
  (uniq-orig nm nc nb nm-0)
  (operation nonce-test (added-strand 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)))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm-0 m price-0 (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 11)
  (parent 9)
  (seen 8)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

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

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

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

(defskeleton epmo_acctnum
  (vars (nm nc nb price nb-0 nm-0 price-0 acctnum goods text)
    (c hash hash-0 b m name))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (hash hash))
  (defstrand bank 2 (acctnum acctnum) (nc nc) (nm nm) (nb nb-0)
    (price price) (b b) (c c) (hash hash-0))
  (defstrand merchant 2 (nc nc) (nm nm-0) (goods goods) (price price-0)
    (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) (hash hash))
  (precedes ((0 1) (4 1)) ((1 1) (4 3)) ((2 1) (1 0)) ((3 1) (0 0))
    ((4 0) (3 0)) ((4 2) (2 0)) ((4 4) (0 2)))
  (non-orig (privk c) (privk hash) (privk hash-0) (privk b) (privk m))
  (uniq-orig nm nc nb nm-0)
  (operation nonce-test (added-strand 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)))))
    ((recv (enc c nc nm acctnum price (pubk b)))
      (send
        (cat
          (enc (enc "hash" c nc nb-0 nm price (pubk hash-0)) (privk b))
          (enc nc nb-0 (pubk c)))))
    ((recv (enc c nc goods (pubk m)))
      (send (enc nc nm-0 m price-0 (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 16)
  (parent 15)
  (seen 11)
  (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 text) (hash name) (nc nm nb price text))
    (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 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" 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) (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" 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))))))

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

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

(defskeleton epmo_acctnum
  (vars (nm nb nc price acctnum goods text) (b m c hash name))
  (defstrand bank 3 (acctnum acctnum) (nc nc) (nm nm) (nb nb)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand merchant 4 (nb nb) (nc nc) (nm nm) (goods goods)
    (price price) (b b) (c c) (m m) (hash hash))
  (defstrand customer 5 (acctnum acctnum) (nb nb) (nc nc) (nm nm)
    (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 27)
  (parent 25)
  (unrealized)
  (shape))

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

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

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

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

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

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

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

(comment "Nothing left to do")