Chi Wong outlined an electronic commerce system consisting of a customer, a merchant, a bank, and goods that can be sent over a network. She then defined two main properties of the system: money atomicity, which requires that the total money in the system remains constant; and goods atomicity, which requires that the customer receives the goods if and only if the merchant receives the money. She described the possible failure modes of the system as either network or processor failure, and cheating, which would be an attempt by the customer to double-spend, or an attempt by the merchant to double-deposit.
Chi then explained that model checking, an approach based on exhaustive search of finite state spaces, could be applied to this system to verify its properties. A model of this system and a property specification could be given as input to a model checker, which would return a yes, meaning that the properties were verified, or provide a counterexample.
In FDR model checking, which stands for ``Failures Divergence Refinement,'' the system model and the property specification are both state machines represented in the same language. The model checker then implements a refinement relation to see if the state space given by the model is a subset of the state space given by the property specification. Chi described building FDR models of simplified versions of the NetBill and Digicash systems, which were then run through a model checker; she referred the audience to the paper for the results, noting that while model checking has been useful for hardware verification, and recently also for software verification, this is the first time it has been applied to electronic commerce protocols. As future work, Chi hopes to create a more complete failure model, do more complex runs, add more properties, and explicitly represent the role of cryptography, which is currently abstracted away.
Dan Geer asked whether it was possible to use these techniques during design rather than just analytically; Chi thought probably not with FDR model checking, but that automatic program generation refinement tools might be useful. Eric Hughes asked how the size of the state space affected the process; Chi referred him to the appendix, noting that the example given had about 3000 states. Eric then asked about asymptotic properties, and Chi answered that the model checker looks at all possibilities and thus is exponential; Eric asked if symbolic modeling had been considered as a technique to cut it down, and Chi replied that it had, and that a tech report would follow.
Jeanette Wing then followed up on Dan Geer's question by stating that yes, you can use these model checkers for iterative checking and design of protocols, and that it would be pushbutton technology so the iteration would be fast. She noted that SMV is a richer language for expressing properties, and that FDR is tuned to check deadline detection and is more limited.