E-commerce Protocol Analysis And Verification Based On SPIN Model Checking

As the wide application of Internet and distributed system, the electronic commerce develops more and more quickly too, and the correspondent web e-commerce protocols are the keys to make sure that the new exchange model runs smoothly. The design of e-commerce protocol is a very large and complicated job, and has extremely easily appeared all kinds of unexpected loopholes and mistakes. The features of protocols, such as distributed, asynchrony and concurrency, may lead to unpredictable losses, therefore, the analysis of e-commerce protocol becomes a subject of reality.Formal method is an important method to analyze and verify e-commerce. It's hard to find potential errors by traditional non-formal method, so the formal method is becoming a hot topic. There are many famous formal methods such as BAN logic, strand space theory, theorem proving and so on. As a formal method, model checking method can automatically verify whether a system meets its design specifications. It has high automation and provides counter-examples, can effectively reduce the protocol design mistakes, and has been widely used in software and hardware verification area. SPIN is one of the well-known model checking tools which is used in distributed system.Based on the model checker SPIN, this paper is analysis and verify a series of e-commerce protocols in HDPolyService system. The article described the SPIN model checking verification mechanism, the basic grammar of PROMELA, liner temporal logic properties, and introduced these three "Distributed" transaction protocols in detail. After analyzed the RFC documents, we extracted formal description and state transition relation in the protocol, and transformed to programs PROMELA using the input language of SPIN. Then some properties were represented by LTL formula. The simulation results were used to repair the models, and some properties were verified by SPIN. Finally, we perfected the protocol by the verification results, summarized the current work and prospected for future plan. The paper shows that the application of SPIN in verifying the e-commerce protocol is feasible, and these three protocols have practical values.