一种基于SPIN的安全协议形式化验证方法

摘要

基于形式化的验证方法是提高软件系统质量以及保证安全攸关系统安全性和可靠性的有效方法。本文提出了一种基于SPIN的模型检测方法，该方法通过DoIev—Yao模型来描述协议系统及攻击者，通过LTL公式对待验证属性进行形式化规约。通过运用这种验证方法以及模型检测器SPIN找到了一种不满足待验证属性的情况即找到了一种针对协议的攻击，说明了这种方法的在实际中可以有效的发现协议的缺陷，而且可方便地用于其它网络安全协议验证。