乐观公平交换协议形式化逻辑及其自动证明技术

论文摘要

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

论文目录

• 中文摘要
• 英文摘要
• 1 绪论
• 1.1 研究背景
• 1.2 研究内容
• 1.2.1 安全属性
• 1.2.2 安全协议
• 1.2.3 形式化方法
• 1.3 论文主要工作和结构安排
• 1.3.1 论文主要工作
• 1.3.2 论文结构安排
• 1.4 本章小结
• 2 相关背景知识
• 2.1 命题模态逻辑句法和公理系统
• 2.2 克里普克模型
• 2.3 时序逻辑
• 2.3.1 线性时序逻辑
• 2.3.2 计算树逻辑
• 2.4 本章小结
• 3 公平交换协议及其形式化技术研究综述
• 3.1 引言
• 3.2 公平交换协议研究综述
• 3.2.1 公平交换的概念和一般模型
• 3.2.2 公平交换协议分类及主要协议研究
• 3.2.3 公平交换协议安全性定义
• 3.2.4 公平交换协议研究中的主要问题分析
• 3.3 公平交换协议的形式化技术研究综述
• 3.3.1 基于信任逻辑的方法
• 3.3.2 基于模型检测的方法
• 3.3.3 其它方法
• 3.3.4 分析和讨论
• 3.4 本章小结
• 4 乐观公平交换协议形式化逻辑
• 4.1 引言
• 4.2 乐观公平交换协议形式化模型定义
• 4.3 乐观公平交换协议形式逻辑
• 4.3.1 逻辑定义
• 4.3.2 推理公理
• 4.3.3 逻辑描述和正确性证明
• 4.4 案例分析
• 4.4.1 PVG 协议分析
• 4.4.2 JAB 协议分析
• 4.5 分析与比较
• 4.6 本章小结
• 5 乐观公平交换协议自动证明技术
• 5.1 引言
• 5.2 主要问题分析
• 5.3 ISABELLE 定理证明器
• 5.3.1 Isabelle 系统结构
• 5.3.2 Isabelle 的逻辑
• 5.3.3 Isabelle 定理证明方法
• 5.3.4 Isabelle 证明理论
• 5.4 案例分析
• 5.4.1 ASW 协议描述
• 5.4.2 ASW 协议攻击和改进
• 5.4.3 ASW 协议形式化描述
• 5.4.4 ASW 协议分析
• 5.5 相关研究分析
• 5.6 本章小结
• 6 乐观型电子支付协议设计及形式化分析
• 6.1 引言
• 6.2 电子支付协议的密码技术
• 6.2.1 双线性映射理论和困难数学问题及假设
• 6.2.2 部分盲签名机制定义
• 6.2.3 部分盲签名机制安全模型定义
• 6.2.4 部分盲签名算法设计
• 6.2.5 基于椭圆曲线的公钥加密机制
• 6.2.6 基于双线性对的短签名机制
• 6.3 乐观型电子支付协议设计
• 6.4 乐观型电子支付协议分析
• 6.4.1 部分盲签名机制分析
• 6.4.2 电子支付协议安全性分析
• 6.4.3 对比分析
• 6.5 本章小结
• 7 总结与展望
• 7.1 全文总结
• 7.2 进一步研究展望
• 致谢
• 参考文献
• 附录
• A. 作者在攻读学位期间发表的论文目录
• B. 作者在攻读学位期间参与项目情况