网络安全认证协议自动分析系统
| 摘要 | 第1-4页 |
| ABSTRACT | 第4-7页 |
| 第一章 引言 | 第7-11页 |
| ·研究背景 | 第7-8页 |
| ·研究思路 | 第8-9页 |
| ·论文组织 | 第9-11页 |
| 第二章 安全协议及其分析方法 | 第11-20页 |
| ·安全协议 | 第11-14页 |
| ·安全协议的概念 | 第11-12页 |
| ·安全协议的历史 | 第12-14页 |
| ·安全协议的分类 | 第14页 |
| ·安全协议的分析方法 | 第14-20页 |
| ·安全协议的非形式化分析 | 第14-16页 |
| ·安全协议形式化分析 | 第16-20页 |
| 第三章 模型检测及相关技术 | 第20-31页 |
| ·模型检测 | 第20-21页 |
| ·几个重要的术语 | 第21-22页 |
| ·模型检测工具SPIN | 第22-23页 |
| ·模型检测工具对网络认证协议的安全性分析 | 第23-25页 |
| ·Promela对认证协议的建模 | 第24页 |
| ·时态逻辑 | 第24-25页 |
| ·验证 | 第25页 |
| ·利用SPIN对N-S协议进行形式化的分析 | 第25-31页 |
| ·套用Promela对认证协议建模的五个步骤 | 第25-30页 |
| ·利用LTL对N-S协议性质的描述 | 第30页 |
| ·利用SPIN对N-S协议进行验证 | 第30-31页 |
| 第四章 网络安全认证协议自动分析系统的设计 | 第31-52页 |
| ·网络安全认证协议自动分析系统概述 | 第31-35页 |
| ·系统简介 | 第31-34页 |
| ·系统功能 | 第34-35页 |
| ·系统实现 | 第35-52页 |
| ·整体设计 | 第35-36页 |
| ·模块设计 | 第36-52页 |
| 第五章 系统特点及其优化策略 | 第52-61页 |
| ·系统描述语言PDL | 第52-55页 |
| ·效率性 | 第55页 |
| ·自动化设计 | 第55页 |
| ·功能可扩展性 | 第55-56页 |
| ·用户界面设计 | 第56页 |
| ·解决状态爆炸问题之策略 | 第56-61页 |
| ·atomic和steps | 第56-57页 |
| ·顺序重定向 | 第57-58页 |
| ·缩减随机数变量的取值范围 | 第58-59页 |
| ·偏序规约技术 | 第59-61页 |
| 第六章 其它相关工作 | 第61-67页 |
| ·认证逻辑 | 第61-63页 |
| ·FDR | 第63页 |
| ·MURφ | 第63-64页 |
| ·NRL | 第64-65页 |
| ·ATHENA | 第65-66页 |
| ·ISBELL | 第66-67页 |
| 第七章 结论与展望 | 第67-70页 |
| ·结论 | 第67-68页 |
| ·进一步工作方向 | 第68-70页 |
| 致谢 | 第70-71页 |
| 参考文献 | 第71-76页 |
| 攻读学位期间的研究成果 | 第76页 |
