基于增量式可满足性求解的安全协议形式化验证方法
| 致谢 | 第1-6页 |
| 摘要 | 第6-7页 |
| ABSTRACT | 第7-10页 |
| 1 引言 | 第10-14页 |
| ·课题研究的目的和意义 | 第10-11页 |
| ·课题研究的现状 | 第11-12页 |
| ·课题研究的主要内容 | 第12-13页 |
| ·论文的结构 | 第13-14页 |
| 2 安全协议 | 第14-22页 |
| ·安全协议的安全属性及实现 | 第14页 |
| ·安全协议的分类 | 第14-15页 |
| ·安全协议的设计规范与准则 | 第15-16页 |
| ·安全协议的缺陷及其分类 | 第16-18页 |
| ·一些攻击实例及其防范 | 第18-22页 |
| 3 安全协议的形式化分析理论 | 第22-37页 |
| ·形式化分析所面临的问题 | 第22-23页 |
| ·安全协议形式化分析方法的分类 | 第23-24页 |
| ·形式逻辑方法 | 第24-28页 |
| ·BAN逻辑 | 第24-26页 |
| ·BAN逻辑的改进 | 第26-27页 |
| ·其他的一些逻辑 | 第27-28页 |
| ·模型检验方法 | 第28-31页 |
| ·CSP和FDR模型检验技术 | 第28-30页 |
| ·Mur (?)模型检验技术 | 第30-31页 |
| ·其它模型检验技术 | 第31页 |
| ·定理证明方法 | 第31-37页 |
| ·Paulson归纳法 | 第31-33页 |
| ·串空间方法 | 第33-35页 |
| ·其它定理证明方法 | 第35-37页 |
| 4 基于增量式SAT的形式化验证方法的设计 | 第37-41页 |
| ·设计思想 | 第37-39页 |
| ·研究内容 | 第39页 |
| ·ISAT-compiler功能的设计 | 第39-40页 |
| ·ISAT-solving功能的设计 | 第40-41页 |
| 5 安全协议的增量式SAT编码过程的实现 | 第41-51页 |
| ·NSPK模型及其攻击实例 | 第41-42页 |
| ·协议的不安全问题 | 第42-43页 |
| ·协议不安全问题的形式化表述 | 第43-45页 |
| ·协议不安全问题到SAT问题的转化 | 第45-49页 |
| ·增量式SAT-compiler算法描述 | 第49-50页 |
| ·输出文件格式 | 第50-51页 |
| 6 增量式可满足性求解方法的实现 | 第51-67页 |
| ·增量式SAT问题及相关公理 | 第51-52页 |
| ·ISAT的语法规则和表达格式 | 第52-54页 |
| ·增量式SAT的研究内容 | 第54-56页 |
| ·增量式SAT求解中的关键技术 | 第56-63页 |
| ·预处理过程 | 第56-57页 |
| ·变量的选取 | 第57页 |
| ·推理过程 | 第57-59页 |
| ·冲突分析 | 第59-61页 |
| ·增加语句和删除语句的处理 | 第61-63页 |
| ·增量式SAT-solving算法描述 | 第63-64页 |
| ·实验数据与分析 | 第64-67页 |
| 7 结论 | 第67-68页 |
| 参考文献 | 第68-70页 |
| 作者简历 | 第70-72页 |
| 学位论文数据集 | 第72页 |
