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

A formal analysis for security protocol against DoS attacks

摘要:

随着拒绝服务（Denial of Service，DoS）攻击给协议的可用性带来的危害越来越大，需要行之有效的方法对安全协议的抗DoS性进行分析。但是目前对安全协议的抗DoS性进行分析的方法模型都存在一些缺陷，有的只能分析部分的DoS攻击，有的只关注协议各方计算资源的消耗，而忽略了存储资源消耗。针对以上不足，本文对基本的串空间模型进行扩展，引入消息相关度集合和代价函数，提出了一种分析安全协议抗DoS性的新方法，并利用该方法，对JFK协议的抗DoS性进行了详细分析。新的方法不仅分析了协议抗资源消耗型DoS攻击的能力，而且分析了抗服务中止型DoS攻击的能力，更加的准确与全面。

Abstract:

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.