论文摘要
公平非否认协议可以防止通信主体对通信事件的抵赖行为并保证通信各方始终处于公平地位,是安全电子商务协议的基础。由于公平非否认协议的重要性,对它的各项安全性质进行分析是近十年来安全领域的研究热点。目前,国内外已提出了一些适用于分析公平非否认协议的形式化方法,这些方法主要分为三类:基于知识与信念的逻辑证明方法;基于模型化技术的状态搜索方法;基于定理证明的方法。这些分析方法或工具往往能分析公平非否认协议是否满足某个或某些性质,但目前还没有一种可以同时分析公平非否认协议非否认性、公平性及时限性的方法。鉴于安全协议各个安全性质的微妙相关性,单独分析某个或某些性质是不科学的。而在公平非否认协议中,非否认性、公平性和时限性是三个紧密相关和互相影响的性质,分析公平非否认协议性能时,忽略对任何一个性质的考虑,都可能使分析结果变得毫无意义。本文针对上述问题,通过深入研究公平非否认协议的相关安全性质的本质,在总结现有分析方法优缺点的基础上,提出了一种可同时分析公平非否认协议非否认性、公平性和时限性的方法。主要工作如下:1.深入研究了公平非否认协议的非否认性、公平性与时限性三个安全性质的本质。分析了目前应用于公平非否认协议分析的若干主要方法的原理、优缺点和应用范围。2.提出了一种基于可证性逻辑的,能同时分析非否认性、公平性与时限性的形式化分析方法。新方法对主体引入限时能力概念,使用“逐步断开,其余主体继续”的分析方案,并假设了一个攻击者能力集合,能全面地分析非否认性、公平性和时限性。使用新方法分析了若干典型的公平非否认协议,找到了一些已知的和未知的漏洞,验证了新方法的有效性。3.使用新方法验证了SET协议中的购买流程协议,有效地分析了该协议的非否认性、公平性和时限性。
论文目录
摘要ABSTRACT第一章 绪论1.1 公平非否认协议概述1.1.1 公平非否认协议的定义1.1.2 公平非否认协议的分类1.2 公平非否认协议分析的历史研究及现状1.2.1 一般安全协议分析方法的研究1.2.2 公平非否认协议分析方法的研究1.3 本课题的研究意义及成果1.4 论文的组织结构第二章 公平非否认协议形式化分析的基础问题2.1 对密码技术的假设2.2 攻击者模型假设2.3 信道的假设2.4 安全协议的若干安全性质2.5 本章小结第三章 公平非否认协议的形式化分析3.1 关于公平非否认协议若干安全性质的进一步说明3.1.1 非否认性3.1.2 可追究性3.1.3 公平性3.1.4 时限性3.1.5 非滥用性3.2 TTP 类型3.3 几个经典公平非否认协议3.3.1 使用Inline TTP 的公平非否认协议示例3.3.2 使用Online TTP 的公平非否认协议示例3.3.3 使用Offline TTP 的公平非否认协议示例3.4 适用于分析公平非否认协议的几个工具3.4.1 基于进程代数的方法3.4.2 SVO 逻辑3.4.3 Kailar 逻辑3.4.4 MurΦ模型检测3.4.5 基于Game 模型的方法3.4.6 SPIN 方法3.4.7 APA 方法3.4.8 基于定理证明的方法3.4.9 使用高阶协议描述语言HLPSL3.4.10 其他分析方法3.4.11 各类用于公平非否认协议分析的方法总结3.5 本章小结第四章 一种新的针对公平非否认协议的形式化分析方法4.1 一种新的针对非否认协议的形式化分析方法4.1.1 分析过程用到的新增符号4.1.2 相关概念和定义4.1.3 假设条件4.1.4 推理规则4.1.5 分析步骤4.2 分析实例4.2.1 分析Zhou-Gollmann 协议4.2.2 分析Zhou-Gollman 协议改进版本一4.2.3 分析Zhou-Gollmann 协议改进版本二4.3 有效性分析4.3.1 新方法可有效分析非否认4.3.2 新方法可有效分析公平性4.3.3 新方法可有效分析时限性4.4 相对于原来分析方法的改进4.5 本章小结第五章 应用新方法分析SET 协议5.1 SET 协议介绍5.1.1 SET 协议参与方简介5.1.2 SET 协议通信过程5.1.3 SET 交易过程5.2 应用新方法分析SET 协议的购买过程协议5.2.1 购买过程协议5.2.2 分析过程5.2.3 分析结果小结5.3 本章小结第六章 总结6.1 主要工作总结6.2 展望致谢参考文献在学期间研究成果
相关论文文献
标签：公平非否认协议论文; 可证性逻辑论文; 协议分析方法论文; 协议分析论文;
