基于事件逻辑的无线Mesh网络客户端认证协议的形式化分析
| 摘要 | 第3-4页 |
| abstract | 第4页 |
| 符号说明 | 第7-8页 |
| 第一章 绪论 | 第8-12页 |
| 1.1 研究背景及意义 | 第8-9页 |
| 1.2 发展历史及研究现状 | 第9-10页 |
| 1.3 本文主要内容 | 第10-11页 |
| 1.4 论文结构安排 | 第11-12页 |
| 第二章 无线Mesh网络协议及形式化方法概述 | 第12-21页 |
| 2.1 无线Mesh网络 | 第12-14页 |
| 2.1.1 无线Mesh网络概述 | 第12-13页 |
| 2.1.2 无线Mesh网络的安全威胁 | 第13-14页 |
| 2.1.3 无线Mesh网络认证协议的安全需求 | 第14页 |
| 2.2 无线Mesh网络客户端协议分析 | 第14-18页 |
| 2.2.1 WMN客户端与LTCA间认证协议 | 第15-16页 |
| 2.2.2 WMN客户端间认证协议 | 第16-18页 |
| 2.3 形式化方法概述 | 第18-21页 |
| 2.3.1 模型检测 | 第18-19页 |
| 2.3.2 定理证明 | 第19-21页 |
| 第三章 事件逻辑理论 | 第21-35页 |
| 3.1 事件逻辑理论 | 第21-26页 |
| 3.1.1 基本定义 | 第21-24页 |
| 3.1.2 加密系统建模 | 第24-26页 |
| 3.2 事件逻辑理论公理、推论及性质 | 第26-30页 |
| 3.2.1 事件逻辑理论公理 | 第26-29页 |
| 3.2.2 事件逻辑理论推论及性质 | 第29-30页 |
| 3.3 形式化方法描述协议 | 第30-32页 |
| 3.3.1 线程和基本序列 | 第30-31页 |
| 3.3.2 匹配会话及协议动作 | 第31页 |
| 3.3.3 事件逻辑方法描述协议 | 第31-32页 |
| 3.4 安全协议证明过程 | 第32-34页 |
| 3.4.1 事件逻辑理论方法证明流程详述 | 第32-33页 |
| 3.4.2 事件逻辑理论方法证明流程 | 第33-34页 |
| 3.5 本章小结 | 第34-35页 |
| 第四章 无线Mesh网协议形式化分析 | 第35-48页 |
| 4.1 WMN客户端与LTCA间双向认证协议证明 | 第35-41页 |
| 4.1.1 协议的形式化分析 | 第35-36页 |
| 4.1.2 协议证明过程 | 第36-41页 |
| 4.2 WMN客户端间双向协议认证性证明 | 第41-46页 |
| 4.2.1 协议的形式化分析 | 第41-42页 |
| 4.2.2 协议证明过程 | 第42-46页 |
| 4.3 本章小结 | 第46-48页 |
| 第五章 形式化方法对比分析 | 第48-51页 |
| 5.1 事件逻辑理论与模态逻辑比较 | 第48-49页 |
| 5.2 事件逻辑理论与PCL比较 | 第49页 |
| 5.3 事件逻辑理论通用性 | 第49-51页 |
| 第六章 总结与展望 | 第51-53页 |
| 6.1 总结 | 第51页 |
| 6.2 展望 | 第51-53页 |
| 参考文献 | 第53-56页 |
| 个人简历在读期间发表的学术论文 | 第56-57页 |
| 致谢 | 第57页 |
