【作者】 文静华；

【导师】 李祥；

【作者基本信息】 贵州大学 ， 计算机软件与理论， 2006， 博士

【摘要】 电子商务协议形式化分析是电子商务研究的一个重要方面，电子商务协议是面向电子商务的密码协议，安全的电子商务协议是保证电子商务活动正常开展的基础，其基本属性包括安全性、保密性、完整性、可认证性、非否认性及公平性等。进行电子商务协议的形式化分析研究具有重大理论意义和现实的应用价值，是顺利开展电子商务应用的技术保障。 目前国内外对电子商务协议的分析验证手段主要有以下几种： (1)实际攻击验证方法； (2)从表面上进行直观检测； (3)形式化逻辑分析方法。 前两种方法存在较多缺点，如：属于事后检测，需在协议建立实施之后才能进行检测、检测手段不够严密等。而形式化逻辑分析方法可以在协议实施之前就用严格可靠的方法对其进行分析验证，是一个最有前途的研究方法。目前在各种电子商务协议形式化分析方法研究中，有影响的方法主要有BAN逻辑方法、Kailar逻辑方法、串空间方法、进程代数方法及基于时序逻辑的方法等。其中，时序逻辑方法能够通过建立数学模型来描述协议系统，可提供相应的模型检测工具对协议性质进行自动验证，对状态空间有限的并发协议系统分析尤为成功，已成为对电子商务协议进行形式化分析的主要工具之一。 本文主要对基于逻辑的形式化方法与模型检测技术及其在电子商务协议形式化分析中的应用进行了系统研究，重点对ATL逻辑方法及其在电子商务协议并形式化分析中的应用进行了研究。总的来说，从理论到实践两个层面上研究了电子商务协议的形式化分析的相关技术，其工作主要有以下几个方面： 1．对电子商务协议的基本理论和基本性质进行了分析和讨论，包括：安全性、保密性、完整性、可认证性、非否认性、公平性、时效性等，并对其中一些重要性质做新的定义，提出电子商务协议设计的基本准则。 2．对当前流行的基于逻辑的电子商务协议形式化分析方法进行重点研究，包括BAN逻辑、Kailar逻辑及周一卿方法。采用这些较新的形式化分析方法对几个典型协议进行分析，找出设计缺陷并提出新的公平非否认性协议。更多还原

【Abstract】 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更多还原