基于CSP模型检测的无线传感网安全协议形式化验证

摘要

由于协议开发过程中，复杂的协议流程和协议应用场景可能会导致协议描述出现逻辑漏洞，致使整个系统产生逻辑冲突。协议的安全性和可靠性对协议是否能够安全有效的运行有很大影响，因此安全性分析和验证一直是协议设计的重点和难点。
　　基于通信顺序进程（CSP）的安全协议形式化分析验证已成为当前一个研究热点，基于CSP的安全协议模型可有效提高形式化分析和验证的效率。另一方面，随着无线传感网络（WSN）应用的日益广泛，其安全问题也逐渐突出。因此，将CSP方法应用到WSN安全协议的形式化分析和验证，在协议设计阶段及时发现协议存在的漏洞，可有效保证安全需求逻辑的正确性。
　　本文在研究WSN安全协议安全问题的基础上，采用当前比较公认的CSP形式化分析方法，对WSN安全协议的形式化分析和验证进行研究。首先，给出了一种基于CSP建模层的PAT工具扩展方法，扩展CSP建模模块，使其适用于WSN安全协议的建模和分析，实现对 WSN安全协议的快速形式化描述；其次，根据传感器节点的可移动性，扩展Dolev-Yao模型，使其适用于节点可移动的攻击者建模；然后，分析WSN安全协议的安全需求，提出一种线性时序逻辑（LTL）刻画性质的方法；最后，通过两个案例分析说明CSP方法在WSN安全协议和WBAN安全认证协议分析过程中的可行性和正确性。

目录

封面

声明

中文摘要

英文摘要

目录

第1章 绪论

1.1 课题背景

1.2 形式化分析的研究进展

1.3 研究内容及意义

1.4 论文组织结构

第2章 无线传感器网络及WSN安全协议

2.1 无线传感器网络体系结构

2.2 无线传感网络安全

2.3 安全协议形式化研究现状

2.4 本章小结

第3章 基于CSP的安全协议形式化分析方法

3.1 通信顺序进程CSP

3.2 安全协议形式化分析工具

3.3 线性时序逻辑公式

3.4 Dolev-Yao攻击者模型

3.5 CSP安全协议模型

3.6 本章小结

第4章 基于CSP的WSN安全协议建模与验证

4.1 无线传感网形式化建模架构

4.2 无线传感网节点位置建模

4.3 WSN安全协议形式化建模与验证

4.4 实验结果与分析

4.5 本章小结

第5章 基于CSP的WBAN安全协议建模与验证

5.1 无线体域网概述

5.2 WBAN安全协议研究现状

5.3 WBAN安全认证协议的建模框架

5.4 WBAN安全认证协议分析案例解析

5.5 本章小结

第6章 总结与展望

6.1 总结

6.2 下一步工作展望

参考文献

致谢

攻读学位期间参加的科研项目和成果