传感技术学报
傳感技術學報
전감기술학보
Journal of Transduction Technology
2013年
2期
234-240
,共7页
无线传感器网络%安全协议%模型检测%线性时序逻辑
無線傳感器網絡%安全協議%模型檢測%線性時序邏輯
무선전감기망락%안전협의%모형검측%선성시서라집
针对Zhang等人提出的一种基于位置的无线传感网络安全方案,开展基于模型检测的形式化分析与改进研究.首先采用模型检测工具SPIN分析和验证邻居节点认证协议,发现节点移动后将导致邻居节点无法认证的问题；为支持节点可移动,直接对协议给出一种改进方案,并采用模型检测对改进后的协议重新建模分析,发现存在中间人攻击威胁；最后根据模型检测结果,进一步提出用时间戳替换随机数的改进方案,可有效抵御中间人攻击.本文工作表明,模型检测不仅能实现对无线传感网络安全协议的形式化分析与验证,还可有效协助实现安全协议的设计与改进.
針對Zhang等人提齣的一種基于位置的無線傳感網絡安全方案,開展基于模型檢測的形式化分析與改進研究.首先採用模型檢測工具SPIN分析和驗證鄰居節點認證協議,髮現節點移動後將導緻鄰居節點無法認證的問題；為支持節點可移動,直接對協議給齣一種改進方案,併採用模型檢測對改進後的協議重新建模分析,髮現存在中間人攻擊威脅；最後根據模型檢測結果,進一步提齣用時間戳替換隨機數的改進方案,可有效牴禦中間人攻擊.本文工作錶明,模型檢測不僅能實現對無線傳感網絡安全協議的形式化分析與驗證,還可有效協助實現安全協議的設計與改進.
침대Zhang등인제출적일충기우위치적무선전감망락안전방안,개전기우모형검측적형식화분석여개진연구.수선채용모형검측공구SPIN분석화험증린거절점인증협의,발현절점이동후장도치린거절점무법인증적문제；위지지절점가이동,직접대협의급출일충개진방안,병채용모형검측대개진후적협의중신건모분석,발현존재중간인공격위협；최후근거모형검측결과,진일보제출용시간착체환수궤수적개진방안,가유효저어중간인공격.본문공작표명,모형검측불부능실현대무선전감망락안전협의적형식화분석여험증,환가유효협조실현안전협의적설계여개진.
