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

摘要

针对形式化方法对安全协议DoS攻击分析的不足之处,提出了一种基于串空间模型的扩展形式化方法.利用扩展后的形式化方法.对IEEE802.11i四步握手协议进行了DoS攻击分析,发现其的确存在DoS攻击漏洞.通过分析,提出一种可以改善DoS攻击的方法,并通过了扩展形式化方法对于判断安全协议DoS攻击分析的测试规则.最后,根据扩展形式化方法对改进后的四步握手协议进行证明,得出改进后协议可以通过两类DoS测试规则运行至结束.