Study And Implementation On Atomicity Of E-commerce Protocol Base On Symbolic Model Checking

Along with the extensive use of e-commerce at the scope in whole world, there are also more and more disputes in e-commerce. Much cause is owing to the defect of electronics payment protocol itself in multitudinous e-commerce disputes. Thus electronics payment protocol became the bottleneck of e-commerce. And the atomicity of electronic payment protocol is the main cause to lead to giving rise to dispute. Thus atomicity of e-commerce protocol became the hotspot which be studied in recent years. People put forward many protocols in accordance with atomicity of electronics payment protocol, and attempt to solve this question. The design of e-commerce protocol is a very huge and complicated job, and has extremely easily appeared the unimageable mistake, and one is seen probably the existing the various leaks of protocol that is the most perfect. The analysis for atomicity of e-commerce protocol becomes the subject of reality.There are some important means to test e-commerce protocol at present: the intuitionistic analysis, the real inspection analysis techniques to attack test and formalization analysis. Because the fact that the form is rely on formalization analysis and formalization tool, it possesses the merit of tight logical and universal asserts, but possesses the defects that the logical verify of formalization analysis needs initialization condition of non-formalization analysis, as well as the defects idealization to the protocol. Gavin Lowe firstly uses CSP and the model check technology to analyses the security protocol, and it overcome the defect mentioned above that the logic verify. The model is tested at the aspect that the e-commerce protocol safety analysis is verified and is got the extensive application.In this thesis, the symbolic model checking ware (SMV) is applied for analysing the atomicity of e-commerce protocol, and analyses and tests to protocol to with SET's, and pointed out the defect of protocol on the foundation carrying on the form description to agreement to with SET's. Improving to this protocol at the same time, again to the protocol after improvements analyses and testing indicates that it is feasible for the symbolic model checking ware to analysis the SET protocol.