安全协议抗DoS攻击的形式化分析研究  

A formal analysis for security protocol against DoS attacks

作　　者：高强 林星辰 林宏刚[2] 金大鹏[2] GAO Qiang;LIN Xing-Chen;LIN Hong-Gang;JIN Da-Peng(National Computer Network Emergency Response Technical Team/Coordination Center of China,Beijing 100029,China;College of Information Security Engineering,Chengdu University of Information Technology,Chengdu 610225,China)

机构地区：[1]国家计算机网络应急技术处理协调中心,北京100029 [2]成都信息工程大学信息安全工程学院,成都610225

出　　处：《四川大学学报（自然科学版）》2018年第6期1211-1218,共8页Journal of Sichuan University(Natural Science Edition)

基　　金：四川省科技厅重点研发项目(2017GZ0319)

摘　　要：随着拒绝服务攻击给协议的可用性带来的危害越来越大,需要行之有效的方法对安全协议的抗DoS性进行分析.但是目前对安全协议的抗DoS性进行分析的方法模型都存在一些缺陷,有的只能分析部分的DoS攻击,有的只关注协议各方计算资源的消耗,而忽略了存储资源消耗.针对以上不足,本文对基本的串空间模型进行扩展,引入消息相关度集合和代价函数,提出了一种分析安全协议抗DoS性的新方法,并利用该方法,对JFK协议的抗DoS性进行了详细分析.As DoS attacks lead to an increasing risk to the availability of protocol, Some effective methods are required to analyze the anti-DoS performance of security protocols. However, the current proposed methods for analyzing the anti-DoS performance of security protocols have some shortcomings, some can only analyze a part of DoS attacks, and some only focus on the agreement of computing resources consumption, while ignoring the consumption of storage resources. In view of the above deficiencies, this paper extends the strand space model with introducing the message correlation set and the cost function, and proposes a new method to analyze the anti-DoS performance of the security protocol. Detailed anti-DoS performance analysis is presented for the JFK protocol by the new proposed method in the paper.

关 键 词：安全协议 拒绝服务攻击 扩展串空间模型 

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