Model checking is a technique that determines whether a property holds of a finite state machine. The expression of the property and the machine could be in different languages where the property is a logical formula and the machine is described as a set of states and a state transition function. Since the machine has a finite number of states, an exhaustive search (through a standard reachability algorithm) is done to check that the logical formula holds at every state. The model checker SMV uses this approach. Alternatively, as with FDR, the expression of the property and the machine could be in the same language. In this case, a test for language inclusion is done to determine whether the property (one set of traces) holds of the machine (the second set of traces). Model checking is completely automatic, and usually fast, at least in comparison to alternative techniques like theorem proving.
An additional benefit that model checking provides over other techniques such as theorem proving is that if the property being checked does not hold, a counterexample is produced. This feedback is an invaluable means of debugging. It also is a way to explore the design space, perhaps finding ways to optimize a design (e.g., by eliminating a message exchanged or an extra encryption step).
In our context of using FDR as our model checker, we describe the protocol that we wish to analyze through a CSP [10] process, Imp. This is the ``machine'' we want to check. We describe the property, e.g., money atomicity, that we wish to check of the protocol as another CSP process, Spec. To determine whether the protocol satisfies the property we test whether Imp is a refinement (in the technical sense used in CSP) of Spec. Roughly speaking, Imp's set of traces should be a subset of Spec's set of traces; thus, the machine is a trace refinement of the property. In reality, for atomicity properties, we need the failure refinement, which extends the trace refinement to handle non-determinism.
Model checking is a demonstrated success in hardware verification. Researchers and industrialists have used checkers like SMV [17], Murphi [6], COSPAN [9] and SPIN [11] to find bugs in published circuit designs, floating point standards, and cache coherence protocols for multiprocessors. It has been adopted by the hardware community to complement the traditional validation method of hardware simulation.
Model checking has also recently gained the attention of the software community. Notably, Atlee and Gannon used SMV to check safety properties for event-driven systems; Jackson uses his model enumeration method in Nitpick to check Z-like specifications [12]; and Vaziri-Farahani and Wing used SMV to check cache coherence in distributed file systems [23].
In the security domain, Roscoe [19] used FDR to prove noninterference of a
simple security high-low hierarchy (after Bell-LaPadula's
model) and Lowe [14] recently used FDR
to debug and prove the correctness of the Needham-Schroeder authentication
protocols [18].
Our work is the first to use model checking for analyzing electronic
commerce protocols and for checking atomicity properties
.