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

• 作者: 何卡特 江颉 陈铁明
• 来源期刊: 传感技术学报
• 学科: 工学
• 关键词: 无线传感器网络 安全协议 模型检测 线性时序逻辑
• 年，卷（期）: 2013,（2）
• 所属期刊栏目: 无线传感器网络
• 页码范围: 234-240
• 页数: 7页
• 分类号: TP309.7
• 字数: 6015字
• 语种: 中文
• DOI: 10.3969/j.issn.1004-1699.2013.02.018

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	江颉	浙江工业大学计算机科学与技术学院	38	249	10.0	13.0
2	陈铁明	浙江工业大学计算机科学与技术学院	60	357	11.0	15.0
3	何卡特	浙江工业大学计算机科学与技术学院	1	4	1.0	1.0