协议抗拒绝服务攻击性自动化证明  

Automatic proof of resistance of denial of service attacks in protocols

作　　者：孟博[1] 黄伟[1] 王德军[1] 邵飞[1] 

机构地区：[1]中南民族大学计算机科学学院,湖北武汉430074

出　　处：《通信学报》2012年第3期112-121,共10页Journal on Communications

基　　金：国家民委基金资助项目(10ZN09);国家自然科学基金资助项目(60603008);中南民族大学自然科学基金资助项目(YZZ09008);武汉市科技型中小企业技术创新基金资助项目(SZY11008)~~

摘　　要：首先从攻击者上下文与进程表达式2个方面对标准应用PI演算进行扩展,然后从协议状态的角度,应用扩展后的应用PI演算对协议抗拒绝服务攻击性进行建模,提出一个基于定理证明支持一阶定理证明器ProVerif的抗拒绝服务攻击性自动化证明方法,最后应用ProVerif分析与验证了JFK协议与IEEE 802.11四步握手协议抗拒绝服务攻击性,发现IEEE 802.11四步握手协议存在一个新的拒绝服务攻击,并且针对IEEE 802.11四步握手协议存在的拒绝服务攻击提出了改进方法。First,the applied PI calculus was extended from two aspects： attacker contexts and process expression,then from the view of protocol state,the protocols were modeled with the extended applied PI calculus and a automatic method of proof of resistance of denial of service attacks based on theorem proof with first order theorem prover ProVerif was presented,finally resistance of denial of service attacks in JFK protocol and IEEE 802.11 four-way handshake pro-tocol were analyzed.The results obtained are that JFK protocol is resistance of denial of service attack and IEEE 802.11 four-way handshake protocol is not.At the same time a new denial of service attack in IEEE 802.11 four-way handshake protocol was found.The methods to prevent resistance of denial of service attacks in IEEE 802.11 four-way handshake protocol were proposed.

关 键 词：拒绝服务攻击 形式化 自动化证明 协议状态 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]