| SPIN在无线网络安全认证协议建模中的应用 |
| |
| 引用本文： | 周莉,陆萍,董虎胜,谭方勇. SPIN在无线网络安全认证协议建模中的应用[J]. 煤炭技术, 2013, 32(1): 169-170 |
| |
| 作者姓名： | 周莉 陆萍 董虎胜 谭方勇 |
| |
| 作者单位： | 1. 江苏省现代企业信息化应用支撑软件工程技术研发中心,江苏苏州,215104
2. 苏州经贸职业技术学院信息系,江苏苏州,215009 |
| |
| 基金项目： | 江苏省自然科学基金，江苏省现代企业信息化应用支撑软件工程技术研发中心开放基金项目 |
| |
| 摘 要： | 为确保无线网络安全认证,应用模型检查工具SPIN对EAP-TLS认证协议进行建模,根据SPIN给出攻击轨迹,指出EAP-TLS可能存在双向认证失败的安全隐患,从抵抗攻击和协议改进提出了基于隧道的认证方法。使用SPIN PROMELA语言对通信各方建模,用线性时态逻辑LTL表示安全属性,提出了将SPIN应用于认证协议的验证方法。
|
| 关 键 词： | 模型检测 认证协议 协议验证 可扩展认证协议 传输层安全 |
Application of SPIN in Wireless Network Security Authentication Protocol Modeling |
| |
| ZHOU Li , LU Ping , DONG Hu-sheng , TAN Fang-yong. Application of SPIN in Wireless Network Security Authentication Protocol Modeling[J]. Coal Technology, 2013, 32(1): 169-170 |
| |
| Authors: | ZHOU Li LU Ping DONG Hu-sheng TAN Fang-yong |
| |
| Affiliation: | 1(1.Jiangsu Province Support Software Engineering R&D Center for Modern Information Technology Application in Enterprise,Suzhou 210104,China;2.Department of Information,Suzhou Institute of Trade & Commerce,Suzhou 215009,China) |
| |
| Abstract: | To insure wireless network authentication security,applying SPIN models 802.1x 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 model checking language PROMELA,security properties expressed by LTL formula,a method of verifying authentication protocol is proposed based on SPIN. |
| |
| Keywords: | model checking authentication protocol protocol verifying EAP TLS |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
