浙江工业大学学报
浙江工業大學學報
절강공업대학학보
Journal of Zhejiang University of Technology
2015年
5期
497-502
,共6页
陈铁明%虞震波%王婷%方赵林
陳鐵明%虞震波%王婷%方趙林
진철명%우진파%왕정%방조림
无线体域网%模型检测%安全协议%PAT%CSP#%线性时序逻辑
無線體域網%模型檢測%安全協議%PAT%CSP#%線性時序邏輯
무선체역망%모형검측%안전협의%PAT%CSP#%선성시서라집
wireless body area networks%model checking%security protocols%PAT%CSP#%linear temporal logic
在研究无线体域网(WBAN)安全属性的基础上,为了对无线体域网安全协议进行安全分析,保证协议设计之初的安全性,提出并实现了一种基于模型检测的无线体域网安全协议形式化分析和验证方法.基于模型检测工具PAT研究建模语言CSP#及其扩展方法,提出一种支持网络节点可移动的抽象建模数据结构,便于对WBAN协议的形式化建模;根据Dolev-Yao模型,结合WBAN节点位置的可移动性,建立攻击者抽象模型.以Chitra等提出的基于双天线的WBAN安全协议为例,在PAT工具中应用笔者提出的方法对其进行建模并加以分析验证,体现了方法的实用性.
在研究無線體域網(WBAN)安全屬性的基礎上,為瞭對無線體域網安全協議進行安全分析,保證協議設計之初的安全性,提齣併實現瞭一種基于模型檢測的無線體域網安全協議形式化分析和驗證方法.基于模型檢測工具PAT研究建模語言CSP#及其擴展方法,提齣一種支持網絡節點可移動的抽象建模數據結構,便于對WBAN協議的形式化建模;根據Dolev-Yao模型,結閤WBAN節點位置的可移動性,建立攻擊者抽象模型.以Chitra等提齣的基于雙天線的WBAN安全協議為例,在PAT工具中應用筆者提齣的方法對其進行建模併加以分析驗證,體現瞭方法的實用性.
재연구무선체역망(WBAN)안전속성적기출상,위료대무선체역망안전협의진행안전분석,보증협의설계지초적안전성,제출병실현료일충기우모형검측적무선체역망안전협의형식화분석화험증방법.기우모형검측공구PAT연구건모어언CSP#급기확전방법,제출일충지지망락절점가이동적추상건모수거결구,편우대WBAN협의적형식화건모;근거Dolev-Yao모형,결합WBAN절점위치적가이동성,건립공격자추상모형.이Chitra등제출적기우쌍천선적WBAN안전협의위례,재PAT공구중응용필자제출적방법대기진행건모병가이분석험증,체현료방법적실용성.
