基于规划的密码协议自动化验证技术研究
| 摘要 | 第1-8页 |
| ABSTRACT | 第8-10页 |
| 第一章 绪论 | 第10-20页 |
| ·研究背景及意义 | 第10-11页 |
| ·课题背景 | 第10页 |
| ·课题意义 | 第10-11页 |
| ·相关研究现状 | 第11-17页 |
| ·密码协议形式化分析技术研究 | 第11-13页 |
| ·密码协议自动化验证系统研究 | 第13-16页 |
| ·智能规划的研究 | 第16-17页 |
| ·论文主要工作 | 第17-18页 |
| ·论文结构安排 | 第18-20页 |
| 第二章 基于规划理论的密码协议形式模型研究 | 第20-41页 |
| ·基本假设 | 第21页 |
| ·运行环境假设 | 第21页 |
| ·完美加密假设 | 第21页 |
| ·强类型假设 | 第21页 |
| ·语法及基本语义 | 第21-24页 |
| ·项 | 第22-23页 |
| ·文字 | 第23-24页 |
| ·操作 | 第24页 |
| ·密码协议攻击规划理论 | 第24-26页 |
| ·密码协议攻击规划系统 | 第24-25页 |
| ·密码协议攻击规划问题 | 第25-26页 |
| ·密码协议攻击规划问题模型 | 第26-39页 |
| ·关于协议规范的建模 | 第27-29页 |
| ·关于攻击者的建模 | 第29-35页 |
| ·关于安全性的建模 | 第35-38页 |
| ·对NS公钥协议的分析 | 第38-39页 |
| ·完备性讨论 | 第39-40页 |
| ·本章小结 | 第40-41页 |
| 第三章 密码协议安全性验证机制研究 | 第41-50页 |
| ·相关概念 | 第41-45页 |
| ·偏序规划 | 第42-43页 |
| ·规划图 | 第43-44页 |
| ·SAT问题 | 第44-45页 |
| ·密码协议攻击规划问题求解机制 | 第45-46页 |
| ·SAT编码的基本准则 | 第46-49页 |
| ·准则描述 | 第47页 |
| ·正确性证明 | 第47-49页 |
| ·本章小结 | 第49-50页 |
| 第四章 密码协议安全性验证算法研究 | 第50-66页 |
| ·设计思想 | 第50-51页 |
| ·算法总体描述 | 第51-52页 |
| ·关键子算法 | 第52-65页 |
| ·规划图扩展算法 | 第52-55页 |
| ·SAT编码算法 | 第55-60页 |
| ·SAT求解算法 | 第60-65页 |
| ·本章小结 | 第65-66页 |
| 第五章 ACPV原型系统的总体设计 | 第66-75页 |
| ·系统需求 | 第66-67页 |
| ·功能需求 | 第66-67页 |
| ·性能需求 | 第67页 |
| ·设计思想 | 第67-68页 |
| ·体系结构 | 第68-69页 |
| ·工作原理 | 第69-71页 |
| ·功能与结构 | 第71-74页 |
| ·系统输入部分 | 第71-73页 |
| ·安全性验证部分 | 第73-74页 |
| ·系统输出部分 | 第74页 |
| ·本章小结 | 第74-75页 |
| 第六章 ACPV原型系统的实现 | 第75-85页 |
| ·密码协议形式描述语言 | 第75-78页 |
| ·语法规则 | 第75-77页 |
| ·描述实例 | 第77-78页 |
| ·系统输入部分的实现 | 第78-79页 |
| ·编辑器模块的实现机制 | 第78-79页 |
| ·编译器模块的实现机制 | 第79页 |
| ·安全性验证部分的实现 | 第79-83页 |
| ·相关类定义 | 第79-82页 |
| ·系统运行参数 | 第82-83页 |
| ·安全性验证过程 | 第83页 |
| ·系统输出部分的实现 | 第83页 |
| ·系统实验结果与分析 | 第83-84页 |
| ·本章小结 | 第84-85页 |
| 第七章 结束语 | 第85-86页 |
| 参考文献 | 第86-92页 |
| 作者简历 攻读硕士学位期间完成的主要工作 | 第92-93页 |
| 致谢 | 第93页 |
