Money Atomicity for Simplified Digital Cash Protocol

Recall the money conservancy property given by the sum in Formula 1. The following CSP specification expresses this property in the context of the simplified digital cash protocol:

SPEC3 = STOP ||
        (debitC -> ((depositC -> STOP) ||
                    (cKeepsToken -> STOP) ||
                    (depositM -> STOP)))

This specification holds in the presence of non-bank communication failures and limited non-bank agent failures. Surprisingly, it even holds in the presence of consumer and merchant fraud.

Next consider the cash property component of money atomicity. This states that possession of a coin gives the possessor the right to spend and/or deposit the coin. For C, this can be stated as:

SPECcashc =
   STOP ||
   (cinb.token -> ((tokenSpent -> STOP) ||
                   (cKeepsToken -> STOP) ||
                   (depositC -> STOP))).

and for M we have:

SPECcashm =
   STOP ||
   (mGetsToken ->
             ((depositM-> STOP) || 
              (mGetsRefundSlip -> STOP))).

C's cash property does in fact hold in the presence of fraud (that is, fraud by M cannot affect C's cash property; M can fail to deliver the goods, but that is not a violation of the cash property, but of goods atomicity). However, M's cash property does not hold: it can be violated by C's fraud. When FDR is applied to this specification, it generates the following counterexample:

coutb.tokenReq, binc.tokenReq, debitC,
boutc.token, cinb.token, coutm.goodsReq,
minc.goodsReq, moutc.challengeA,
cinm.challengeA, coutm.responseA,
minc.responseA, mGetsToken, moutc.goods,
moutb.responseA, binm.responseA, depositM,
boutm.depositSlip, minb.depositSlip,
cinm.goods, coutm.goodsReq, minc.goodsReq,
moutc.challengeB, cinm.challengeB,
coutm.responseB, minc.responseB, mGetsToken,
moutc.goods, moutb.responseB,
binm.responseB, boutm.alreadyDeposited,
cFraud, minb.alreadyDeposited, cinm.goods,
tokenSpent

This sequence of events corresponds to the scenario where a consumer double spends a coin: after finishing a successful transaction with the merchant (shown by events mGetsToken, depositM, and cinm.goods), the consumer uses the coin again (mGetsToken), gets the goods (cinm.goods), but instead of successfully depositing the coin, the merchant receives a message indicating that the coin in question had been spent before (boutm.alreadyDeposited), and consumer fraud (cFraud) is revealed. (For further details, see the Appendix.)

However, in the absence of revealed fraud (i.e. in the case where there are no (cFraud) or (mFraud) events), M's cash property is satisfied. We express this as follows:

SPECcashm' =
   STOP ||
   ((mGetsToken ->
           ((depositM -> STOP) || 
            (mGetsRefundSlip -> STOP))) ||
    FRAUD)

where FRAUD denotes processes that contain at least one fraud event, cFraud or mFraud, and are otherwise arbitrary. Using FDR we checked that indeed the unmodified protocol satisfies this modified property.