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

Research on Attacker Modeling Method of Security Protocol Based on SPIN

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

Security protocol is the key to ensure network security, in the existing technical conditions, there are many methods to analyze the security of protocol, but the attacker modeling method is not effcient, resulting in lower detection and analysis effciency of protocols. Formal method is a means to verify protocol, which can effectively analyze the loopholes in the design of verification protocol. As one of the formalized methods, model detection has the characteristics of simplicity, effcient and high degree of automation, the model detector SPIN has a powerful detection capability. This paper uses SPIN to studysecurity protocol, proposes a more effcient method to verify the security protocol of attacker model, frstly, analyze the attacker＇s behavior, acquire the attacker＇s initial knowledge base, update the attacker＇s knowledge base according to the decomposition rule and the synthetic rule; secondly, formalize the Promela semantic model of each honest subject and the attacker; fnally, the model checker SPIN is used for verifcation. The experimental results show that the proposed method can reduce the complexity of the model, greatly reduce the number of state of the model, effectively avoid the state space explosion, and improves the verifcation effciency.