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