Model checking electronic commerce protocols

Abstract

The paper develops model checking techniques to examine NetBill and Digicash. We show how model checking can verify atomicity properties by analyzing simpli ed versions of these protocols that retain crucial security constraints. For our analysis we used the FDR model checker. 1 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