【作者】 陈明；

【导师】 徐洁； 吴中福；

【作者基本信息】 重庆大学 ， 计算机科学与技术， 2011， 博士

【摘要】 随着Internet的日益发展与普及,电子信息交换已成为现代经济生活的主要形式之一,它是在任意两个互不信任的主体之间以一种公平的方式来交换电子数据。实现公平电子信息交换的协议被称为公平交换协议,公平性成为这类型协议的基本安全属性,目标是实现数据交换而又不会使一方比另一方有获取更多信息的优势,促使互不信任的合作伙伴公平完成交换。公平交换协议是一类重要的安全协议,而其设计是一个众所周知的难题,常常因为一些细微的问题产生安全缺陷。目前已有一些分析公平交换协议的形式化方法,最典型和得到广泛应用的是信任逻辑方法。许多研究者采用扩展的信任逻辑方法成功分析了在线可信第三方公平交换协议的不可否认性。由于信任逻辑方法自身固有的缺陷,难以用于分析乐观型公平交换协议的公平性和时限性等性质。乐观型公平交换协议是目前公平交换协议研究领域的热点之一,是一种兼顾公平和效率的公平交换协议形式。在乐观型公平交换协议中,可信第三方不再直接参与数据交换,只需要扮演争端解决者的角色。交易过程中对可信第三方的请求次数远远低于其它类型的公平交换协议,避免了针对可信第三方的拒绝服务攻击。但是,乐观型公平交换协议引入了分支协议结构,协议执行存在多种可能结果,使得对该类型协议的形式化分析更加复杂和困难。本文研究工作围绕乐观型公平交换协议及其形式化分析技术展开,主要包括三方面内容:第一,对公平交换协议及其形式化技术进行研究综述;第二,研究乐观公平交换协议形式化模型、逻辑及其自动证明技术;第三,研究乐观公平交换协议在电子商务中的应用和实现技术。论文主要工作和创新性成果如下:1.对公平交换协议的基本理论和基本性质进行综述和分析,对其中一些重要性质进行重新定义,如公平性等。2.对主要的公平交换协议形式化分析方法进行综述性研究,讨论各种方法的优缺点及其存在的问题。3.提出一种新的乐观公平交换协议形式化模型,将信道错误转化为攻击行为,将协议参与者分为诚实与不诚实两类,将入侵者与不诚实参与者的共谋归结为两类Dolev-Yao入侵者。新模型不再单独考虑信道错误,简化了问题空间。4.提出一种乐观公平交换协议形式化逻辑。新逻辑采用信任逻辑的句法结构,定义乐观公平交换协议为具有Kripke语义结构的演化系统。案例分析显示,新逻辑被成功用于分析乐观型公平交换协议的公平性和时限性。5.基于自动定理证明器Isabelle,研究实现本文模型和逻辑的自动定理证明技术。采用Paulson归纳法实现更为主动的攻击者,将攻击者主动获取知识的能力描述为对消息进行解析和组合的归纳函数。将信道假设对应为不诚实参与者的行为,以降低协议模拟的复杂度。6.提出双授权部分盲签名概念,解决电子支付中银行经理滥用职权恶意签发电子钱币的问题。设计实现采用双授权的部分盲签名机制,在随机预言机模型下证明新签名机制是安全的。对比分析表明,新机制具有较高的计算性能。7.提出新的乐观型电子支付协议。新协议采用双授权部分盲签名机制,同时实现电子现金离线支付(支付阶段无须银行在线支持)和乐观型公平交换。具有复杂结构的安全协议形式化技术研究正在蓬勃发展,本文研究工作对促进这一研究领域发展和电子商务安全具有一定的理论和实用意义。更多还原

【Abstract】 With the increasing development of Internet, Internet-based electronic information exchange has become one of major forms of modern economic life. Electronic information exchange switches electronic data in a fair way between two un-trusted entities. A protocol achieving fair exchange of electronic information is known as a fair exchange protocol. Fairness is the basic security property of fair exchange protocols. The goal of a fair exchange protocol is to achieve the data exchange and not to leave any advantages over parties, and urges two un-trusted partners to complete a fair exchange.As is known to all, a secure security protocol designing is hard. A slight fault may even drive great flaws. Fair exchange protocol is of an important security protocol. So far, there are some formal methods for analyzing fair exchange protocols. The widely used method is the belief logic. Many researchers using the extended belief logic method successfully analyzed the non-repudiation of some online trusted third party fair exchange protocols. For the inherent defects in the belief logic method, it is difficult to analyze the fairness, timeliness and other properties of optimistic fair exchange protocol.Currently, the analyzing and designing of optimistic fair exchange protocol is one of the hottest research fields. The optimistic fair exchange protocol keeps a balance between fairness and efficiency. In the optimistic fair exchange protocol, the trusted third party only plays the arbiter instead of directly involving in the process of data exchange. So, during the transaction process, the number of requesting on the trusted third party is much lower than those of other types of fair exchange protocol, which avoids denial service attacks on the trusted third party. However, the optimistic fair exchange protocol leads to a branch structure, and there are several possible outcomes which make the protocols’formal analysis turns to be more complex and difficult.This dissertation studies the optimistic fair exchange protocol and its formal analysis techniques, including three following aspects: first, a literature review of fair exchange protocols and their formal techniques; second, a research of formal model, logic and automatic proof techniques of optimistic fair exchange protocols; third, a study of security and applications techniques of optimistic fair exchange protocols in e-commerce. The main study and innovative results of this dissertation are as follows:1. Basic theories and properties of fair exchange protocols are reviewed and analyzed, and some important properties are re-defined, such as fairness and the like. 2. The main methods of formal analysis of fair exchange protocols are reviewed, and the advantages, disadvantages and problems of each method are discussed as well.3. A new formal model of optimistic fair exchange protocols is proposed. The new formal model turns channel errors into channel attacks, divides the protocol participants into honesty ones and dishonesty ones, and attributes the conspiracy between intruders and dishonest participants as two types of Dolev-Yao intruders. Case analysis shows that the new model simplifies the problem space.4. A formal logic of optimistic fair exchange protocols is proposed. The new logic adopts the syntax structure of the belief logic, and defines optimistic fair exchange protocols as the evolution system with the Kripke semantic structure. Case analysis shows that the new logic has been successfully used to analyze the fairness and timeliness of optimistic fair exchange protocols.5. Based on Isabelle, an interactive theorem proving framework, the automatic theorem proving technology of logics and models in this dissertation are achieved. A more active attacker is achieved using Paulson induction, and the ability of the attacker to acquire knowledge initiatively is described as the inductive function to parsing and combining messages. The channel assuming is modeled as the behaviors of dishonest participants in order to reduce the complexity of the simulation protocol.6. The concept of dual authorizing in partially blind signature is put forward, which solves a problem, that is, bank manager in the abuse of power maliciously issues e-coins in electronic payments. A scheme of partially blind signature with dual authorizing is designed, and its security is proved under the random oracle model. Comparative analysis shows that the new mechanism has a high computational performance.7. A new optimistic electronic payment protocol is introduced. The scheme of partially blind signature with dual authorizing is employed, while off-line electronic cash payments (no need of online bank payment support) and optimistic fair exchange are achieved.The studies of formal technology in security protocols with the complex structure and e-commerce security are booming. There are some theoretical and practical significance in this dissertation for promoting those research fields.更多还原