基于SPIN的安全协议的攻击者建模方法研究

摘要：

安全协议是确保网络安全的关键,在现有的技术条件下,已经有许多方法来分析协议的安全性,但是对攻击者建模的方法不够高效,导致协议的检测和分析效率较低.形式化方法是检验协议安全性的一种手段,它能高效地分析验证协议设计中存在的漏洞.模型检测作为形式化方法的一种,具有简洁、高效和自动化程度高的特性,模型检测器SPIN具有强大的检测能力.文章使用SPIN对安全协议进行研究,提出了一种更有效的方法来验证攻击者模型的安全协议,首先对攻击者行为进行分析,获取攻击者初始知识库,根据分解规则和合成规则不断地更新攻击者知识库;其次形式化分析各诚实主体,并建立各诚实主体和攻击者的Promela语义模型;最后使用模型检测器SPIN进行验证.实验结果表明,文章提出的方法能使模型复杂度降低,大幅度减少模型的状态数量,有效地避免状态空间爆炸,提升验证效率.

关键词：安全协议、形式化方法、网络安全、模型检测、状态空间

分类号：TP309(计算技术、计算机技术)

资助基金：贵州省科学基金[黔科合J字[2011]2328号,黔科合LH字2014]7634号

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

页数：共10页

页码：61-70