SPIN在无线网络安全认证协议建模中的应用  

Application of SPIN in Wireless Network Security Authentication Protocol Modeling

作　　者：周莉[1] 陆萍[2] 董虎胜[2] 谭方勇[1] 

机构地区：[1]江苏省现代企业信息化应用支撑软件工程技术研发中心,江苏苏州215104 [2]苏州经贸职业技术学院信息系,江苏苏州215009

出　　处：《煤炭技术》2013年第1期169-170,共2页Coal Technology

基　　金：江苏省自然科学基金(BK2007050);江苏省现代企业信息化应用支撑软件工程技术研发中心开放基金项目(SX201001)

摘　　要：为确保无线网络安全认证,应用模型检查工具SPIN对EAP-TLS认证协议进行建模,根据SPIN给出攻击轨迹,指出EAP-TLS可能存在双向认证失败的安全隐患,从抵抗攻击和协议改进提出了基于隧道的认证方法。使用SPIN PROMELA语言对通信各方建模,用线性时态逻辑LTL表示安全属性,提出了将SPIN应用于认证协议的验证方法。To insure wireless network authentication security, applying SPIN models 802.1 x EAP -TLS authentication protocol. With the attack track given by SPIN, the security vulnerabilities caused by the improper configuration are pointed out, meanwhile the new tunnel authentication protocol is proposed to reduce the occurrence of attack and to improve the agreement. With communication parts defined by mod- el checking language PROMELA, security properties expressed by LTL formula, a method of verifying authentication protocol is pronosed based on SPIN.

关 键 词：模型检测 认证协议 协议验证 可扩展认证协议 传输层安全 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]