Figures 6, 7, and 8 present the consumer, merchant, and bank processes in FDR. To provide a more realistic modeling of the operation of the protocol, we have expanded the protocol behavior outlined in Figure 5 to include:
Unfortunately, in the context of this slightly more realistic system, a serious ambiguity arises. Consider the following scenerio. A consumer withdraws a coin from the bank and attempts to use the coin to pay a merchant. However, as the consumer's response to the merchant's challenge was in transit, the communication network fails. The consumer is left in an uncertain situation. Has the coin been spent? If the merchant actually receives the response, then the consumer should consider the coin spent, but if not, then the coin is unspent. This is a critical issue for money atomicity, because if the consumer makes the wrong guess, then either money will be lost or she could be accused of double spending. To establish money atomicity, we allow the consumer to go to the bank in this situation and see if the coin has been spent; if it has not, she is eligible for a refund on the coin. Of course this leads to a problem: the consumer can spend the coin and then immediately go to the bank and claim the coin may have been lost in transit and obtain a refund, and then moments later the merchant appears coin in hand. In practice this issue could be addressed by timeout/coin-lifetime management. In our model, we abstract the details of how this is solved and enter an ``arbitration'' state.
There are, however, two well-defined kinds of fraud that are detected
and resolved in our model. The first is when a consumer attempts to
double spend a coin, and the second is when a merchant attempts to
deposit a coin twice. Both cases are detected by the bank and
respective events cFraud and mFraud are triggered by the
bank process. This is important, because it allows us to talk about
money atomicity properties: in short, money atomicity holds when there
are no cFraud and mFraud events. We elaborate further
when we discuss money atomicity.
Our model includes only two challenge/response pairs, whereas there are really billions of possible such pairs. However, the specific identities of challenge/response pairs are immaterial: the critical property is the number of different challenges to which the customer responds (in fact there are only three important cases corresponding to zero, one, or more than one consumer response). Hence we consider just two ``symbolic'' challenge response pairs. We also abstract the statistical arguments, and simply state that if both of the symbolic challenge/response pairs are sent to the bank, then the bank has proof of consumer double spending.
We remark that the bank process is somewhat complicated because the
bank must record information as it proceeds. This is somewhat
cumbersome in FDR, and involves using process parameters. The main
process involved here is WAIT, which has three parameters, the
first indicating whether the coin has been deposited or returned, and
the second and third indicating which challenge/response pairs have
been seen.
Figure 6: The consumer process for the simplified digital cash protocol.
Figure 7: The merchant process for the simplified digital cash protocol.
Figure 8: The bank process for the simplified digital cash protocol.
