Atomicity Properties

Correctness is a prime concern for electronic commerce protocols. How can we show that a given protocol is safe for use? Here we show how to use model checking to test whether electronic commerce protocols satisfy some given atomicity properties.

For verifying properties of protocols, model checking is a dramatic improvement over doing hand proofs, because it is mechanizable; it is a dramatic improvement over using state-of-the-art theorem provers because it is automatic, fast, and requires no human interaction. Moreover, we found a number of problems in proposed electronic commerce protocols using model checking. Model checking allows us to focus on just those aspects of the protocol necessary to guarantee desired properties. In doing so, we can gain a better understanding of why the protocol works and often can identify places of optimizing it.

For this paper, we have chosen to check atomicity properties. [2] argue that these properties are central to electronic commerce protocols.

In an atomic protocol, an electronic purchase either

• aborts with no transfer of money and goods; or
• fully completes with money and goods exchanged.

Moreover, these atomic properties are preserved even if communications fail between some of the parties, because of failure of either a communications link or a node (including the parties participating in the protocol.)

Tygar [22] gave informal descriptions of three protocol properties that appear to be related to atomicity:

money atomicity

Money should neither be created nor destroyed by electronic commerce protocols. For example, this protocol is not money atomic:

1. Consumer sends message to consumer's bank: transfer $value to merchant;
2. Consumer's bank decrements consumer's balance by $value;
3. Consumer's bank sends message to merchant's bank: increase merchant's bank balance by $value;
4. Merchant's bank increments merchant's balance by $value.

If Message 3 is not received, then the consumer's balance will have lost money without the merchant's bank having received the money. Effectively, money is destroyed.

goods atomicity

A merchant should receive payment if and only if the consumer receives the goods. Goods atomicity is particularly relevant in the case of electronic goods (such as binary files) that are delivered over the network. For example this protocol is not goods atomic:

1. Consumer sends credit card number to merchant;
2. Merchant charges consumer's credit card;
3. Merchant sends electronic goods to consumer

Suppose Message 3 is not received by the consumer; then she will not have received the goods for which she was charged.

certified delivery

In the case of electronic goods, both the merchant and the consumer should be able to give non-repudiable proof of the contents of the delivered goods. (We do not consider certified delivery in this paper.)

In this paper, we discuss how to use model checking to determine whether money atomicity and goods atomicity hold of two classes of electronic commerce protocols: account-based (e.g., NetBill [5, 21]) and token-based (e.g., a simplified protocol inspired by Chaum's offline Digicash protocol [3, 4]). We used the FDR model checker [15], though other model checkers could have been used.