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

梅映天 吴尚青

(1池州职业技术学院 安徽池州 247100；2江西省机场集团公司九江机场分公司 江西九江 332000)

IEEE 802.11是自1997年以来，无线局域网络使用的通用标准，随着信息时代的不断发展，IEEE 802.11标准也在不断地修改和完善，从而增强数据安全和用户认证机制[1]。最初，管理框架不包含敏感信息，因此不太需要对其进行保护，但是随着新的无线网络管理方案的更新以及管理帧中敏感信息未加密问题的日益严重，IEEE工作组提出了一个新的IEEE 802.11w修正案，旨在保护无线连接和管理帧中交换的网络敏感信息[2]。IEEE 802.11w标准基于IEEE 802.11i无线网络管理框架[3]，是一种在原始框架下增加管理帧保护的标准，致力于改进IEEE 802.11通用标准中的MAC层从而增加管理帧的安全性[4-5]，可以对抗攻击者在无线局域网中基于管理帧的攻击[6]。

形式化方法被广泛应用于验证密码协议的不同安全属性，如协议交互过程中密文机密性的证明，不同主体之间认证性的证明，或是电子商务协议中不可否认性的证明，从而保证协议执行过程中的正确性[7]。事件逻辑[8]属于定理证明一类，是形式化方法的一种，不仅可以形容各类分布式系统中出现的状态迁移事件，同样也可以对密码协议的各种属性进行描述[9]。事件逻辑理论可以将安全协议表述为事件序和事件类的语言，并且使用原子Atom来表示nonce,key,signature,ciphertexts，给出简单的公理化理论[10]，通过这些定义，安全协议可以被正式定义，其强认证属性也可以通过定义进行进一步的证明。

文章组织结构如下：第2节介绍IEEE 802.11w无线网络认证协议；第3节介绍事件逻辑理论，并提出随机数引理；第4节使用事件逻辑理论对IEEE 802.11w无线网络认证协议认证性进行证明；第5节为文章的结论部分。

1 IEEE802.11w无线认证协议

在IEEE 802.11w无线网络认证协议正式通过确立之前，只有数据帧能够被加密保护[11]，而对管理帧和控制帧等所有其他帧都没有任何保护[12]。IEEE 802.11w在协议的交互过程中，有别于其他标准的一处就是允许使用一些具有保护的管理帧，通过四次握手完成秘钥协商从而保护管理帧。

IEEE 802.11w无线认证协议通过四次握手过程验证STA(Station，工作站)是否知道PMK(Pre-Shared Key，预共享密钥)[13]。其中AP(Acess point，接入点)可以理解为无线网络的创建方，提供无线网络接入的服务，STA是任何可以连接并且加入到当前无线局域网的终端。

根据完美密码假设，假定密码系统是完善的，从而对协议本身进行剖析，可得到主要认证交互信息如图1所示，首先AP发送包含NonceA的信息，然后STA发送给AP新生成的随机数NonceS和基于NonceA的消息完整性验证。在接收到第二条消息之后，AP能够导出PTK，通过发送经PTK加密的GTK，IGTK，NonceS的消息完整性验证来检查消息的正确性并继续认证，最后STA发送给AP一个只包含GTK，IGTK的完整性确认。

图1 IEEE 802.11w中主要交互信息描述

2事件逻辑理论

事件逻辑是定理证明方法中的一种，使用严格的数学规则和逻辑方法对密码协议的性质进行证明分析，是一种描述并发与分布式系统下协议和算法的逻辑。

2.1基本语义

该部分介绍事件逻辑基本语义[8，14-15]，用于刻画IEEE 802.11w无线网络认证协议交互过程中的不同安全属性，基本符号定义具体如表1所示。

表1 事件逻辑基本符号

在对IEEE 802.11w无线网络认证协议进行形式化证明之前，首先需要使用事件逻辑理论对IEEE 802.11w无线网络认证协议的交互过程进行建模，建立包含事件点的模型，主要通过三种类型布尔值、标识符、原子(Atom)，其中原子表示不可预测的数据值[6-7]，即任何无法猜测的内容，比如密文和挑战数。x:T||a表示类型T不包含原子a。当x属于类型T时，x和a相互独立。

事件类是事件逻辑中另一个基本概念，将密码协议中会发生的主要事件进行分类，包括信息的发送，信息的接受，不同主体随机数的生成，明文的加密，密文的解密，信息的签名以及签名的验证，其中不同事件的类型由此决定。事件类包含Atom，可以使用一个二叉树Data≡defTree(Id+Atom)来定义所有事件类，七个协议动作类型可定义如下：

2.2公理系统

2.2.1因果公理 因果公理包括AxiomR,AxiomV,AxiomD，将任何的接收，验证以及解密事件之间发生前后相互关联起来。

2.2.2不相交公理 不相交公理定义任何主体，其产生的随机数nonce与自身持有的私钥，签名以及密文是不相交的。

2.2.3诚实公理 诚实主体在任何情况下都不会释放自己的私钥，并且任何的签名事件、加密事件以及解密事件，如果需要使用到主体私钥，这些事件都必须发生在诚实主体上。

2.2.4秘钥公理 对称密钥只能匹配自身，而分配给主体的私有秘钥只匹配相对的公钥，协议交互过程中没有任何两个主体会拥有相同的私钥。

2.2.5随机数公理 随机数公理主要包含三部分，主要定义签名、密文以及包含事件之间的相似关系。如果存在没有经过假设的签名消息或者加密信息，那么一定与独立事件有关，所以如果存在一个事件包含签名消息或者加密过的信息，只能推断出部分的消息签名或加密事件。

2.2.6流关系 流关系公理定义事件与事件之间的因果顺序，假设Atom类型的a从e1流入到e2，只能以有限的方式发生。第一种方式是e1和e2位于同一主体；第二种是存在发送和接收事件，将a通过明文发送；第三种情况为a位于加密事件，并流入匹配的解密事件。

2.3推理规则

线程thr是主体A中已知bss基本序列的其中之一，记作thr=oneof(bss,A)。关系inoneof(e,thr,bss,A)用协议的形式化定义为：e∈thr∧thr=oneof(bass,A)[14-15]。

线程thr1和thr2构成一个长度为n的匹配会话，如果它们包含至少n个消息，且当线程中前n个消息成对存在，每对满足m1|m2∨m2|m1。此时强匹配会话定义为如果每对只满足m1～m2∨m2～m1，得到一个弱匹配会话，记作

2.4随机数引理

如果协议Protocol(bss)是合法的。A是诚实主体并且属于协议Protocol(bss)，且thr属于基本序列bssthr[j]、n∈E(New)、e=thr[j]，和j

3 IEEE802.11w无线认证协议分析

使用事件逻辑理论对IEEE802.11w无线认证协议的认证性进行分析，首先需要对该协议的基本序列进行描述，定义I1,I2,I3,I4,I5为协议认证方产生的基本序列，R1,R2,R3,R4为协议被认证方产生的基本序列，图2所示为IEEE 802.11w无线网络认证协议的交互过程描述。

图2 IEEE802.11w无线认证协议序列描述

通过事件逻辑理论形式化分析在协议交互过程中需要满足的安全属性，来验证IEEE802.11w无线网络认证协议是否存在未知风险，还需要对协议交互中的基本序列进行排序。图3所示为IEEE802.11w无线网络认证协议交互过程中每个主体间基本序列的排序。

图3 IEEE802.11w无线认证协议基本序列

如果IEEE802.11w无线认证协议可以保证不同时间的两个线程间具有强匹配会话，则IEEE802.11w无线网络认证协议满足协议交互过程中的强认证属性。所以分析基本序列，使用事件逻辑理论将IEEE802.11w无线网络认证协议定义为Protocol([I1，I2，I3，I4，I5，R1，R2，R3，R4])，需要验证的强身份认证性质为：

Nse╞auth(I5，4)∧Nse╞auth(R4，3)

首先对Nse╞auth(I5，4)进行证明，假设诚实主体AP≠STA，且双方都遵循IEEE802.11w无线认证协议，根据事件逻辑理论中对于协议中基本序列的定义，线程作为基本序列的实例存在，则令thr1是基本序列I5的一个实例，定义 e0

由验证公理AxiomV和诚实公理AxiomS可知，存在某个事件e′并且e′能够使得式子e′

故而可以排除I2,I3,I4,I5，即意味着R2,R3,R4中存在一个基本序列可能与I5构成匹配会话.

假设e′为R2中的一个实例，那么对于Atom类型的NonceS′,NonceA′,s1′以及主体A，在主体STA上存在事件e0′,e1′,e2′,e3′有：

通过上式发现，R2中签名事件e2′与验证事件e8不匹配，所以排除e′是R2中一个实例的可能性，同理排除R3。

可发现满足：

则可知有e7′=e′,B=AP,GTK′=GTK,IGTK′=IGTK,s4′=s4，可得出：

在已知e7′=e′，e′一定为R4中的某个实例后，必须存在某个事件e″，并且这个事件能够令e″,AP,s3>。

因此，事件e″必然为协议基本序列中的实例成员，在基本序列中，包含Sign( )动作的有I2,I3,I4,I5,R2,R3,R4。可以排除I4,I5，同样为了保证事件发生的有效性，所以AP和STA参与的事件类不能是单方的，可以排除R2,R3,R4，也就得出I2,I3中存在一个基本序列包含序列e″。

假设e″是I2上的实例，对于Atom类型的NonceS″,NonceA″,s1″和主体C，在主体AP存在事件e0″,e1″,e2″,e3″有：

从上式可得出I2中的签名事件e1″与解密事件e5′不匹配，所以排除e″是I2中的一个实例的可能性.

由上式可以发现，满足：

则可知有e6″=e″,NonceS″=NonceS,D=STA,s3″=s3，可以得到：

当e″为I3中的实例后，则必须再存在某个事件e‴并且这个事件可以使得如下表达式e‴,STA,s1>。

如果e‴存在，那么事件e‴必然为IEEE802.11w无线认证协议基本序列中的某一个实例成员，其中包含Sign( )动作的有I2,I3,I4,I5,R2,R3,R4。对于未发生的事件将不纳入考虑范围，则可以排除R3,R4,I4,I5，即R2中可能存在一个基本序列包含序列e‴。

假设e‴是R2上的一个实例，那么对于Atom类型的NonceS‴,NonceA‴,s1‴和主体E，在主体STA上存在事件e0‴,e1‴,e2‴,e3‴,e4‴,e5‴有：

可以发现满足：

则由上式可知存在e‴，故有e4‴=e‴,E=AP,NonceA‴=NonceA,s1‴=s1，由此可以得到：

根据以上证明结果，可以得到：

所以在协议的交互过程中，存在一个弱匹配会话，并且其长度为3。

下一步对协议交互过程中的强匹配会话进行证明，根据事件逻辑理论定义，首先需要证明e3′进行签名，而不包括STA的名称，若攻击者拥有足够的能力[16]，则在证明步骤中无法得出D=STA的结论，并且证明失败，即存在中间人的攻击。

类似的，可证明Nse╞auth(R4，3)。

通过证明，可知IEEE802.11w无线网络认证协议的交互主体同时满足需要证明的两个强认证性质，所以在协议交互过程中不存在消息重放的可能性，但是在攻击者拥有足够能力的情况下，存在中间人攻击，IEEE802.11w无线网络认证协议交互过程中的认证性无法得证。

4结语

文章基于事件逻辑理论对IEEE802.11w无线网络认证协议交互过程中的认证性进行验证，结合事件逻辑基本公理以及推理规则并提出随机数引理对IEEE 802.11w标准交互过程中认证性进行验证，证明得出IEEE 802.11w无线认证协议能够抵抗重放攻击但是存在中间人攻击。研究表明，事件逻辑理论适用于类似无线认证协议的证明。