基于模型检测的无线传感网安全协议形式化分析与改进

针对Zhang等人提出的一种基于位置的无线传感网络安全方案，开展基于模型检测的形式化分析与改进研究。首先采用模型检测工具SPIN对邻居节点认证协议进行分析和验证，发现节点移动后将导致邻居节点无法认证的问题；为了支持节点可移动，直接对协议给出一种改进方案，采用模型检测对改进后的协议重新建模分析，又发现存在中间人攻击的威胁；最后根据模型检测结果，进一步提出用时间戳替换随机数的改进方案，有效抵御了中间人攻击。本文的工作表明，模型检测不仅能实现对无线传感器网络安全协议的形式化分析与验证，还可有效协助完成安全协议的设计与改进。

Model Checking-based Formal Analysis and Improvement on Wireless Sensor Network Security Protocols

Formal analysis and improvement for a novel location-based security mechanism on wireless sensor networks are conducted in this paper. At first, the neighbor node authentication protocol is formally verified using the model check tool SPIN, and it is found that the authentication will fail if the node moves its location. Due to obtain a node move-free scheme, an improved location-based authentication security protocol is proposed. However, by model checking the proposed scheme under the modified specification, a man-in-the-middle attack is eventually detected. Finally, the timestamp is employed to substitute the original used nonce to resist the MITM attack. Our works show that model check, as an efficient formal method, can not only analyze and verify the specialized security protocols on wireless sensor networks, but also facilitate the security scheme design and improvement.