信息网络安全

信息网络安全 ›› 2018, Vol. 18 ›› Issue (2): 61-70.doi: 10.3969/j.issn.1671-1122.2018.02.009

• • 上一篇    下一篇

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

易辉凡1,2, 万良1,2(), 黄娜娜1,2, 王鹍鹏1,2   

  1. 1.贵州大学计算机科学与技术学院,贵州贵阳 550025
    2.贵州大学计算机软件与理论研究所,贵州贵阳 550025
  • 收稿日期:2017-11-20 出版日期:2018-02-20 发布日期:2020-05-11
  • 作者简介:

    作者简介：易辉凡（1993—）,男,贵州,硕士研究生,主要研究方向为形式化方法、信息安全;万良（1974—）,男,贵州,教授,博士,主要研究方向为形式化方法、信息安全;黄娜娜（1986—）,女,江苏,硕士研究生,主要研究方向为Web应用安全漏洞、信息安全;王鹍鹏（1991—）,男,河南,硕士研究生,主要研究方向为软件工程。

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

Research on Attacker Modeling Method of Security Protocol Based on SPIN

Huifan YI1,2, Liang WAN1,2(), Nana HUANG1,2, Kunpeng WANG1,2   

  1. 1.College of Computer Science and Technology,Guizhou University, Guiyang Guizhou 550025, China
    2. Computer Software and Theoretical Research Institute, Guizhou University, Guiyang Guizhou 550025, China
  • Received:2017-11-20 Online:2018-02-20 Published:2020-05-11

RichHTML

3

PDF (PC)

402

摘要：

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

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

Abstract:

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 efficient, resulting in lower detection and analysis efficiency 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, efficient and high degree of automation, the model detector SPIN has a powerful detection capability. This paper uses SPIN to study security protocol, proposes a more efficient method to verify the security protocol of attacker model, firstly, 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; finally, the model checker SPIN is used for verification. 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 verification efficiency.

Key words: security protocol, formalized methods, network security, model detection, state space

中图分类号: