| 摘要 | 第1-5页 |
| ABSTRACT | 第5-6页 |
| 1 前言 | 第6-9页 |
| ·课题研究背景和意义 | 第6-7页 |
| ·研究的目标、内容和方案 | 第7-8页 |
| ·本文的结构安排 | 第8-9页 |
| 2 安全协议及其形式化分析 | 第9-21页 |
| ·安全协议 | 第9-12页 |
| ·协议与安全协议 | 第9页 |
| ·安全协议的安全属性 | 第9-11页 |
| ·安全协议的缺陷 | 第11-12页 |
| ·安全协议的形式化分析 | 第12-21页 |
| ·形式化方法概述 | 第12页 |
| ·形式化分析涵义 | 第12-13页 |
| ·安全协议形式化分析思路 | 第13-14页 |
| ·基本假设 | 第14-15页 |
| ·形式化分析方法的现状 | 第15-19页 |
| ·安全协议形式化分析的热点研究方向和发展趋势 | 第19-21页 |
| 3 串空间模型理论及其协议分析方法 | 第21-33页 |
| ·串空间模型理论的基础知识 | 第21-27页 |
| ·消息空间和代数假定 | 第21-22页 |
| ·基本概念 | 第22-23页 |
| ·丛和结点关系 | 第23-25页 |
| ·攻击者描述 | 第25-26页 |
| ·协议正确性的含义 | 第26-27页 |
| ·协议描述 | 第27页 |
| ·理想与诚实理论 | 第27-28页 |
| ·理想 | 第27页 |
| ·诚实 | 第27-28页 |
| ·认证测试理论 | 第28-31页 |
| ·基本概念 | 第29-30页 |
| ·三种重要的认证测试方法 | 第30页 |
| ·认证测试规则 | 第30-31页 |
| ·基于串空间模型3种典型的安全协议形式化分析方法 | 第31-33页 |
| ·基于极小元理论的串空间方法 | 第31页 |
| ·基于理想与诚实理论的串空间方法 | 第31-32页 |
| ·基于认证测试理论的串空间方法 | 第32-33页 |
| 4 基于串空间模型几个典型协议的形式化分析 | 第33-62页 |
| ·基于极小元理论 NSL协议的形式化分析 | 第33-41页 |
| ·NSL 协议串空间 | 第33-34页 |
| ·NSL 协议响应者的认证性 | 第34-38页 |
| ·NS 协议的脆弱性分析 | 第38页 |
| ·NSL 协议响应者的秘密性 | 第38-40页 |
| ·NSL 协议发起者的秘密性 | 第40页 |
| ·NSL 协议发起者的认证性 | 第40-41页 |
| ·基于理想与诚实理论 Yahalom 改进协议的形式化分析 | 第41-49页 |
| ·Yahalom 协议串空间 | 第42-44页 |
| ·秘密性 | 第44-45页 |
| ·认证性分析 | 第45-49页 |
| ·基于认证测试理论 X.509 三消息改进协议的形式化分析 | 第49-53页 |
| ·X.509 三消息改进协议的串空间 | 第50页 |
| ·发起者对响应者的认证性 | 第50-52页 |
| ·响应者对发起者的认证性 | 第52-53页 |
| ·基于认证测试理论 Yahalom 改进协议的形式化分析 | 第53-57页 |
| ·基于认证测试理论 NSL 协议的形式化分析 | 第57-60页 |
| ·方法总结与对比分析 | 第60-62页 |
| ·与非串空间方法的对比分析 | 第60-61页 |
| ·三种串空间形式化方法的特点与异同 | 第61-62页 |
| 5 总结与展望 | 第62-64页 |
| ·研究总结 | 第62-63页 |
| ·进一步的工作 | 第63-64页 |
| 致谢 | 第64-65页 |
| 参考文献 | 第65-68页 |
| 附录 | 第68-69页 |
