基于Maude的安全协议的形式化分析
| 摘要 | 第1-4页 |
| Abstract | 第4-7页 |
| 第一章 绪论 | 第7-17页 |
| ·形式化方法概述 | 第7-9页 |
| ·分布式系统 | 第7-8页 |
| ·形式化方法 | 第8-9页 |
| ·安全协议简介 | 第9-13页 |
| ·安全协议的分类 | 第10-11页 |
| ·安全协议的性质 | 第11-12页 |
| ·安全协议的缺陷 | 第12-13页 |
| ·攻击者理论 | 第13-16页 |
| ·Dolev-Yao 模型 | 第13页 |
| ·攻击者的能力和知识 | 第13-14页 |
| ·消息以及环境推测系统 | 第14-15页 |
| ·通信网络模型 | 第15-16页 |
| ·本文的主要内容及组织 | 第16-17页 |
| 第二章 重写逻辑 | 第17-25页 |
| ·重写技术 | 第17-19页 |
| ·重写逻辑 | 第19-24页 |
| ·推理规则 | 第19-20页 |
| ·初始化和自由模型 | 第20-22页 |
| ·反射性 | 第22-23页 |
| ·可执行能力 | 第23-24页 |
| ·本章小结 | 第24-25页 |
| 第三章 协议检测软件 Maude | 第25-35页 |
| ·Maude 系统 | 第25-27页 |
| ·Maude 语言 | 第25-26页 |
| ·Maude 主要特征及应用 | 第26-27页 |
| ·Core Maude | 第27-33页 |
| ·Core Maude 基本语法 | 第27-29页 |
| ·Core Maude 函数模块 | 第29-31页 |
| ·Core Maude 系统模块 | 第31-33页 |
| ·Full Maude | 第33页 |
| ·本章小结 | 第33-35页 |
| 第四章 IKEv2 协议保密性和认证性测试 | 第35-57页 |
| ·IKEv2 协议 | 第35-36页 |
| ·IKEv2 协议形式化建模 | 第36-50页 |
| ·主体和临时值建模 | 第37-39页 |
| ·加密算法建模 | 第39-40页 |
| ·密钥建模 | 第40-41页 |
| ·消息内容建模 | 第41-44页 |
| ·网络环境建模 | 第44页 |
| ·入侵者知识建模 | 第44-47页 |
| ·IKEv2 协议重写 | 第47-50页 |
| ·IKEv2 协议保密性和认证性检测 | 第50-56页 |
| ·IKEv2 测试原理 | 第52页 |
| ·IKEv2 协议保密性测试 | 第52-53页 |
| ·IKEv2 协议认证性测试 | 第53-56页 |
| ·IKEv2 协议改进 | 第56页 |
| ·本章小结 | 第56-57页 |
| 第五章 SHARE 协议检测 | 第57-69页 |
| ·SHARE 协议测试原理 | 第57-59页 |
| ·SHARE 协议 | 第57页 |
| ·SHARE 协议测试 | 第57-59页 |
| ·SHARE 协议形式化建模分析 | 第59-65页 |
| ·临时值建模 | 第59-61页 |
| ·消息建模 | 第61-62页 |
| ·SHARE 协议重写 | 第62-65页 |
| ·协议认证性检测 | 第65-67页 |
| ·本章小结 | 第67-69页 |
| 第六章 总结与展望 | 第69-71页 |
| 致谢 | 第71-73页 |
| 参考文献 | 第73-76页 |
| 作者读研期间参加的科研项目 | 第76-77页 |
