Check out the new USENIX Web site. next up previous
Next: Assumptions Up: Model Checking Electronic Commerce Previous: Model Checking

Two Case Studies

We investigate NetBill and a simplified digital cash protocol with respect to money atomicity and goods atomicity. Money atomicity is concerned with the conservation of money in the context of account balances and electronic coins. That is, electronic coins should not be arbitrarily created or destroyed, and fund transfers and conversions between funds and coins should be consistent. In other words, if we have a system formed by a consumer C and a merchant M who have accounts at a bank, the sum given by the formula

  eqnarray89

should be conserved. In the context of electronic coins, another component of money atomicity is that rightful possession of a coin should entitle the owner to spend the coin or deposit it in an account. This ``cash property'' will play an important role in our analysis of a simplified digital cash protocol.

Goods atomicity is concerned with the integrity of a sale: we want to guarantee that goods are transferred exactly when money is transferred. A consumer only wants to pay for goods received. A merchant wants to be payed for goods delivered.





TOM Comversion
Sat Oct 5 08:55:54 EDT 1996