密码协议的形式化分析方法研究
| 摘要 | 第1-9页 |
| Abstract | 第9-12页 |
| 第一章 绪论 | 第12-23页 |
| ·概述 | 第12页 |
| ·密码协议的安全性 | 第12-13页 |
| ·形式化分析的研究与进展 | 第13-18页 |
| ·形式化观点 | 第14-16页 |
| ·计算观点 | 第16-17页 |
| ·计算观点与形式化观点的关系 | 第17页 |
| ·形式化分析的现状与进一步发展 | 第17-18页 |
| ·主要内容与创新点 | 第18-21页 |
| ·论文结构及基本内容 | 第21-23页 |
| 第二章 密码协议的形式化模型 | 第23-44页 |
| ·概述 | 第23-25页 |
| ·进程演算的语法 | 第25-26页 |
| ·进程演算的语义 | 第26-31页 |
| ·攻击者 | 第26-28页 |
| ·转移系统 | 第28-31页 |
| ·保密性 | 第31-38页 |
| ·保密性的概率定义 | 第32-33页 |
| ·两种保密性概念的比较 | 第33-34页 |
| ·DY保密性和DY_P保密性的比较 | 第34-38页 |
| ·认证性 | 第38-40页 |
| ·认证性的概率定义 | 第39-40页 |
| ·认证性的比较 | 第40页 |
| ·非固定开销的操作 | 第40-42页 |
| ·模型的扩展 | 第42-43页 |
| ·秘密通道 | 第42页 |
| ·没有猜测的破坏 | 第42页 |
| ·盲猜测 | 第42-43页 |
| ·其他密码学概念 | 第43页 |
| ·小结 | 第43-44页 |
| 第三章 进程分析方法 | 第44-63页 |
| ·概述 | 第44-45页 |
| ·基本概念 | 第45-49页 |
| ·语义 | 第49-51页 |
| ·逼近的完成算法 | 第51-53页 |
| ·完成算法 | 第51-53页 |
| ·完成算法的合理性 | 第53页 |
| ·弱化左线性假设 | 第53-57页 |
| ·完成算法 | 第55-56页 |
| ·完成算法的合理性 | 第56-57页 |
| ·算法改进 | 第57-62页 |
| ·完成算法的精确性改进 | 第57-59页 |
| ·完成算法的合理性 | 第59-62页 |
| ·小结 | 第62-63页 |
| 第四章 密码协议的静态分析方法 | 第63-79页 |
| ·概述 | 第63-64页 |
| ·密码协议的形式化描述语言 | 第64-65页 |
| ·动态语义 | 第65-68页 |
| ·静态语义 | 第68-73页 |
| ·控制流分析 | 第68-72页 |
| ·CFA简化 | 第72-73页 |
| ·密码协议分析 | 第73-78页 |
| ·Wide-Mouthed Frog密钥交换协议 | 第73-74页 |
| ·Diffie-Helman密钥交换协议 | 第74-78页 |
| ·小结 | 第78-79页 |
| 第五章 基于Spi演算的密码协议自动化验证 | 第79-109页 |
| ·密码协议自动化验证概述 | 第79-80页 |
| ·密码协议自动化验证技术 | 第80-84页 |
| ·基于模型检测的密码协议自动化验证技术 | 第80-83页 |
| ·基于定理证明的密码协议自动化验证技术 | 第83-84页 |
| ·扩展Spi演算与安全特性的形式化描述 | 第84-95页 |
| ·密码协议的形式化描述语言 | 第84-85页 |
| ·扩展Spi演算 | 第85-88页 |
| ·密码协议的一阶逻辑描述 | 第88-91页 |
| ·转换规则 | 第91-95页 |
| ·密码协议安全特性的验证方法 | 第95-102页 |
| ·协议安全特性的形式化定义 | 第95-98页 |
| ·协议安全特性的验证 | 第98-102页 |
| ·EKE协议的安全性分析 | 第102-108页 |
| ·协议安全性的验证 | 第102-104页 |
| ·EKE协议概述 | 第104-105页 |
| ·EKE协议的形式化描述 | 第105-107页 |
| ·EKE协议分析 | 第107-108页 |
| ·小结 | 第108-109页 |
| 第六章 结束语与展望 | 第109-111页 |
| ·主要工作 | 第109-110页 |
| ·将来的工作 | 第110-111页 |
| 参考文献 | 第111-121页 |
| 作者简历 攻读博士学位期间完成的主要工作 | 第121-122页 |
| 致谢 | 第122页 |
