网络安全协议的高效分析系统
| 摘要 | 第1-4页 |
| ABSTRACT | 第4-7页 |
| 第一章 引言 | 第7-10页 |
| ·研究背景 | 第7-8页 |
| ·论文的主要工作 | 第8-9页 |
| ·论文组织 | 第9-10页 |
| 第二章 安全协议及其分析方法 | 第10-18页 |
| ·安全协议 | 第10-12页 |
| ·安全协议的基本概念 | 第10-11页 |
| ·安全协议的分类 | 第11页 |
| ·安全协议的漏洞 | 第11-12页 |
| ·安全协议的分析方法 | 第12-18页 |
| ·安全协议的非形式化分析 | 第13-15页 |
| ·安全协议形式化分析 | 第15-18页 |
| 第三章 模型检测技术 | 第18-28页 |
| ·模型检测的基本概念 | 第18-20页 |
| ·基本术语 | 第18-19页 |
| ·基本原理 | 第19-20页 |
| ·模型检测工具SPIN | 第20-22页 |
| ·SPIN工作机理 | 第21页 |
| ·Promela语言 | 第21-22页 |
| ·线性时态逻辑(LTL) | 第22页 |
| ·利用SPIN对NS协议进行形式化分析 | 第22-28页 |
| ·建立NS协议的Promela模型 | 第23-26页 |
| ·利用LTL对NS协议性质的描述 | 第26页 |
| ·利用SPIN对NS协议进行验证 | 第26-27页 |
| ·验证效率分析 | 第27-28页 |
| 第四章 安全协议自动分析系统的设计与实现 | 第28-47页 |
| ·系统概述 | 第28-32页 |
| ·系统简介 | 第28-30页 |
| ·系统功能 | 第30-31页 |
| ·系统的特点 | 第31-32页 |
| ·系统实现 | 第32-43页 |
| ·消息数据结构和通道定义 | 第32-33页 |
| ·扩展后的PDL语法 | 第33-36页 |
| ·验证模型自动生成算法 | 第36-43页 |
| ·安全协议实例分析 | 第43-47页 |
| 第五章 系统优化策略 | 第47-53页 |
| ·atomic和d_step | 第47-48页 |
| ·偏序规约 | 第48页 |
| ·语法重定序 | 第48-49页 |
| ·类型检查 | 第49-50页 |
| ·验证效率 | 第50-53页 |
| 第六章 总结与展望 | 第53-55页 |
| ·总结 | 第53页 |
| ·进一步工作方向 | 第53-55页 |
| 致谢 | 第55-56页 |
| 参考文献 | 第56-59页 |
| 攻读学位期间发表的论文 | 第59页 |
