基于树自动推理的安全协议自动化检测
| 摘要 | 第1-4页 |
| Abstract | 第4-7页 |
| 第一章 绪论 | 第7-11页 |
| ·安全协议 | 第7-9页 |
| ·基本概念 | 第7页 |
| ·安全性质 | 第7-9页 |
| ·常见攻击 | 第9页 |
| ·安全协议的发展 | 第9-10页 |
| ·论文的研究内容及论文安排 | 第10-11页 |
| 第二章 安全协议形式化分析技术 | 第11-21页 |
| ·概述 | 第11-12页 |
| ·历史与现状 | 第12-13页 |
| ·分类 | 第13-17页 |
| ·形式逻辑 | 第13-14页 |
| ·模型检测 | 第14-16页 |
| ·定理证明 | 第16-17页 |
| ·形式化分析面临的挑战 | 第17-19页 |
| ·形式化分析的贡献 | 第19页 |
| ·本章小结 | 第19-21页 |
| 第三章 树自动机推理技术 | 第21-29页 |
| ·自动机理论 | 第21-22页 |
| ·树自动机推理系统 | 第22-28页 |
| ·基本概念 | 第22-23页 |
| ·项重写系统 | 第23-24页 |
| ·逼近技术 | 第24-28页 |
| ·树自动机的应用 | 第28页 |
| ·本章小结 | 第28-29页 |
| 第四章 树自动机自动检测安全协议 | 第29-47页 |
| ·总体结构 | 第29-30页 |
| ·攻击者模型 | 第30-31页 |
| ·协议建模 | 第31-37页 |
| ·初始树 | 第31-32页 |
| ·重写规则 | 第32-35页 |
| ·逼近规则 | 第35-37页 |
| ·安全目标 | 第37页 |
| ·推理迭代 | 第37-40页 |
| ·结果判定和攻击路径重构 | 第40-43页 |
| ·路径重构方法 | 第40-41页 |
| ·具体过程 | 第41-43页 |
| ·程序设计 | 第43-45页 |
| ·SML 语言 | 第43页 |
| ·底层模块 | 第43-45页 |
| ·本章小结 | 第45-47页 |
| 第五章 LPD-IMSR 协议检测实现 | 第47-57页 |
| ·初始树 | 第47-48页 |
| ·重写规则 | 第48-49页 |
| ·逼近规则 | 第49-50页 |
| ·安全需求 | 第50页 |
| ·检测结果 | 第50-55页 |
| ·分析与改进 | 第55-56页 |
| ·本章小结 | 第56-57页 |
| 第六章 总结与展望 | 第57-59页 |
| 致谢 | 第59-61页 |
| 参考文献 | 第61-65页 |
| 硕士期间发表的论文和参与的科研项目 | 第65-66页 |
