安全协议形式化分析关键问题研究
| 图目录 | 第1-7页 |
| 摘要 | 第7-8页 |
| ABSTRACT | 第8-9页 |
| 第一章 绪论 | 第9-15页 |
| ·课题背景及意义 | 第9-10页 |
| ·国内外研究现状 | 第10-12页 |
| ·三种形式化分析方法 | 第10-11页 |
| ·混合形式化分析方法 | 第11-12页 |
| ·论文工作 | 第12-13页 |
| ·论文结构安排 | 第13-15页 |
| 第二章 基础理论 | 第15-21页 |
| ·项重写系统 | 第15-18页 |
| ·基本概念 | 第15-17页 |
| ·项重写系统 | 第17-18页 |
| ·树自动机 | 第18-20页 |
| ·基本概念 | 第18-19页 |
| ·树自动机与传统字符自动机的比较 | 第19-20页 |
| ·本章小结 | 第20-21页 |
| 第三章 安全协议形式化基础模型 | 第21-30页 |
| ·安全协议形式化分析假设 | 第21-23页 |
| ·完美密码假设 | 第21页 |
| ·自由代数假设 | 第21-22页 |
| ·协议参与者假设 | 第22-23页 |
| ·基于TRS的形式化协议模型 | 第23-26页 |
| ·基于A&B模式的协议描述 | 第23-24页 |
| ·基于TRS的协议形式化描述 | 第24-26页 |
| ·基于TRS和树自动机的攻击者模型 | 第26-29页 |
| ·基于TRS的攻击者能力形式化描述 | 第26-27页 |
| ·基于树自动机的攻击者知识形式化描述 | 第27-29页 |
| ·本章小结 | 第29-30页 |
| 第四章 代数属性问题 | 第30-37页 |
| ·代数属性问题的产生 | 第30-31页 |
| ·代数属性问题的处理 | 第31-34页 |
| ·等式理论 | 第31-32页 |
| ·两类理论 | 第32-33页 |
| ·重写规则 | 第33-34页 |
| ·NSL协议的代数属性处理 | 第34-36页 |
| ·本章小结 | 第36-37页 |
| 第五章 安全属性问题 | 第37-44页 |
| ·认证性 | 第37-41页 |
| ·基于项的认证性描述 | 第37-39页 |
| ·基于树自动机的认证性描述 | 第39-41页 |
| ·秘密性 | 第41-42页 |
| ·基于项的秘密性描述 | 第41页 |
| ·基于树自动机的秘密性描述 | 第41-42页 |
| ·NSL协议的安全属性处理 | 第42页 |
| ·本章小结 | 第42-44页 |
| 第六章 基于攻击者知识的安全协议形式化分析与检测 | 第44-55页 |
| ·方法概述 | 第44-45页 |
| ·主要思想 | 第44-45页 |
| ·方法流程 | 第45页 |
| ·攻击者知识分析 | 第45-49页 |
| ·非左线性TRS | 第45-47页 |
| ·转移规则标准化 | 第47-48页 |
| ·自动化算法 | 第48-49页 |
| ·安全协议形式化分析检测 | 第49-50页 |
| ·认证性检测 | 第49-50页 |
| ·秘密性检测 | 第50页 |
| ·NSL协议的分析检测实例 | 第50-54页 |
| ·本章小结 | 第54-55页 |
| 结束语 | 第55-57页 |
| 参考文献 | 第57-60页 |
| 作者简历 攻读硕士学位期间完成的主要工作 | 第60-61页 |
| 致谢 | 第61页 |
