基于CSP模型检测的无线传感网安全协议形式化验证
| 摘要 | 第1-6页 |
| ABSTRACT | 第6-9页 |
| 第1章 绪论 | 第9-13页 |
| ·课题背景 | 第9-10页 |
| ·形式化分析的研究进展 | 第10页 |
| ·研究内容及意义 | 第10-11页 |
| ·论文组织结构 | 第11-13页 |
| 第2章 无线传感器网络及WSN安全协议 | 第13-21页 |
| ·无线传感器网络体系结构 | 第13-14页 |
| ·无线传感器节点体系结构 | 第13-14页 |
| ·无线传感网络体系结构 | 第14页 |
| ·无线传感网络安全 | 第14-18页 |
| ·无线传感器网络的安全特点 | 第14-15页 |
| ·无线传感器网络安全问题 | 第15页 |
| ·无线传感器网络攻击类型 | 第15-17页 |
| ·无线传感器网络安全目标 | 第17-18页 |
| ·安全协议形式化研究现状 | 第18-20页 |
| ·形式化方法的概念 | 第18-19页 |
| ·安全协议形式化描述 | 第19页 |
| ·安全协议形式化分析 | 第19页 |
| ·安全协议形式化验证 | 第19-20页 |
| ·本章小结 | 第20-21页 |
| 第3章 基于CSP的安全协议形式化分析方法 | 第21-32页 |
| ·通信顺序进程CSP | 第21-23页 |
| ·CSP语法和语义 | 第21-22页 |
| ·CSP运算符 | 第22-23页 |
| ·安全协议形式化分析工具 | 第23-25页 |
| ·PAT模型检测工具 | 第23-24页 |
| ·其他模型检测工具 | 第24-25页 |
| ·线性时序逻辑公式 | 第25-27页 |
| ·命题逻辑 | 第25页 |
| ·LTL公式 | 第25-27页 |
| ·Dolev-Yao攻击者模型 | 第27-28页 |
| ·攻击者的知识和能力 | 第27-28页 |
| ·攻击者的行为 | 第28页 |
| ·CSP安全协议模型 | 第28-30页 |
| ·CSP安全协议模型中的数据类型 | 第29页 |
| ·CSP安全协议模型中的事件和结构 | 第29-30页 |
| ·安全协议的属性描述 | 第30页 |
| ·本章小结 | 第30-32页 |
| 第4章 基于CSP的WSN安全协议建模与验证 | 第32-42页 |
| ·无线传感网形式化建模架构 | 第32-33页 |
| ·无线传感网节点位置建模 | 第33-36页 |
| ·基于位置的无线传感网协议 | 第33-34页 |
| ·支持节点可移动的抽象方法 | 第34-35页 |
| ·基于数据结构扩展的CSP语言和结构 | 第35-36页 |
| ·WSN安全协议形式化建模与验证 | 第36-40页 |
| ·协议诚实实体建模 | 第36-38页 |
| ·节点可移动的攻击者建模 | 第38-39页 |
| ·协议性质描述 | 第39-40页 |
| ·实验结果与分析 | 第40-41页 |
| ·本章小结 | 第41-42页 |
| 第5章 基于CSP的WBAN安全协议建模与验证 | 第42-55页 |
| ·无线体域网概述 | 第42-44页 |
| ·无线体域网标准 | 第42-43页 |
| ·无线体域网与无线传感网的区别 | 第43-44页 |
| ·WBAN安全协议研究现状 | 第44-46页 |
| ·WBAN安全协议隐私保护研究现状 | 第44-45页 |
| ·WBAN安全协议安全认证研究现状 | 第45页 |
| ·WBAN安全协议的形式化方法应用研究现状 | 第45-46页 |
| ·WBAN安全认证协议的建模框架 | 第46-47页 |
| ·WBAN安全认证协议分析案例解析 | 第47-53页 |
| ·基于双天线的WBAN安全认证协议 | 第47-48页 |
| ·协议信任实体建模 | 第48-50页 |
| ·攻击者节点建模 | 第50-52页 |
| ·协议安全属性描述 | 第52页 |
| ·验证结果 | 第52-53页 |
| ·本章小结 | 第53-55页 |
| 第6章 总结与展望 | 第55-57页 |
| ·总结 | 第55页 |
| ·下一步工作展望 | 第55-57页 |
| 参考文献 | 第57-61页 |
| 致谢 | 第61-62页 |
| 攻读学位期间参加的科研项目和成果 | 第62页 |
