IEEE 802.11w无线网络协议的形式化分析与验证  

Formal Analysis and Verification of IEEE 802.11w Wireless Network Protocol

作　　者：梅映天 吴尚青 MEI Yingtian;WU Shangqing(Chizhou Vocational and Technical College,Chizhou,Anhui 247100;Jiangxi Airport Group Company,Jiujiang Airport Branch,Jiujiang,Jiangxi 332000,China)

机构地区：[1]池州职业技术学院,安徽池州247100 [2]江西省机场集团公司九江机场分公司,江西九江332000

出　　处：《九江学院学报（自然科学版）》2021年第2期57-64,共8页Journal of Jiujiang University：Natural Science Edition

基　　金：安徽省级质量工程项目(2019jyxm0648);江西省教育厅科学技术研究项目(编号GJJ190326);池州职业技术学院院级科研项目(编号ZR2018Z02)的成果之一。

摘　　要：IEEE802.11是在无线局域网中提供安全通信的标准,主要用于无线工作站访问由访问点管理的受保护无线网络,IEEE802.11w无线认证协议增强了原先基础上所选管理帧的安全性。事件逻辑理论是一种描述并发与分布式系统下协议和算法的逻辑,使用严格的数学规则和逻辑方法对协议的性质进行证明分析。协议认证性的证明是一个安全协议设计中必不可少的一部分,文章基于事件逻辑理论,定义协议运行过程中的基本序列和匹配会话,结合事件逻辑基本公理和推理规则并提出随机数引理对IEEE 802.11w标准交互过程中认证性进行验证,证明得出IEEE 802.11w无线认证协议能够抵抗重放攻击但存在中间人攻击。研究表明,事件逻辑适用于无线认证协议的分析。IEEE 802.11 was the standard designed to provide secured communication in WLAN and it mainly provided wireless station to access a protected wireless networkmanaged by an access point.IEEE 802.11w authentication protocol enhanced the security to selectedmanagement frames.Logic of events was a kind of logic to describe protocols and algorithms in concurrent and distributed systems,it used strict mathematical rules and logic to analyze the security properties of cryptographic protocols.The certification of authentication property was an essential part in the design of a secure protocol.Based on the logic of events,this paper defined the basic sequence andmatching session,combined the basic axioms and reasoning rules of logic of events,and proposed nonce lemma to verify the authentication property in the interaction process of IEEE 802.11w standard.It was proved that IEEE 802.11w wireless authentication protocol could resist replay attack but hasman-in-the-middle attack.Research showed that logic of events was suitable for wireless network protocols.

关 键 词：形式化方法 事件逻辑 无线网络认证协议 IEEE 802.11w 

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