孟博，黄伟，王德军，邵飞

（中南民族大学 计算机科学学院，湖北 武汉 430074）

1 引言

拒绝服务攻击具有威害巨大及难以有效防御的特点，越来越受到网络安全专家与用户的关注。拒绝服务攻击是通过各种手段使提供服务的主机无法提供服务的一种攻击，本质是对分布式系统的可用性进行攻击。按照攻击方式可以分为：资源消耗型、服务中止型和物理破坏型。这种攻击简单有效，如攻击者可以发送大量垃圾信息给服务器，造成服务器处理大量无效的数据，从而无法向合法用户提供正常的服务，而产生拒绝服务攻击；此外拒绝服务攻击很难甚至无法确定攻击者，并且能够通过这种攻击产生其他攻击，例如，中间人攻击，会话拦截攻击等。目前的 TCP/IP协议架构从链路层到应用层都存在拒绝服务攻击，例如，链路层的ARP Flooding攻击、ARP poisoning攻击，网络层的ICMP攻击，传输层的SYN Floods攻击，应用层的session flooding攻击、buffer overflow攻击等。

对拒绝服务攻击的形式化建模，目前有2类主要方法，一类是以用户合约为基础的 Yu-Gligor形式化建模方法[1]，另一类是以代价为基础的Meadows形式化建模方法[2]，后者受到了人们的重点关注。

安全协议的形式化分析与验证方法主要有定理证明、模型检测、逻辑推理、类型检测等。代表性的定理证明方法有 Paulson的归纳证明法和Thayer等学者提出的串空间模型。基于定理证明的方法在自动化工具支持方面虽然无法与模型检测方法比拟，但是它克服了模型检测固有的缺陷——状态空间爆炸的问题，能够处理无穷状态系统。定理证明可以通过自动化的定理证明器协助完成证明过程。主要的定理证明器有 ProVerif、Isabelle、HOL、ACL2、PVS等，其中ProVerif是Blanchet[3]开发的基于Dolev-Yao模型的一阶定理证明器，它可以分析和验证使用Horn子句或应用PI演算描述的安全协议的秘密性、强秘密性、认证性等。ProVerif已经成功分析了很多复杂的协议，如电子商务协议[4]、网络投票协议[5,6]、JFK协议[7]等。

在拒绝服务攻击中非常重要的一类攻击就是利用了协议状态而产生的，例如，利用协议状态的保持来耗尽系统资源，产生资源消耗型拒绝服务攻击；修改协议状态，使其前后状态不一致而产生协议中止型拒绝服务攻击。因此，本文脱离以用户合约为基础的 Yu-Gligor形式化建模方法与以代价为基础的Meadows形式化建模方法，从协议状态的角度，对协议抗拒绝服务攻击性进行建模，分析与验证协议抗拒绝服务攻击性。由于标准应用PI演算[8]不能够对协议状态进行建模，为了能够使用基于应用PI演算ProVerif来自动化分析与验证协议抗拒绝服务攻击性，必须对标准应用PI演算进行扩展。首先从2个方面：一个是攻击者上下文，另外一个是进程表达式对标准应用PI演算进行扩展，然后应用扩展后的应用 PI演算对协议抗拒绝服务攻击性进行建模，提出一个基于定理证明支持一阶定理证明器ProVerif的抗拒绝服务攻击性自动化证明方法，最后应用ProVerif来分析与验证协议的抗拒绝服务攻击性。

2 相关的工作

目前，协议拒绝服务攻击形式化建模主要有 2类方法。

Yu和 Gligor基于时态逻辑，引入用户合约，提出了一个对共享服务拒绝服务攻击的形式化规范和验证方法。他们把拒绝服务攻击归结为新鲜性与安全性问题。Yu-Gligor形式化建模方法的核心思想是以访问控制策略为基础对拒绝服务攻击进行形式化建模，因此不能够处理在认证发生之前产生的拒绝服务攻击，如 SYN Floods攻击。此外 Yu-Gligor形式化建模方法不支持自动化工具。Millen[9]通过对时间逝去的明确度量对 Yu-Gligor形式化建模方法进行了扩展，使得它可以处理最大等待时间策略。Cuppens与 Saurel[10]应用模态逻辑和道义逻辑也对Yu和Gligor框架的可用性策略进行了形式化建模。

Meadows提出了基于代价的拒绝服务攻击形式化建模方法，该形式化建模方法通过设置容忍关系灵活的判断协议是否会产生拒绝服务攻击，适合对协议的资源消耗型拒绝服务攻击进行建模。Meadows声明其框架支持NRL协议分析器，但是没有给出具体例子。基于代价的形式化建模方法存在一个问题：在任何时候产生一个伪造的数据比验证它要花费的代价要小，按照Meadows形式化建模方法，那么所有的协议都不能够抵抗拒绝服务攻击。Ramachandran[11]应用 Meadows 形式化建模方法分析并指出 JFK协议具有抗拒绝服务攻击性。Smith[12]等应用 Meadows 形式化建模方法分析了JFK协议，声称在允许攻击者IP地址保密或者协议双方的DH协议的公钥可以重用的情况下，JFK协议存在2个拒绝服务攻击，但是我们认为他们的结论是值得商榷的。基于Meadows 形式化建模方法，Groza与 Minea[13]应用支持 ASLan规范语言的AVANTSSAR自动化工具对资源消耗型的拒绝服务攻击进行了建模，分析STS与JFK协议，指出STS协议不能抵抗拒绝服务攻击，JFK协议具有抗拒绝服务攻击性；Abadi和Blanchet[7]应用观察等价关系对抗拒绝服务攻击性进行建模，且应用PI演算分析并证明JFKr协议具有抗拒绝服务攻击性；Lafrance和 Mullins[14]应用安全进程代数 SPPA与容许干扰来对安全协议中的拒绝服务攻击进行建模，具体是通过引入“Impassivity”来描述攻击者通过利用低代价的行为来产生对协议另外一方的高代价行为的干扰，适合对资源消耗型拒绝服务攻击进行建模，并且分析证明1KP支付协议不能够抵抗拒绝服务攻击；周世健等学者[15]对串空间模型进行了扩展，分析了IEEE 802．11i四步握手协议抗拒绝服务攻击性，发现其存在拒绝服务攻击；Tritilanunt等[16,17]指出Meadows基于代价的形式化建模方法存在2个主要的问题：1) 仅仅考虑到诚实的协议参加方；2) 代价的分类方式太粗糙而不具有实用性。故他们应用着色Petri网提出了一个基于时间和代价的形式化拒绝服务形式化建模方法，分析了HIP协议，指出在攻击者为类型3（攻击者选择正确的客户端难题答案（client puzzle solution））和类型4（攻击者伪造客户端难题答案（client puzzle solution））情况下，存在拒绝服务攻击。

除了上述2类主要的形式化建模方法之外，Agha等[18]应用概率重写理论PMAUDE对拒绝服务攻击进行了形式化建模，应用CSL逻辑形式化描述拒绝服务攻击成功的概率，并且应用基于统计的模型检查器VESTA对TCP三步握手协议进行了分析，指出TCP三步握手协议不具有抗拒绝服务攻击性。Mahimkar和Shmatikov[19]基于博弈的ATL逻辑，对资源消耗与带宽消耗抗拒绝服务攻击性进行了建模，应用MOCHA模型检查器分析并证明JFKr协议具有抗拒绝服务攻击性。

3 扩展的应用PI演算

为了对协议状态及抗拒绝服务攻击性进行建模，从2个方面对标准应用PI演算进行扩展：一个是攻击者上下文，另外一个是进程表达式。扩展应用PI演算语义与标准应用PI演算相同。

3.1 攻击者上下文

按照攻击者对消息的攻击能力将攻击者所处的上下文分为现实上下文和理想上下文。

现实上下文形式化表示为

3.2 项

应用PI演算[5]是一个用来描述并发进程的语言。它继承了PI演算的通信与并发结构，增加了函数和等价理论。消息不仅是原子名，还可以是通过名字和函数构成的项。

项的定义如图1所示。用a、b、c、m、n等标识符及其组合表示名字，用x、y、z表示变量；也使用原语言变量u、v、w表示名字和变量；用f、g、h表示函数项，每个函数项都带有固定元数的参数，例如，encrypt（ m, k）表示函数encrypt有参数m和k。函数项是用来构造项的。因此，项M、N、T、V是变量，名字和函数项。

图1 项的定义

如果项M=f( M1,…,Mn)，则项M有子项Mi, i∈[1,n]。项Mi, i∈[1,n]也可能包含子项，不包含任何子项的项叫作原子项。项M用来描述协议中参与者之间相互交换的消息。变量可以描述任何消息或值，名字用来描述原子值，函数项用来描述从已知消息和值构造新的消息和值。

3.3 扩展后的进程

扩展后的进程如图2所示，空进程0不做任何操作；并行复合进程|P Q同时运行进程P和Q；复制进程!P并发执行无数个P进程；受限进程.n Pν首先产生一个新的私有名字n，然后执行P进程；条件进程分为2种：理想上下文中的条件进程if M =N then P else C和现实上下文中的条件进程if M = N then P else Q 。理想上下文中的条件进程if M =N then P else C.Q首先判断条件M N= 是否为真，如果为真，则执行P进程，否则执行C.Q 进程；现实上下文中的条件进程if M = N then P else Q 首先判断条件M = N 是否为真，如果为真，则执行P进程，否则执行Q进程；消息输入进程 u( x). P准备从通道u接受消息，并将接收到的消息与P中的x绑定，然后执行P进程；消息输出进程. P准备从通道u输出消息N，然后执行P进程。闭进程P从通道c输出消息M，当且仅当存在进程 P '和 P ''，使得

图2 扩展后的进程

3.4 进程上下文

进程上下文C是带洞([_])的进程表达式，如图3所示。if M = Nthen C else Q 表示如果项M与项N匹配，那么执行进程上下文C，则C是可验证上下文。if M = N then PelseC 表示如果项M与项N不匹配，那么执行进程上下文C，则C是不可验证上下文。

图3 进程上下文

4 定义和符号说明

定义1 带注解Alice-and-Bob 规范描述。

定义2 消息Ml认证性。

定义3 操作一致性。

定义41γ逻辑先于2γ。

P为协议带注解Alice-and-Bob 规范描述，S为P中操作的集合。对于S中的任意操作1γ和2γ，1γ逻辑先于2γ当且仅当：

3) 存在操作3γ，使得3γ逻辑先于2γ，1γ逻辑先于3γ。

定义5 关联集合。

协议中的任意消息 Mi和 Mj的关联集合 ω 为中验证操作v的数据项集合ʊ和 Mi的数据项的集合Ψ的交集，即 ω=ʊ∩Ψ。其中 i, j∈[1 , n]且i＜j。

关联集合ω反映了消息之间互相影响的程度：ω为空集，消息之间互不影响，是独立的，关联度为零；ω包含的数据项越多，消息之间互相影响的程度就越高，关联度越高。

定义6 抗拒绝服务攻击性。

P为协议带注解Alice-and-Bob 规范描述，B具有抗拒绝服务攻击性，当且仅当 ()Recv B中的任意一对消息iM和jM 的关联集合ω满足：

1) ω是空集∅；

2) ω中的每一个元素都是可认证的。

其中， R ecv( B)为协议P中参与者B所有处理消息的操作按逻辑先于组成的集合， i, j ∈[1,n]且i＜j。

如果协议 P中任意一对消息 Mi和 Mj之间互不关联，那么处理这两条消息的下文是互相独立的，则B具有抗拒绝服务攻击性；如果消息 Mi和Mj相关联，则对消息 Mj的处理依赖于对消息 Mi的处理，那么处理这2条消息的上下文是状态关联的，则消息 Mi和 Mj关联集合ω必须是可认证的才使B具有抗拒绝服务攻击性。

5 自动化证明抗拒绝服务攻击性方法

首先，应用扩展后的应用PI演算对协议带注解Alice-and-Bob规范描述进行精确的形式化建模。假设协议由 2n条消息组成，协议参加者为 Alice和Bob，Alice分别发送消息Mii∈[1,n]和接收消息Mi'i∈[1,n]，Bob分别接收消息Mii∈[1,n]和发送接收消息Mi'i∈[1,n]。协 议 进 程PP≡νn.（!A lice|!Bob）是封闭进程，由任意的发起者进程Alice和响应者进程Bob并行复合组成。根据扩展后的应用PI演算，进程Alice和Bob可以经过一系列的规约到达如图4所示某一个进程。

图4 可达进程

为了应用ProVerif对Bob的抗拒绝服务攻击性进行形式化分析，需要对 Bob收到的消息Mii∈[1,n -1]进行形式化建模，如果攻击者能够从公开信道c上获得秘密S，则攻击者可以通过对消息 Mi进行攻击使协议产生拒绝服务攻击。

首先对消息 M1进行建模。如图 5所示。在现实上下文中交换和处理消息 M1，在理想上下文中交换和处理消息协议进程PP， 其中，c1,c是公开信道，ci, i∈[2,n]是Bob接收消息Mi的隐私通道,

如果攻击者能够从公开信道c上获得秘密S，则攻击者可以通过对消息1M 进行攻击使协议产生拒绝服务攻击。

图5 消息M1的形式化模型

采用类似的方法对消息 Mi, i ∈[2,n -1]分别建立如图6所示的模型。在现实上下文中交换和处理消息 Mi，在理想上下文中交换和处理消息。协议进程PP为为PP≡ν（!Alicei|!Bobi），其中，ci, i∈[2,n-1],c是公开信道，cj,j∈[2,n-1]∩j≠i 是Bob接收消息Mi的隐私通道,。如果攻击者能够从公开信道c上获得秘密S，则攻击者可以通过对消息iM进行攻击使协议产生拒绝服务攻击。

图6 消息Mi的形式化模型

定理 抗拒绝服务攻击性。协议进程PP的响应者Bob具有抗拒绝服务攻击性当且仅当对Bob收到的所有消息Mi, i∈[1,n]的形式化模型，PP都不能从公共通道c输出秘密消息S，即不存在进程P'，P''和攻击者进程Attacker，使得。

证明

Bob具有抗拒绝服务攻击性，依据定义6，∀Mi, Mj∈Recv（ Bob），i, j∈[1,n]，Mi逻辑先于Mj，验证操作v是进程ifM=NthenP else，则对消息iM的形式化模型：

1) ω=∅即在协议规范描述中MN=的值与消息Mi无关，那么不论在理想上下文还是现实上下文中交换Mi，MN=的值恒为真，协议进程PP（→ ∪ ≡）*P ；

所以，对响应者Bob收到的所有消息Mi, i∈[1,n]的形式化模型，PP都不能从公共通道c输出秘密消息S。

如果对于响应者Bob收到的消息Mi, i∈[1,n]的形式化模型，PP能从公共通道c输出秘密消息S，即存在进程P'，P''和攻击者进程Attacker，使得，则攻击者Attacker可以通过篡改与v关联的逻辑先于Mj的消息，使M=N的值为假。那么关联集合ω存在不可认证项m'，所以协议进程PP的响应者Bob不具备防止拒绝服务攻击性。 证毕。

由定理可知如果攻击者能够获得秘密消息S，那么它能够构造一个拒绝服务攻击：在不影响其他消息正常交互的情况下，篡改消息iM的内容并使其不被接收者察觉，产生拒绝服务攻击。

至此，可以使用扩展后的应用PI演算对抗拒绝服务攻击进行形式化描述，基于给出的定理，应用ProVeif自动化证明协议的抗拒绝服务攻击性。

6 一阶定理证明器ProVerif

ProVerif[3]是Blanchet开发的基于重写逼近的一阶定理证明器。它基于Prolog语言，能够分析与验证使用Horn子句、应用PI演算及本文提出的扩展的应用PI演算描述的安全协议的安全性。同时，它克服了模型检测方法固有的缺陷－状态空间爆炸问题，能够处理无穷状态系统。ProVerif已经成功分析了很多复杂的安全协议，如电子商务协议[4]、网络投票协议[5,6]等。

ProVerif的体系结构如图7所示，由协议输入、处理和输出3部分组成。协议输入部分主要包括安全协议形式化描述和安全属性的形式化定义。ProVerif对输入的协议形式化描述进行初始处理，主要是语法检查。输入语言为应用 PI演算、Horn子句或者本文提出的扩展的应用PI演算。

处理部分负责根据安全协议的形式化描述对要证明的安全属性进行逻辑推导证明。它包括自动翻译模块和逻辑推导模块。当输入语言为应用 PI演算或本文提出的扩展的应用PI演算时，自动翻译模块主要负责实现安全协议的应用PI演算或本文提出的扩展的应用PI演算形式化描述到一阶逻辑规则的转换，逻辑推导模块则基于一阶逻辑规则对要证明的安全属性进行推理和验证。当输入语言为Horn子句时，处理部分为逻辑推导模块，不需要自动翻译模块。

结果输出部分主要负责输出处理结果。从输出结果可以得知该协议是否满足相应的安全属性，供用户进一步分析，但是ProVerif不输出详细的证明过程。如果不满足某安全属性，则ProVerif会给出详细的攻击方式。

图7 ProVerif结构

7 JFK与IEEE 802.11四步握手协议抗拒绝服务攻击性

7.1 JFK协议

JFK(just fast keying)协议是一个密钥交换协议，主要有JFKr和JFKi 2个版本，主要区别是对协议双方提供不同的身份保护。JFKr基于Sign-and-MAC协议[20]，能够在有主动攻击者的环境中保护响应者的身份，在被动攻击者的环境中保护发起者的身份。JFKi基于ISO 9798-3 密钥交换协议[21]，能够在有主动攻击者的环境中保护发起者的身份。Abadi和Blanchet[7]应用应用PI演算分析了对JFKr协议的秘密性、认证性、可否认性，同时用手工的方式分析了JFKr抗拒绝服务攻击性，指出JFKr协议可以抵抗拒绝服务攻击。Aiello等学者[22,23]采用非形式化的方法分析了JFK协议的安全性。这里主要应用提出的自动化抗拒绝服务攻击方法分析JFKr协议的抗拒绝服务攻击性。

JFKr协议涉及2个角色：协议的发起者Alice和协议的响应者Bob。攻击者建模为Dolev-Yao模型中的攻击者，既可以在公开信道上监听、拦截、修改，删除和插入消息，又可以伪装成诚实的参与者。

JFKr协议的Alice-and-Bob 规范描述如图8所示，符号说明见文献[17]。

图8 JFKr协议的Alice-and-Bob 规范描述

JFKr协议有4条消息组成，消息1和消息2通过Diffie-Hellman密钥交换协议建立共享密钥。首先Alice生成公钥Alicex和随机数AliceN，发送给Bob。Bob生成公钥Bobx、随机数BobN，认证cookieBobt。tBob是状态信息的MAC值。是Bob成功收到消息1准备发送消息2时的自己环境状态。消息3和消息4提供认证性。消息3和消息4包含加密随机数、Diffie-Hellman指数及其他信息的签名。Alice生成消息3发送给Bob，Bob验证消息3中状态信息的MAC值tBob的正确性。如果验证成功，Bob用及eK生成加密后的身份标识eBob及其MAC值hBob组成消息4发送给Alice。

基于提出的抗拒绝服务攻击性自动化证明方法，应用扩展的应用PI演算对JFKr协议响应者Bob收到的消息1进行建模，然后转换成ProVerif的输入语言，最后应用ProVerif对JFKr协议进行分析。由于空间的限制，只给出了ProVerif的分析结果，如图9所示。图9表明公开通道c没有输出秘密信息dos。

图9 JFKr的ProVerif输出结果

根据消息1形式化模型，得知Bob处理收到的消息1和消息3的操作是Recv( Bob){ act( Bob)验证操作v是对的验证，其中，。所以消息1和消息3的关联集合ω为空集。这和ProVerif在公开通道c的输出是一致的。由定义6可知JFKr中的响应者Bob能够防止拒绝服务攻击。

7.2 IEEE 802.11 i四步握手协议

IEEE 802.11标准是无线局域网中广泛采用的标准。由于IEEE 802.11标准被证明在实体认证和有线等价保密方面是不安全的，IEEE 802.11i标准[21]被提出来增强IEEE 802.11的安全性。IEEE 802.11i除了引入了新的密钥管理和生成算法，还改进了加密和认证算法。它定义了一个基于IEEE 802.1X认证和4步握手的强安全网络关联。Bicakcia与Tavli[24]对IEEE 802.11的拒绝服务攻击与防范措施进行了深入研究。

四步握手协议简化了的Alice-and-Bob 规范描述如图10所示。

图10 四步握手协议的Alice-and-Bob 规范描述

其中，Anonce和Snonce分别为认证者Alice和请求者Bob生成的随机数，它用来生成PTK（Pairwise Transient Key）。m1、m2、m3、m4分别为不同的消息，其中，m1、m2、m3、m4都包含有重放计数值Replay_Counter。MIC2=MIC（Snonce,m2）,MIC3=MIC（Anonce,m3）,MIC4=MIC（m4），MIC（message integrity code）值为消息完整性码。

四步握手协议运行过程如下：首先认证者Alice首先发送消息1M给请求者Bob，请求者Bob收到消息M1后，首先验证重放计数值_ReplayCounter的有效性，验证通过则产生一个随机数Snonce，然后应用伪随机函数PRF(pseudo random functions)生成临时密钥PTK。伪随机函数PRF输入为Anonce、Snonce与其他信息。请求者Bob生成MIC值，把消息M2发送给认证者Alice。认证者Alice收到消息2M后，计算临时密钥PTK值，验证M2中的MIC值，生成消息3M给请求者Bob。请求者Bob收到消息M3对MIC值进行验证，如果成功，生成并发送消息M4给认证者Alice，安装PTK。认证者Alice在收到M4后对MIC值进行验证，如果验证成功，安装PTK。至此四步握手结束，产生并安装PTK。

应用提出的自动化抗拒绝服务攻击性证明方法，ProVerif给出了两个拒绝服务攻击：拒绝服务攻击1，如图11和图12所示。拒绝服务攻击2，如图13和图14所示。其中拒绝服务攻击2是应用我们提出的方法发现的。。

根据四步握手协议规范，由于请求者Bob对消息M3的验证依赖于临时密钥PTK，而临时密钥PTK的生成取决于Anonce和Snonce，Snonce的产生又依赖于对消息M1的重放计数值Replay_Counter的有效性验证，所以攻击者只要成功篡改或重放Anonce与计数值Replay_Counter，就可以使请求者Bob对合法的消息M3的验证失败，从而产生拒绝服务攻击。

根据消息M1形式化模型，请求者Bob处理消息M1和消息M3的操作Recv(Bob){act(Bob)其中，v是验证操作，。所以M1和M3的关联集合ω=｛Anonce1｝。由于四步握手协议没有对Anonce1进行验证，Anonce1是不可认证的，由定义6可知四步握手协议中的请求者Bob不能防止拒绝服务攻击。

拒绝服务攻击1，如图11和图12所示。图11表明公开通道c输出秘密信息S。ProVerif构造的拒绝服务攻击1如图12所示：在协议的一次运行中，请求者Bob收到消息M3前，攻击者伪造一个随机数Anonce'和重放计数值Replay_Counter（'使Replay_Counter'的值为有效值），并生成消息M1发送给请求者Bob，根据四步握手协议规范，请求者Bob重新生成PTK，此时Bob收到合法的消息M3，将不能通过对 MIC值验证。根据四步握手协议规范，认证者Alice在将重新发送M3，但仍然不能通过验证，n次这样的验证后，认证者Alice将和请求者Bob重新开始认证。从而产生拒绝服务攻击。

图11 针对拒绝服务攻击1的ProVerif输出

图12 ProVerif输出的拒绝服务攻击1

拒绝服务攻击2，如图13和图14所示。图13表明公开通道c输出秘密信息S。ProVerif构造的拒绝服务攻击2如图14所示。拒绝服务攻击2与拒绝服务攻击1基本上是相同的，区别是攻击者只伪造重放计数值 Replay _ C ounter'，使Replay _ C ounter'的值为有效值。

图13 针对拒绝服务攻击2的ProVerif输出

图14 ProVerif输出的拒绝服务攻击2

针对拒绝服务攻击1，He[25]提出请求者Bob除了存储 PTK，另外为每一个消息M1存储一个TPTK(temporary PTK )，在收到消息M1时，仅更新TPTK，在收到正确的消息M3时才更新PTK。但是，当攻击者大量发送伪造的消息M1时，Bob就会存储大量的 TPTK，产生存储资源消耗型的拒绝服务攻击。

基于以上分析， 为了防止拒绝服务攻击1和2，我们认为使消息M1可认证即可。具体方案是应用认证者 Alice的签名密钥对M1进行签名或使用MSK对M1进行加密。这样就使消息1是可认证的，来防止拒绝服务攻击1和2。在通过认证以后再分配资源。

如果只防止拒绝服务攻击 2，那么请求者 Bob可以存储其在一定时间内收到的Anonce，并且在进行下一步处理前，检查Anonce是否是在一定时间内是重放的，则可以防止这种攻击。

8 结束语

拒绝服务攻击具有威害巨大及难以有效防御的特点，受到网络安全专家与用户的重点关注。形式化方法是分析协议安全性强有力的工具。本文没有遵循Yu-Gligor形式化建模方法和Meadows形式化建模方法，而是从协议状态的角度，应用形式化方法对拒绝服务攻击性进行建模。首先从攻击者上下文与进程表达式2个方面对标准应用PI演算进行扩展，然后应用扩展后的应用PI演算对协议的抗拒绝服务攻击性进行建模，提出了一个基于定理证明的支持一阶定理证明器ProVerif的抗拒绝服务攻击性自动化证明方法，最后应用ProVerif分析与验证了JFK协议与IEEE 802.11四步握手协议抗拒绝服务攻击性，证明JFK协议能够抵抗拒绝服务攻击，而IEEE 802.11四步握手协议的确存在拒绝服务攻击，同时也发现了IEEE 802.11四步握手协议的一个新的拒绝服务攻击。针对IEEE 802.11四步握手协议存在的攻击提出了2种改进方法。由于提出的抗拒绝服务攻击性自动化证明方法主要从协议状态来分析协议抗拒绝服务攻击性，因此既可以分析利用协议状态的保持产生的资源消耗型拒绝服务攻击，又可以分析协议中止型拒绝服务攻击，但是在分析由其他原因产生的存储资源消耗型的拒绝服务攻击方面还有欠缺，可以作为下一步的工作方向。同时在未来的工作中，计划应用提出的基于定理证明的支持一阶定理证明器ProVerif的抗拒绝服务攻击性自动化证明方法对复杂的电子商务、电子投票协议的抗拒绝服务攻击性进行深入的研究，验证其抗拒绝服务攻击性。

[1] YU C，GLIGOR V. A formal specification and verification method for the prevention of denial of service[J]. IEEE Transactions on Software Engineering, 1990, 16(6):581-592.

[2] MEADOWS C. A cost-based framework for analysis of denial of service networks[J]. Journal of Computer Security, 2001,9(1/2):143-164.

[3] BLANCHET B. An efficient cryptographic protocol verifier based on prolog rules[A]. Proc of the 14th IEEE Workshop on Computer Security Foundations Workshop (CSFW)[C]. Cape Breton, Nova Scotia,Canada, 2001.82-96.

[4] 郭云川, 丁丽, 周渊等. 基于 ProVerif的电子商务协议分析[J]. 通信学报,2009,30(3):125-129.GUO Y C, DING L, ZHOU Y, et al. E-commerce protocol analysis based on ProVerif[J]. Journal on Communications, 2009, 30(3):125-129.

[5] MENG B, HUANG W, LI Z M, et al. Automatic verification of security properties in remote Internet voting protocol with applied pi cal-culus[J]. International Journal of Digital Content Technology and its Applications, 2010, 4(7):88-107.

[6] MENG B. Refinement of mechanized proof of security properties of remote Internet voting protocol in applied PI calculus with ProVerif[J].Information Technology Journal, 2011, 10(2):293-334.

[7] ABADI M, BLANCHET B, FOURNET C. Just fast keying in the pi calculus[J]. ACM Transactions on Information and System Security,2007, 10(3):1-59.

[8] ABADI M, FOURNET C. Mobile values, new names, and secure communication[A]. Proc of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)[C]. London,UK, 2001.104-115.

[9] MILLEN J K. A resource allocation model for denial of service protection[J]. Journal of Computer Security, 1993, 2(2-3):89-106.

[10] CUPPENS F, SAUREL C. Towards a formalization of availability and denial of service[A]. Proc of Information Systems Technology Panel Symposium on Protecting Nato Information Systems in the 21st Century[C]. Washington, 1999.

[11] RAMACHANDRAN V. Analyzing DoS-Resistance of Protocols Using a Cost-based Framework[R]. Technical Report DCS/TR-1239,Yale University, 2002.

[12] SMITH J,GONZALEZ-NIETO J M,BOYD C. Modelling denial of service attacks on JFK with Meadows's cost-based framework[A]. Proc of the 2006 Australasian Workshops on Grid Computing and E-Research(ACSW Frontiers)[C]. Darlinghurst, Australia, 2006. 125-134.

[13] GROZA B, MINEA M. Formal modelling and automatic detection of resource exhaustion attacks[A]. Proc of 6th ACM Symposium on Information, Computer and Communications Security (ASIACCS)[C].HongKong,China, 2011.

[14] LAFRANCE S, MULLINS J. Using admissible interference to detect denial of service vulnerabilities[A]. Proc of the Sixth International Workshop in Formal Methods (IWFM)[C]. Ireland,2003.

[15] 周世健, 蒋睿, 杨晓辉. 安全协议DoS攻击的形式化分析方法研究[J].中国电子科学研究院学报.2008, 3(6):592-598.ZHOU S J, JING R, YANG X H. DoS attacks on security protocols of the formal analysis[J]. Journal of Research Institute of China Electronics, 2008, 3(6):592-598.

[16] TRITILANUNT S,BOYD C,FOO E, et al. Cost-based and time-based analysis of DoS-resistance in HIP[A]. Proc of the Thirtieth Australasian Conference on Computer Science (ACSC '07)[C]. Darlinghurst,Australia, 2007.191-200.

[17] TRITILANUNT S. Protocol Engineering for Protection Against Denial of Service Attacks[D]. Brisbane Australia, Queensland University of Technology, 2009.

[18] AGHA G, GREENW ALD M, GUNTER C A, et al. Formal modeling and analysis of DoS using probabilistic rewrite theories[A]. Proc of International Workshop on Foundations of Computer Security(FCS)[C].Chicago IL,2005.

[19] MAHIMKAR A, SHMATIKOV V. Game-based analysis of denial-of-service prevention protocols[A]. Proc of the 18th IEEE workshop on Computer Security Foundations (CSFW)[C]. Aix-en-Provence,France, 2005.287-301.

[20] KRAWCZYK H. Invited talk, SIGMA: the SIGn-and-MAc approach to authenticated diffie Hellman and its use in the IKE protocols[A].Proc of the 23rd Annual International Cryptology Conference(CRYPTO)[C]. Santa Barbara, California, USA, 2003.400-425.

[21] CANETTI R , KRAWCZYK H. Analysis of key-exchange protocols and their use for building secure channels[A]. Proc of the International Conference on the Theory and Application of Cryptographic Techniques: Advances in Cryptology (EUROCRYPT)[C]. Innsbruck, Austria, 2001.453-474.

[22] AIELLO W, BELLOVIN S M, BLAZE M, et al. Efficient,DoS-resistant, secure key exchange for Internet protocols[A]. Proc of the 9th ACM Conference on Computer and Communications Security(CCS)[C]. Washington, DC, USA, 2002.48-58.

[23] AIELLO W, BELLOVIN S M, BLAZE M, et al. Just fast keying: key agreement in a hostile internet[J]. ACM Transactions on Information and System Security, 2004, 7(2):242-273.

[24] BICAKCIA K, TAVLI B. Denial-of-service attacks and countermeasures in IEEE 802.11 wireless networks[J].Computer Standards & Interfaces, 2009, 31(5):931-941.

[25] HE C, MITCHELL J C. Analysis of the 802.11i 4-way handshake[A].Proc of the 3rd ACM Workshop on Wireless Security (WiSe '04)[C].ACM, New York, NY, USA, 2004.43-50.