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