| 摘要 | 第4-6页 |
| Abstract | 第6-7页 |
| 目录 | 第8-10页 |
| 第1章 绪论 | 第10-14页 |
| 1.1 计算机网络安全存在的问题 | 第11-12页 |
| 1.2 论文研究意义 | 第12页 |
| 1.3 论文主要内容及结构 | 第12-14页 |
| 第2章 安全协议及安全协议形式化分析 | 第14-24页 |
| 2.1 安全协议 | 第14-15页 |
| 2.2 安全协议其自身的安全性 | 第15-19页 |
| 2.2.1 安全协议其自身的安全性及攻击分析 | 第15-17页 |
| 2.2.2 安全协议的设计规范 | 第17-18页 |
| 2.2.3 安全协议的安全分析 | 第18-19页 |
| 2.3 形式分析研究与进展 | 第19-23页 |
| 2.3.1 安全协议形式化分析基于逻辑分析的方法 | 第20-21页 |
| 2.3.2 基于模型检测的安全协议分析方法 | 第21-22页 |
| 2.3.3 基于证明的安全协议分析方法 | 第22-23页 |
| 2.4 本章小结 | 第23-24页 |
| 第3章 安全协议自动化验证工具 AVISPA | 第24-29页 |
| 3.1 AVISPA 介绍 | 第24-26页 |
| 3.1.1 AVISPA 工具 | 第25-26页 |
| 3.2 HLPSL 语言及语义 | 第26-28页 |
| 3.2.1 基本角色 | 第26页 |
| 3.2.2 构造角色 | 第26-27页 |
| 3.2.3 变迁 | 第27页 |
| 3.2.4 认证检测 | 第27-28页 |
| 3.2.5 算法操作 | 第28页 |
| 3.3 本章小结 | 第28-29页 |
| 第4章 Yahalom 协议的 AVISPA 分析 | 第29-41页 |
| 4.1 Yahalom 协议简单描述 | 第29-30页 |
| 4.2 用 AVISPA 工具验证 Yahalom 协议安全性 | 第30-38页 |
| 4.2.1 HLPSL 语言表示 | 第30-34页 |
| 4.2.2 Yahalom 协议的协议模拟 | 第34-35页 |
| 4.2.3 Yahalom 协议的攻击模拟 | 第35-38页 |
| 4.3 Yahalom 协议的改进 | 第38-40页 |
| 4.4 本章小结 | 第40-41页 |
| 第5章 总结与展望 | 第41-43页 |
| 5.1 论文总结 | 第41-42页 |
| 5.2 今后展望 | 第42-43页 |
| 参考文献 | 第43-46页 |
| 作者简介 | 第46-47页 |
| 致谢 | 第47页 |