| 摘要 | 第5-7页 |
| ABSTRACT | 第7-8页 |
| 目录 | 第9-11页 |
| 第一章 绪论 | 第11-26页 |
| 1.1 引言 | 第11-12页 |
| 1.2 安全协议 | 第12-14页 |
| 1.2.1 安全协议的种类 | 第12-13页 |
| 1.2.2 形式化分析的意义 | 第13-14页 |
| 1.3 安全属性和安全缺陷 | 第14-16页 |
| 1.3.1 协议的安全属性 | 第15-16页 |
| 1.3.2 协议的安全缺陷 | 第16页 |
| 1.4 形式化分析方法概述 | 第16-19页 |
| 1.4.1 Dolev-Yao 安全模型 | 第17页 |
| 1.4.2 基于知识与信念推理的模态逻辑方法 | 第17-19页 |
| 1.4.3 基于定理证明的方法 | 第19页 |
| 1.5 基于进程演算的形式化分析方法 | 第19-24页 |
| 1.5.1 进程演算 | 第19-21页 |
| 1.5.2 模型检测技术 | 第21-22页 |
| 1.5.3 程序分析技术 | 第22-23页 |
| 1.5.4 互模拟等价技术 | 第23-24页 |
| 1.6 本文研究的内容和成果 | 第24-25页 |
| 1.7 本文结构 | 第25-26页 |
| 第二章 基于 pi 演算的协议分析 | 第26-41页 |
| 2.1 pi 演算基础 | 第26-27页 |
| 2.2 pi 演算的语法 | 第27-29页 |
| 2.3 安全协议的初步抽象 | 第29-31页 |
| 2.4 pi 演算的语义 | 第31-35页 |
| 2.4.1 变迁关系 | 第32-34页 |
| 2.4.2 委托关系 | 第34-35页 |
| 2.5 互模拟等价关系 | 第35-39页 |
| 2.5.1 强互模拟等价关系 | 第35-37页 |
| 2.5.2 强互模拟关系和结构等价 | 第37-38页 |
| 2.5.3 强互模拟关系在置换下的加强 | 第38-39页 |
| 2.5.4 强互模拟关系和 Agent 结构等价 | 第39页 |
| 2.6 结论与相关工作 | 第39-41页 |
| 第三章 基于 Spi 演算的协议分析 | 第41-59页 |
| 3.1 Spi 演算的语法 | 第41-42页 |
| 3.2 安全协议的进一步抽象 | 第42-45页 |
| 3.2.1 协议的 Spi 演算表示 | 第42-44页 |
| 3.2.2 协议规范的 Spi 演算表示 | 第44-45页 |
| 3.3 Spi 演算的语义 | 第45-49页 |
| 3.3.1 反应关系 | 第45-46页 |
| 3.3.2 委托关系 | 第46-47页 |
| 3.3.3 测试等价关系 | 第47-49页 |
| 3.3.4 安全属性的刻画 | 第49页 |
| 3.4 Spi 演算的扩展 | 第49-58页 |
| 3.4.1 非对称密码体系下的 Spi 演算 | 第50-51页 |
| 3.4.2 Spi 演算的消息签名语义 | 第51-53页 |
| 3.4.3 Framed 互模拟关系 | 第53-56页 |
| 3.4.4 barbed 同余关系 | 第56-58页 |
| 3.5 结论与相关工作 | 第58-59页 |
| 第四章 协议验证 | 第59-70页 |
| 4.1 利用 Spi 演算分析 NSSK 协议 | 第59-64页 |
| 4.1.1 NSSK 协议的 Spi 演算表示 | 第60页 |
| 4.1.2 NSSK 协议规范的 Spi 演算表示 | 第60-61页 |
| 4.1.3 对 NSSK 协议攻击的分析 | 第61-64页 |
| 4.2 利用 Spi 演算验证 SSL V3.0 握手协议 | 第64-68页 |
| 4.2.1 SSL V3.0 协议简介 | 第64-65页 |
| 4.2.2 SSL 握手协议的 Spi 演算表示 | 第65-67页 |
| 4.2.3 验证 SSL 握手协议 | 第67-68页 |
| 4.3 结论与相关工作 | 第68-70页 |
| 第五章 总结与展望 | 第70-72页 |
| 5.1 全文总结 | 第70-71页 |
| 5.2 工作展望 | 第71-72页 |
| 参考文献 | 第72-75页 |
| 致谢 | 第75-76页 |
| 攻读硕士学位期间已发表或录用的论文 | 第76-78页 |