| 摘要 | 第1-5页 |
| ABSTRACT | 第5-13页 |
| 第一章 绪论 | 第13-22页 |
| ·公平非否认协议概述 | 第13-15页 |
| ·公平非否认协议的定义 | 第13-14页 |
| ·公平非否认协议的分类 | 第14-15页 |
| ·公平非否认协议分析的历史研究及现状 | 第15-20页 |
| ·一般安全协议分析方法的研究 | 第15-18页 |
| ·公平非否认协议分析方法的研究 | 第18-20页 |
| ·本课题的研究意义及成果 | 第20-21页 |
| ·论文的组织结构 | 第21-22页 |
| 第二章 公平非否认协议形式化分析的基础问题 | 第22-27页 |
| ·对密码技术的假设 | 第22-23页 |
| ·攻击者模型假设 | 第23页 |
| ·信道的假设 | 第23-24页 |
| ·安全协议的若干安全性质 | 第24-25页 |
| ·本章小结 | 第25-27页 |
| 第三章 公平非否认协议的形式化分析 | 第27-40页 |
| ·关于公平非否认协议若干安全性质的进一步说明 | 第27-29页 |
| ·非否认性 | 第27-28页 |
| ·可追究性 | 第28页 |
| ·公平性 | 第28-29页 |
| ·时限性 | 第29页 |
| ·非滥用性 | 第29页 |
| ·TTP 类型 | 第29-30页 |
| ·几个经典公平非否认协议 | 第30-34页 |
| ·使用Inline TTP 的公平非否认协议示例 | 第30-31页 |
| ·使用Online TTP 的公平非否认协议示例 | 第31-32页 |
| ·使用Offline TTP 的公平非否认协议示例 | 第32-34页 |
| ·适用于分析公平非否认协议的几个工具 | 第34-39页 |
| ·基于进程代数的方法 | 第34页 |
| ·SVO 逻辑 | 第34-35页 |
| ·Kailar 逻辑 | 第35-36页 |
| ·MurΦ模型检测 | 第36页 |
| ·基于Game 模型的方法 | 第36页 |
| ·SPIN 方法 | 第36-37页 |
| ·APA 方法 | 第37页 |
| ·基于定理证明的方法 | 第37-38页 |
| ·使用高阶协议描述语言HLPSL | 第38页 |
| ·其他分析方法 | 第38页 |
| ·各类用于公平非否认协议分析的方法总结 | 第38-39页 |
| ·本章小结 | 第39-40页 |
| 第四章 一种新的针对公平非否认协议的形式化分析方法 | 第40-61页 |
| ·一种新的针对非否认协议的形式化分析方法 | 第40-46页 |
| ·分析过程用到的新增符号 | 第40-41页 |
| ·相关概念和定义 | 第41-43页 |
| ·假设条件 | 第43页 |
| ·推理规则 | 第43-45页 |
| ·分析步骤 | 第45-46页 |
| ·分析实例 | 第46-58页 |
| ·分析Zhou-Gollmann 协议 | 第46-50页 |
| ·分析Zhou-Gollman 协议改进版本一 | 第50-54页 |
| ·分析Zhou-Gollmann 协议改进版本二 | 第54-58页 |
| ·有效性分析 | 第58-59页 |
| ·新方法可有效分析非否认 | 第58页 |
| ·新方法可有效分析公平性 | 第58页 |
| ·新方法可有效分析时限性 | 第58-59页 |
| ·相对于原来分析方法的改进 | 第59-60页 |
| ·本章小结 | 第60-61页 |
| 第五章 应用新方法分析SET 协议 | 第61-74页 |
| ·SET 协议介绍 | 第61-68页 |
| ·SET 协议参与方简介 | 第61-62页 |
| ·SET 协议通信过程 | 第62-63页 |
| ·SET 交易过程 | 第63-68页 |
| ·应用新方法分析SET 协议的购买过程协议 | 第68-73页 |
| ·购买过程协议 | 第68-69页 |
| ·分析过程 | 第69-72页 |
| ·分析结果小结 | 第72-73页 |
| ·本章小结 | 第73-74页 |
| 第六章 总结 | 第74-75页 |
| ·主要工作总结 | 第74页 |
| ·展望 | 第74-75页 |
| 致谢 | 第75-76页 |
| 参考文献 | 第76-82页 |
| 在学期间研究成果 | 第82-83页 |