基于Maude的PKMv3协议形式化建模与验证
| 摘要 | 第6-8页 |
| abstract | 第8-9页 |
| 第一章 绪论 | 第13-21页 |
| 1.1 研究背景与意义 | 第13-15页 |
| 1.2 国内外研究现状 | 第15-18页 |
| 1.3 研究内容和方法 | 第18-19页 |
| 1.4 论文结构 | 第19-21页 |
| 第二章 Maude介绍 | 第21-33页 |
| 2.1 重写逻辑 | 第22-23页 |
| 2.2 Maude形式化建模规范 | 第23-28页 |
| 2.2.1 函数模块 | 第23-25页 |
| 2.2.2 系统模块 | 第25-28页 |
| 2.3 Maude形式化分析方法 | 第28-31页 |
| 2.4 本章小结 | 第31-33页 |
| 第三章 PKMv3密钥管理协议 | 第33-51页 |
| 3.1 IEEE802.16m标准 | 第33-35页 |
| 3.1.1 IEEE802.16m标准的特点 | 第33-34页 |
| 3.1.2 IEEE802.16m网络拓扑结构 | 第34-35页 |
| 3.2 IEEE802.16参考模型层次结构 | 第35-38页 |
| 3.2.1 物理层 | 第36-37页 |
| 3.2.2 介质访问控制层 | 第37-38页 |
| 3.3 PKMv3协议密钥协商流程 | 第38-46页 |
| 3.3.1 双向认证过程 | 第40-42页 |
| 3.3.2 安全组件交换 | 第42-44页 |
| 3.3.3 传输密钥的生成 | 第44-45页 |
| 3.3.4 加密消息传输 | 第45-46页 |
| 3.4 PKMv3密钥重认证 | 第46-49页 |
| 3.4.1 AK重认证 | 第47-48页 |
| 3.4.2 TEK重认证 | 第48-49页 |
| 3.5 本章小结 | 第49-51页 |
| 第四章 PKMv3协议的形式化建模 | 第51-73页 |
| 4.1 基本数据类型的定义 | 第51-58页 |
| 4.1.1 通信主体建模 | 第51-53页 |
| 4.1.2 消息内容建模 | 第53-54页 |
| 4.1.3 密钥信息建模 | 第54-57页 |
| 4.1.4 传输消息建模 | 第57-58页 |
| 4.2 网络环境的建模 | 第58-68页 |
| 4.2.1 系统状态的形式化定义 | 第58-60页 |
| 4.2.2 消息传输形式化建模 | 第60-68页 |
| 4.3 入侵者模型 | 第68-71页 |
| 4.3.1 攻击者类型定义 | 第68页 |
| 4.3.2 攻击者行为建模 | 第68-71页 |
| 4.4 本章小结 | 第71-73页 |
| 第五章 PKMv3协议的形式化验证 | 第73-85页 |
| 5.1 协议初始状态的定义 | 第74页 |
| 5.2 PKMv3协议验证过程 | 第74-83页 |
| 5.2.1 时间特性的验证 | 第74-77页 |
| 5.2.2 安全特性的验证 | 第77-82页 |
| 5.2.3 验证结果分析 | 第82-83页 |
| 5.3 本章小结 | 第83-85页 |
| 第六章 PKMv3协议的改进 | 第85-95页 |
| 6.1 安全密钥管理协议 | 第85-88页 |
| 6.1.1 认证阶段消息传输 | 第86-87页 |
| 6.1.2 共享认证消息传输 | 第87-88页 |
| 6.2 密钥管理协议的建模和验证 | 第88-93页 |
| 6.2.1 安全协议建模过程 | 第89-91页 |
| 6.2.2 安全协议验证过程 | 第91-93页 |
| 6.3 现有改进方案对比与分析 | 第93-94页 |
| 6.4 本章小结 | 第94-95页 |
| 第七章 总结和展望 | 第95-97页 |
| 7.1 论文总结 | 第95-96页 |
| 7.2 工作展望 | 第96-97页 |
| 附录A 重写规则与变量表 | 第97-103页 |
| 参考文献 | 第103-111页 |
| 致谢 | 第111-113页 |
| 攻读硕士学位期间发表论文和科研情况 | 第113页 |
