基于连续ARQ协议的隐蔽洪水攻击

A Covert Flooding Attack Based on Successive ARQ Protocol

通信协议设计时的疏漏很容易造成严重的后果,因此有必要采用形式化的方法来保证协议的安全性和可靠性。模型检测是一种具有工业应用前景的形式化分析方法,并具有很高的自动化程度,适合于协议的分析与验证。文中采用模型检测工具SPIN对连续ARQ协议建模,通过验证该协议的基本属性证明所建模型的正确性。然后依据Dolev和Yao的思想加入攻击者模型再进行分析,发现了连续ARQ协议的一个新漏洞,攻击者能够利用这个漏洞造成大量冗余数据的传输和存储。这种攻击建立在互信的数据传输基础上,且攻击者并不直接发送冗余数据,因此具有很高的隐蔽性。

The careless omission of the design of communication protocol can easily lead to serious consequence. So it is necessary to use formal method to ensure the security and reliability of the protocol, Model checking is a formal method which has wide industrial applica- lion prospect aod high level of automation. It is suitable for the analysis and verification of the protocol. It uses SPIN model cheek tech-nology to model the successive ARQ protocol and verifies its basic attributes. And then it adds the attacker model which is proposed by Dolev and Yao. This work finds a new loophole of successive ARQ protocol. Attacker can use this loophole to cause the transmission and store of a large number of redundant data. This attack based on the mutual-trust data transmission, and the attacker don＇t send redundant data directly. Such attacks have good concealment.