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

摘要：

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

关键词：连续ARQ协议、洪水攻击、模型检测、SPIN、Promela

分类号：TP393.04(计算技术、计算机技术)

在线出版日期：2012-11-06（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：177-180