安全协议形式化模型刻画与代数属性研究
| 摘要 | 第1-8页 |
| ABSTRACT | 第8-9页 |
| 第一章 绪论 | 第9-14页 |
| ·论文背景 | 第9页 |
| ·安全协议形式化研究现状 | 第9-12页 |
| ·基于逻辑推理的形式化分析方法 | 第10页 |
| ·基于定理证明的形式化分析方法 | 第10-11页 |
| ·基于模型检测的形式化分析方法 | 第11-12页 |
| ·论文工作 | 第12-13页 |
| ·论文结构安排 | 第13-14页 |
| 第二章 模型刻画问题研究 | 第14-22页 |
| ·MSR模型简介 | 第14-16页 |
| ·基本概念 | 第14-15页 |
| ·重写模型 | 第15-16页 |
| ·执行模型 | 第16页 |
| ·MSR模型扩展 | 第16-21页 |
| ·类型扩展 | 第16-18页 |
| ·安全属性检测 | 第18-21页 |
| ·本章小结 | 第21-22页 |
| 第三章 代数属性问题研究 | 第22-35页 |
| ·项重写理论简介 | 第23-26页 |
| ·基本概念 | 第23-25页 |
| ·项重写系统 | 第25-26页 |
| ·攻击者推演问题分析 | 第26-30页 |
| ·基于TRS的形式化描述 | 第26-27页 |
| ·等价理论划分 | 第27-28页 |
| ·代表元选取 | 第28-30页 |
| ·算法实现 | 第30-34页 |
| ·算法设计 | 第30-32页 |
| ·复杂度分析 | 第32页 |
| ·算法实例研究 | 第32-34页 |
| ·本章小结 | 第34-35页 |
| 第四章 项重写理论终止性分析 | 第35-48页 |
| ·终止性证明 | 第35-37页 |
| ·不可判定性 | 第35页 |
| ·约简序简述 | 第35-36页 |
| ·多项式序 | 第36-37页 |
| ·字典路径序 | 第37页 |
| ·向量序的构建与分析 | 第37-42页 |
| ·向量序构建 | 第38-40页 |
| ·序的对比 | 第40-42页 |
| ·向量序的工程应用 | 第42-46页 |
| ·等价合一问题分析 | 第42-43页 |
| ·算法实现 | 第43-44页 |
| ·算法实例分析 | 第44-46页 |
| ·本章小结 | 第46-48页 |
| 第五章 项重写理论在安全电子交易中的应用 | 第48-54页 |
| ·安全电子交易简述 | 第48-49页 |
| ·形式化建模 | 第49-52页 |
| ·模型基础 | 第49-50页 |
| ·电子交易过程形式化分析 | 第50-52页 |
| ·模型性质与安全属性研究 | 第52-53页 |
| ·完整性与一致性分析 | 第52页 |
| ·安全属性分析 | 第52-53页 |
| ·本章小结 | 第53-54页 |
| 结束语 | 第54-56页 |
| 参考文献 | 第56-59页 |
| 作者简历 攻读硕士学位期间完成的主要工作 | 第59-60页 |
| 致谢 | 第60页 |
