Formal Verification Method Of Model Checking-based E-commerce Agreement

The secure e-commerce protocols are fundamental to E-commerce. But, because of subtleties involved in their design, many of them have been shown to have flaws. To avoid these subtle misconceptions, several formal methods for analyzing e-commerce protocols have been devised. Model checking has been proved to be very useful for this purpose, although it has a poor ability of illation. Meanwhile, with the growing popularity of the Internet, it is necessary to analyze multiple runs of the protocol in the presence of site or communication failure. This paper's main contribution includes:1. Presenting a framework based on the protocol message exchanges. We define an extended finite state automaton, some new logic rules and a set of analysis steps. Modeling the protocol by such a FSA, we can not only display dynamically how each participant executes the protocol concurrently, but improve the ability of illation of the FSA, which enable us to analyze signature and ciphertext in the e-commerce protocols. We take Anonymous Atomic Transactions Protocol as an example, and find such properties as accountability, fairness and atomicity are satisfied in this protocol given that the principals are honest. After abstracting the model, we use a model-checking tool UPPAAL to verify whether the time of the protocol violates or not.2. Presenting a framework based on the principals' action exchanges. We extend finite state automata with logic rules, trust matrix and actions of principals to analyze E-commerce protocols. The trust matrix describes the reliable relationship between the principals formally so that the initial state assumption is unnecessary. The set of actions leads us to model the protocol without idealization process, and the set of inference rules is provided for reduction and analysis of signature and ciphertext. As an example, accountability is found not to be satisfied in the AATP when the participants are dishonest. Fortunately, we can find the reason of violation according to the principals' models. After optimizing the protocol, we can show the accountability, fairness and atomicity are satisfied.