| 摘要 | 第1-4页 |
| Abstract | 第4-8页 |
| 第一章 绪论 | 第8-12页 |
| ·课题研究背景 | 第8-9页 |
| ·课题研究意义 | 第9-10页 |
| ·本文工作 | 第10-12页 |
| 第二章 安全协议形式化分析综述 | 第12-21页 |
| ·密码学概述 | 第12-14页 |
| ·密码学简介 | 第12-13页 |
| ·密码学基本概念 | 第13页 |
| ·密码体制的特点 | 第13-14页 |
| ·安全协议的概念和安全性质 | 第14-17页 |
| ·安全协议的形式化分析 | 第17-21页 |
| ·安全协议分析的困难性 | 第17-18页 |
| ·安全协议分析的基本假定 | 第18页 |
| ·安全协议形式化分析方法分类 | 第18-21页 |
| 第三章 串空间理论模型及其应用研究 | 第21-33页 |
| ·串空间基本概念 | 第21-24页 |
| ·基本概念 | 第21-23页 |
| ·攻击者模型 | 第23-24页 |
| ·认证协议的一致性属性 | 第24页 |
| ·利用串空间理论分析MY-Helsinki协议 | 第24-30页 |
| ·MY-Helsinki协议描述 | 第24-25页 |
| ·MY-Helsinki协议分析 | 第25-30页 |
| ·理想和诚实 | 第30-31页 |
| ·理想 | 第30-31页 |
| ·入口点和诚实 | 第31页 |
| ·运用理想分析Weakened-Yahalom协议的认证性 | 第31-33页 |
| 第四章 认证测试及其应用研究 | 第33-40页 |
| ·基本概念 | 第33-34页 |
| ·转换边和已转换边 | 第34页 |
| ·认证测试 | 第34-36页 |
| ·运用认证测试分析Weakened-Yahalom协议的认证性 | 第36-38页 |
| ·理想和认证测试方法分析Weakened-Yahalom协议比较 | 第38-40页 |
| 第五章 动态串空间模型及其算法研究 | 第40-53页 |
| ·动态串空间概念 | 第40-42页 |
| ·状态空间消减规则 | 第42-43页 |
| ·结点绑定算法的改进 | 第43-46页 |
| ·丛扩展规则的增加 | 第46-47页 |
| ·实例分析 | 第47-53页 |
| ·Needham-Schroeder-Lowe协议分析 | 第47-50页 |
| ·BAN-Yahalom协议分析 | 第50-53页 |
| 第六章 总结 | 第53-54页 |
| 参考文献 | 第54-58页 |
| 致谢 | 第58-59页 |
| 附录1 攻读硕士学位期间发表的论文 | 第59页 |
