金大鹏， 林宏刚

(成都信息工程大学信息安全工程学院，四川成都610225)

0 引言

DoS攻击是一种常见的网络攻击方式［1］，是通过各种手段使提供服务的主机无法提供正常服务的一种攻击，按照攻击方式可分为:物理破坏型、服务中止型、资源消耗型。传统的形式化分析方法，如BAN类逻辑等，往往注重的是协议的认证性、秘密性等，忽略了协议的可用性，无法及时发现协议存在的DoS攻击。随着互联网的飞速发展，DoS攻击带来的危害越来越大，因此，已经有专家学者对DoS攻击的形式化建模方法进行了深入研究。

Meadows提出的基于代价的形式化分析方法［2-4］，适合对资源消耗型DoS攻击进行建模，该建模方法通过设置容忍关系，比较产生一个数据和验证这个数据所要花费的代价大小，判断协议是否存在DoS攻击。基于Meadows的形式化分析模型，Minea与Groza分析了JFK与STS协议［5］，指出 JFK协议能够抵抗DoS攻击，而STS协议不具有抗DoS攻击能力。基于时态逻辑，Yu和Gligor引入用户合约，提出一种对共享服务DoS攻击的形式化规范与验证方法［6］，该方法的核心思想是以访问控制策略为基础，对DoS攻击进行建模，所以不能处理发生在认证之前的DoS攻击。周世健等［7］在基本串空间的基础上［8-10］，进行了扩展，提出了判断安全协议DoS攻击分析的2条检验规则，并利用这两条规则，分析了IEEE802.11i 4步握手协议，发现其存在的DoS攻击，并针对此提出了改进办法。这些规则是基于代价，能够较好地分析资源消耗型DoS攻击，但是对服务中止型DoS攻击却无能为力。孟博等［11］从进程表达式和攻击者上下文2个方面扩展了标准应用PI演算，并且从协议状态的角度，建立安全协议抗DoS攻击分析模型，并验证了模型的有效性。由于该方法主要是从协议状态的角度分析抗DoS攻击性，因此可以分析由于协议的状态保持而产生的资源消耗型DoS攻击，以及服务中止型DoS攻击，但是在分析其他原因产生的资源消耗型DoS攻击时还存在不足。

提出一种扩展的串空间模型，在基本串空间模型中引入消息相关度集合，代价函数，使串空间模型能够全面、有效地分析安全协议是否存在DoS攻击。

1 扩展的串空间模型理论

以基本串空间模型为基础，参考Meadows提出的基于代价的DoS攻击形式化建模方法，在串空间模型中引入消息相关度集合，使模型能够分析服务中止型DoS攻击;引入代价函数，使模型能够分析资源消耗型DoS攻击。新的模型保留了串空间模型原有的分析协议安全性的优点，同时具有对协议是否能够抵抗DoS攻击进行全面分析的能力。

1．1 串空间模型基本概念

Fabrega，Herzog和Guttman在1998年提出了串空间模型理论，用于分析认证协议。串空间包含诚实主体的串和攻击者的串，利用串空间模型，能够证明协议的认证性与机密性，以下为详细的串空间模型介绍。

设集合A中的元素为协议主体交换的消息，则称A为项集合，A的元素为项。

定义1 集合{+，-}是串空间的动作集，其中“+”表示发送消息的动作，“-”表示接收消息的动作。

定义2 二元组＜σ，a＞表示一个事件，其中σ∈{+，-}，a∈A。用+a和-a代表一个事件.TIF，+a和-a称为带符号的消息。(±A)*为带符号项的有限序列集合。

定义3 串是协议参与者所执行事件的序列，令∑表示串的集合，定义迹映射tr:∑→(±A)*，将一个串映射到有限消息序列的集合。

定义4 串空间的其他基本概念:

(1)结点，假设串s∈∑，s中的每个事件称为串s的一个结点，用n=＜s，i＞表示，其中i是结点n在串中序号。结点n属于串s，记为n∈s，结点的集合记为N。

(2)结点 n= ＜s，i＞ ∈s，定义 index(n)=i，strand(n)=s，若结点n代表的实体动作为(tr(s))i=σa，定义 term(n)=σa，uns-term(n)=((tr(s))i)2=a，sign(n)=σ，称term为结点事件函数，uns-term(n)为结点消息函数，sign为结点符号函数。

(3)结点 n1，n2∈N，存在一个边 n1→n2，当且仅当term(n1)=+a，term(n2)=-a，称 n1发送消息 a给n2，或者n2从n1接收消息a。

(4)若 n1= ＜s，i＞，n2= ＜ s，i+1 ＞，则存在边 n1⇒n2，称作事件相继发生，表示事件n2在事件n1之后发生，称n1是n2在同一个串上的因果前驱。

1．2 消息相关度集合

若结点 ni，nj属于 N，Mi为 term(ni)的所有子项构成的集合，Mj为term(nj)的所有子项构成的集合，则结点ni，nj的消息相关度集合定义为集合Mi与集合Mj的交集O，集合O反应了结点ni和nj的消息相关程度，若O为空集，表明ni和nj是不相关的，反之，若集合O中包含的元素越多，表明结点ni和nj的消息相关程度越高。

1．3 代价函数

如图1所示，定义代价函数为边n1→m1及m1⇒m2的集合到非负实数R的映射，其中边n1→m1到非负实数R的映射用函数f表示，若n1发送消息a给m1，则fa表示n1产生并发送消息a所付出的代价值;边m1⇒m2到非负实数R的映射用函数g表示，若结点m1接收了来自另一个串的消息a后，由事件m1变为事件m2，则ga表示接收并对消息a进行处理所付出的代价值。

图1 代价函数串空间模型

2 基于扩展的串空间模型的DoS攻击分析方法

利用上文提出的消息相关度集合和代价函数，提出两条检验规则，分析安全协议抗服务中止型DoS攻击和资源消耗型DoS攻击的能力。

服务中止型DoS攻击产生的原因是协议本身存在缺陷，当攻击者篡改请求者数据，或者发送伪造的虚假数据时，响应者却不能及时发现，仍然当作正常的数据处理，导致认证失败，协议不能继续向下执行，造成DoS。基于此，提出如下规则1。

规则1:设s是协议的响应者串，ni，nj是s中满足sign(ni)=-，sign(nj)=-的任意两个结点，其中i＜j，O为ni和nj的消息相关度集合，若O满足以下条件之一:

(1)O是空集;

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

则协议的响应者能够抵抗服务中止型DoS攻击。

如果O是空集，说明这两条消息的处理的数据是互不相关的，响应者能够抵抗服务中止型DoS攻击;如果O不为空集，说明ni中的数据和nj中的数据是相关的，集合O中的数据必须是可认证的，响应者才具有抗服务中止型DoS攻击的能力，

不同于服务中止型DoS攻击，资源消耗型DoS攻击的实质是攻击者向响应者发送大量伪造的请求信息，使响应者在对这些消息进行认证以及维持连接的过程中用尽自身资源，造成DoS。因此，要想防止资源消耗型DoS攻击，必须使协议发起者付出比协议响应者更多的资源，基于此，提出如下规则2。

规则2:如图 2 所示，设结点 n1，m1，m2，边 n1→m1，m1⇒m2，n1属于发起者串，m1，m2属于响应者串，若边m1⇒m2的代价函数ga小于边n1→m1的代价函数fa，那么协议由n1运行到m2，能够抵抗资源消耗型DoS攻击。

图2 规则2串空间模型

可以用上面的两条规则形成形式化分析方法检测安全协议的抗DoS攻击能力，如果一个安全协议的响应者串满足规则1，则响应者能够抵抗服务中止型DoS攻击;如果响应者串满足规则2，则能够抵抗资源消耗型DoS攻击。

3 IEEE802．11i 4步握手协议与 JFK协议抗DoS攻击性分析

3．1 IEEE802．11i 4 步握手协议

IEEEE802.11i标准在无限局域网中具有更好的认证性和机密性，认证过程包括3个实体:认证服务器(AS)，认证者(AP)，申请者(STA)。完整过程包括STA和AP之间的握手，AP和AS之间的握手，以及STA和AP之间的握手。经过握手，STA和AS相互认证并形成一个主会话密钥(MSK)，AS将MSK安全的传输给 AP。STA和 AP，分别用 MSK生成相同的PMK，当作握手协议生成临时密钥(PTK)的材料。

4步握手可简化为如下描述:

消息 M1:AP→STA:Na，Sn，m1

消息 M2:STA→AP:Ns，Sn，m2，{Ns，Sn，m2}kck

消息 M3:AP→ STA:Na，Sn+1，m3，{Na，Sn+1，m3}kck

消息 M4:STA → AP:Ns，Sn+1，m4，{Ns，Sn+1，m4}kck

其中，Na，Ns分别是 AP和 STA 的随机数，Sn，Sn+1为重放计数值，m1，m2，m3，m4为其他不同的信息，kck用来计算消息完整性验证码。具体过程如下:首先AP向STA发送M1，STA收到M1后，验证重放计数值，通过则产生随机数Ns，以及其他信息，利用这些信息计算临时密钥PTK以及完整性验证码{Ns，Sn，m2}kck，然后生成消息M2发送给AP，AP收到M2后，计算PTK，并验证完整性验证码，然后生成消息M3，发送给STA。STA收到M3后，进行消息完整性验证，验证成功，则生成M4发送给AP，安装PTK。AP收到M4后，进行完整性验证，成功则安装PTK，4步握手完成。

4步握手协议扩展的串空间模型，如图3所示，其中AP和STA是协议的参与双方，fM1、fM3分别为AP生成并发送消息M1、M3所付出的代价值，fM2、fM4分别为STA生成并发送消息M2、M4所付出的代价值，gM1、gM3分别为STA接收并处理消息M1、M3所付出的代价值。

图3 4步握手协议扩展串空间模型

3.1.1 抗服务中止型DoS分析

消息 M1的所有子项组成的集合 O1:{Na，Sn，m1}，消息 M2的所有子项组成的集合 O2:{Ns，Sn，m2，{Ns，Sn，m2}kck}，消息 M3的所有子项组成的集合 O3:{Na，Sn+1，m3，{Na，Sn+1，m3}kck}，消息 M4的所有子项组成的集合 O4:{Ns，Sn+1，m4，{Ns，Sn+1，m4}kck}，其中，Sn与Sn+1只相差数值1，可认为是同样的子项。

STA收到的M1，M3的消息相关度集合O13:{Na，Sn}，M1是明文传输，其中的 Na，Sn都是明文，AP接收到M1后，并不能确定M1的准确来源，所以Na和Sn都是不可认证的，根据规则1，存在针对STA的服务中止型DoS攻击。

事实上已经被证实存在针对STA的服务中止型DoS攻击，由于消息M1是明文传输，攻击者很容易截取M1并得到其中STA和AP的MAC地址，之后单独伪造 Na＇或 Sn＇，或者同时伪造 Na'和 Sn'，且 Na'和 Sn＇均是有效值，在STA收到合法的消息M3前，发送伪造的M1＇给STA，STA在收到 M1＇后，重新计算生成新的PTK＇，此时STA收到合法的M3后，将导致STA无法通过对M3的MIC校验，根据协议规则，M3将被丢弃，STA将继续等待，在超过一段间隔后，AP没有接收到来自STA的M4，就会重新发送M3，但同样不能通过MIC校验，导致握手失败。根据协议规则，AP再一次发起对STA的认证请求。

AP收到的消息M2，M4的消息相关度集合O24:{Ns，Sn}，Ns和Sn在消息M2，M4也是明文形式出现，但是因为完整性校验码MIC，AP收到消息M2和M4后，先提取Ns，计算PTK，然后验证MIC码，因为只有STA具有相同的PTK，所以如果验证MIC成功，则可确定M2和M4来自STA，且未经篡改，否则不是来自STA。因此，M2和M4的消息相关度集合O24是可认证的，根据规则1，不存在针对AP的服务中止型DoS攻击。

3.1.2 抗资源消耗型DoS分析

对于STA，结点 ＜AP，1＞，＜STA，1＞，＜STA，2＞构成丛一，结点 ＜AP，3＞，＜STA，3＞，＜STA，4＞构成丛二。在丛一中，AP产生随机数Na，重放计数值Sn，并和自己的MAC地址一同生成M1发给STA，付出的代价值为fM1;STA接收到M1后，首先取出Na，然后产生随机数Ns，之后再利用PMK，算出PTK并存储，然后计算完整性校验码MIC，发送消息M2给AP，付出的代价是 gM1。比较 fM1和 gM1，可知 gM1大于fM1，根据规则2，存在对STA的DoS攻击，但是由于STA并不会同时发起多个认证，所以只存储一个STA，所以不会产生资源消耗型DoS攻击。同样分析丛二，也不会出现针对STA的资源消耗型DoS。

对于AP，结点结点 ＜STA，2＞，＜AP，2＞，＜AP，3＞构成丛三。丛三中，STA产生并发送M2的代价是fM2，AP接收到并处理M2，付出的代价是gM2，fM2大于gM2，根据规则2，AP在此处能够防止资源消耗型DoS。

3．2 JFK 协议

JFK协议是一种新的Internet密钥交换协议，分为JFKr和JFKi两种变种协议，其中JFKi主要应用在C/S模式，能够保护发起者的身份;JFKr主要适用于P2P模式，每一个响应者都能够保护自己的身份信息。

JFKr协议可简化为如下描述，符号说明见表1。

消息 M1:I→R:Ni，xi

消息 M1:R→I:Ni，Nr，xr，tr

消息 M1:I→R:Ni，Nr，xi，xr，tr，ei，hi

消息 M1:R→I:er，hr

表1 JFKr协议符号说明

接下来，采用扩展后的串空间模型对JFKr协议进行建模，如图4所示。

JFKr协议包含4条消息，消息M1和消息M2建立共享密钥，首先发起者产生公开密钥xi，和随机数Ni，发送给响应者。响应者产生公开密钥xr，随机数Nr，认证信息 tr，其中 tr是状态信息(xr，Nr，Ni)的 MAC值。(xr，Nr，Ni)是响应者成功接收消息M1，准备发送消息M2时的环境状态。消息M3和消息M4提供认证性，包含Diffie-Hellman指数、加密随机数和其他信息的签名。发起者生成消息M3发送给响应者，响应者验证M3中状态信息的MAC值tr的正确性，如果验证通过，响应者生成加密后的身份标识符er及其MAC值hr组成消息M4发送给协议发起者。

图4 JFKr协议扩展串空间模型

3.2.1 抗服务中止型DoS分析

JFKr协议中，消息 M1的所有子项组成的集合O1:{Ni，xi}，消息M2的所有子项组成的集合O2:{Ni，Nr，xi，xr}，消息 M3的所有子项组成的集合 O3:{Ni，Nr，xi，xr}，消息 M4的所有子项组成的集合 O4:{Ni，Nr，xi，xr}。

响应者收到的消息 M1，M3的消息相关读集合O13:{Ni，xi}，发起者收到的 M2，M4的消息相关度集合O24:{Ni，Nr，xi，xr}，因为 M3和 M4中，双方的身份信息都被加密，且进行了MAC值计算，且双方的私钥都由自身保管，不被泄漏，因此保证了消息相关度集合O13和O24中的项都是可认证的，根据规则1，JFKr协议能够防止服务中止型DoS攻击。

3.2.2 抗资源消耗型DoS分析

对于响应者，付出的资源消耗主要是gM1和gM3，发起者对应付出的代价是fM1和fM3。首先，发起者产生随机数Ni，之后计算公钥xi，并存储Ni和 xi，付出代价是fM1。响应者接收M1后，生成随机数，计算MAC值作为Cookie，最多的资源消耗就是计算MAC值，但是在不确定发起者的合法身份前，不会保留发起者有关的状态信息，没有存储资源消耗，因此满足fM1大于gM1。发起者收到M2后，利用Ke和Ka对身份信息加密，并计算其MAC值hi，连同收到的Cookie值以及双方的随机数，公开密钥等信息，组成消息M3，发给响应者，此过程中发起者付出的代价值是fM3。响应者接收到M3后，首先再次计算Cookie值，并和M3中的Cookie比较，只有验证通过，才进行后续操作，之后再计算生成身份标识符er及其MAC值hr，此过程中响应者付出代价是gM3小于发起者付出的代价fM3。经过以上分析，根据规则2，JFKr协议能够防止资源消耗型DoS攻击。

4 结束语

针对安全协议中存在的DoS攻击，对基本的串空间模型进行扩展，提出一种形式化的分析方法，能够较为全面地分析安全协议存在的服务中止型以及资源消耗型DoS攻击，并且利用该模型对IEEEE802.11i协议中的4步握手协议以及JFK协议进行分析，发现IEEEE802.11i 4步握手协议中存在的DoS攻击，验证了JFK协议具有抗DoS攻击的能力。不足的是，模型只能够分析在攻击者和响应者系统资源相当情况下的资源消耗型攻击，当有大量的攻击者发起分布式DoS攻击时，还需要更好的办法进行应对，在接下来的研究中将以此为重点。

［1］ 卫剑钒，陈钟，段云所，等.一种认证协议防御拒绝服务攻击的设计方法［J］.电子学报，2005，33(2):288-293.

［2］ Meadows C.A formal framework and evaluation method for，network denial of service［C］//Proceedings of 12th IEEE Computer，Security Foundations Workshop，1999:4-13.

［3］ Meadows C.A cost-based framework for analysis of denial of service networks［J］.Journal of Computer Security，2001，9:143-164.

［4］ Meadows C.Formal Methods for Cryptographic Protocol Analysis:Emerging Issues and Trends［J］.IEEE Journal on Selected Areas，in Communications，2003，21(1):44-54.

［5］ GROZA B，MINEA M.Formal modelling and automatic detection of resource exhaustion attacks［A］.Proc of 6th ACM Symposium on Information，Computerand Communications Security(ASIACCS)［C］.HongKong，China，2011.

［6］ 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.

［7］ 周世健，蒋睿，杨晓辉.安全协议 DoS攻击的形式化分析方法研究［J］.中国电子科学研究院学报，2008，3(6):592-598.

［8］ Fabregaf，Herzog，Guttmanj.Strand space:Why is a Security Protocol Correct［C］//Proceedings of，the 1998 IEEE Symposium on Security and Privacy，IEEE，Computer Society Press.1998:160-171.

［9］ Thayer FJ，Herzog JC，Guttman JD.Strand spaces:Proving security protocols correct［J］.Journal of Computer Security，1999，7(2-3):191-230.

［10］ Thayer FJ，Herzog JC，Guttman JD.Strand spaces:Honest ideals on strand spaces［C］.In:Proceedings of the 1998 IEEE Computer Security Foundations Workshop.LosAlamitos:IEEE Computer Society Press，1998:66-77.

［11］ 孟博，黄伟，王德军，等.协议抗拒绝服务攻击性自动化证明［J］.通信学报.2012，(3).

［12］ 卿斯汉.安全协议20年研究进展［J］.软件学报，2013，14.

［13］ Ramachandran V.Analyzing DoS-Resistance of Protocols Using a Cost-based Framework［R］.Technical Report DCS/TR-1239，Yale University，2002.

［14］ 李建华.网络安全协议的形式化分析与验证［M］.北京:机械工业出版社，2010.

［15］ 冯登国.网络安全原理与技术［M］.北京:科学出版社，2003.