The Application Study On Formalism And Model Checking Techniques Of Electronic Commerce Protocols

Formal analysis of E-commerce protocols is an important aspect of E-commerce study, the E-commerce protocols is a cryptographic protocol of E-commerce, a secure E-commerce protocol is the foundation of E-commerce, the basic characters of the protocol includes: security, secrecy, integrality, authentication, non-repudiation, fairness and etc. Study on formal analysis of E-commerce protocols has profound effects both in theory and realizable application, it's the technical indemnification for E-commerce operation.The current analysis and validation approach for E-commerce protocols are:(1) Practical attacking validating system;(2) Intuitionistic detecting from the exterior;(3) Formal logic analysis system.There are many flaws in the former two, for instance: it's an afterwards checking, and need to be established and executed before checking, the measurements for checking are not strictness enough etc. But the formal logic analysis system can validate it in a credible and strict way before protocol was applied, it is one of the most promising way for protocol checking. The current influential formal analysis methods for E-commerce protocols are BAN logic, Kailar logic, bunch space method, course algebra method and method based on temporal logic etc. Among them, the temporal logic can describe the protocol system by establish the mathematic model, and can provide the corresponding model checking tool to check the characteristics of the protocols automatically, it's very successful on analyzing the finite state space intercurrent protocol system, it has became one of the main analytic tools of formal analyzing of E-commerce.The dissertation mainly studies the applications of logic and model checking methods in formal analysis of E-commerce protocols, especially study on ATL logic method and the application of ATL logic on E-commerce formal analyzing. In general, the author studies the related formal analysis technology of E-commerce protocols from two aspects, theory and applications. The main works and results are as follows:1.Analyzes and discusses the basic theories and characters of E-commerce protocols, includes: security, secrecy, integrity, authentication, non-repudiation, fairness, timeliness and etc. redefine some key significant characters, and bring forward some new rules of E-commerce protocols design.2.Studies the current formal analysis methods for E-commerce protocols based on logic: BAN logic,Kailar logic and Zhou-Qing approach. Use the above methods to analyzing some important protocols, find out its limitations and bring forward a new fair non-repudiation...