基于CPN的安全协议形式化建模及安全分析方法

龚翔; 冯涛; 杜谨泽

doi:10.11959/j.issn.1000-436x.2021175

您当前的位置：

首页 >

文章列表页 >

基于CPN的安全协议形式化建模及安全分析方法

学术通信 | 更新时间：2024-06-05

- 基于CPN的安全协议形式化建模及安全分析方法
- Formal modeling and security analysis method of security protocol based on CPN
- 通信学报 2021年42卷第9期页码：240-253
- 作者机构：
  
  兰州理工大学计算机与通信学院，甘肃兰州 730050
- 作者简介：
  
  [ "龚翔（1986− ），男，上海人，兰州理工大学博士生，主要研究方向为制造业信息化系统与网络安全、工业物联网协议安全的形式化验证等" ]
  [ "冯涛（1970− ），男，甘肃临洮人，博士，兰州理工大学研究员、博士生导师，主要研究方向为网络与信息安全、区块链和工业互联网等" ]
  [ "杜谨泽（1986− ），男，甘肃会宁人，博士，兰州理工大学讲师，主要研究方向为无线传感器网络、工业物联网、室内定位、网络安全等" ]
- 基金信息：
  
  国家自然科学基金资助项目(62162039);国家自然科学基金资助项目(61762060);甘肃省高等学校科研基金资助项目(2017C-05);甘肃省科技厅重点研发计划基金资助项目(20YF3GA016)
- DOI：10.11959/j.issn.1000-436x.2021175
  中图分类号： TP393.06
- 网络出版日期：2021-09，
  
  纸质出版日期：2021-09-25
- 稿件说明：
移动端阅览
龚翔, 冯涛, 杜谨泽. 基于CPN的安全协议形式化建模及安全分析方法[J]. 通信学报, 2021,42(9):240-253.

Xiang GONG, Tao FENG, Jinze DU. Formal modeling and security analysis method of security protocol based on CPN[J]. Journal on communications, 2021, 42(9): 240-253.
龚翔, 冯涛, 杜谨泽. 基于CPN的安全协议形式化建模及安全分析方法[J]. 通信学报, 2021,42(9):240-253. DOI： 10.11959/j.issn.1000-436x.2021175.

Xiang GONG, Tao FENG, Jinze DU. Formal modeling and security analysis method of security protocol based on CPN[J]. Journal on communications, 2021, 42(9): 240-253. DOI： 10.11959/j.issn.1000-436x.2021175.

摘要

为了解决有色Petri网（CPN）对安全协议进行形式化建模分析时，仅能判断协议是否存在漏洞而无法找出漏洞具体位置和攻击路径的问题，以及 CPN 建模时随着攻击者模型引入，安全协议的形式化模型可能的消息路径数量激增，状态空间容易发生爆炸导致难以提取准确攻击路径的问题，改进了基于 CPN 的安全协议形式化建模方法，验证并提取攻击路径的同时，采用更细粒度的协议建模及控制。在状态空间收敛方面提出了 CPN 模型不同进程在各分层模型中等待-同步的方法控制状态空间规模。通过针对TMN协议的安全评估分析，成功提取出该协议25条攻击路径，评估了该协议安全性的同时证明了所述方法的有效性。

Abstract

To solve the problem of modeling and analyzing with colored Petri net (CPN)

which was determining vulnerabilities in hole location but couldn’t identify any attack path

and the problem of when the introduction of the attacker model

the number of possible message paths in the CPN formal model of security protocol surges the state space prone to explosion

which made it difficult to extract accurate attack paths

the formal modeling method of security protocol was improved base on CPN

the attack paths were verified and extracted

further the fine-grained protocol modeling and control were adopted.As well as in the aspect of state-space convergence

and a waiting-sync method for different processes of CPN model in each hierarchy model was proposed

which effectively controlled the state-space scale of the model.Through the security evaluation and analysis of TMN protocol

25 attack paths of the protocol are extracted successfully

the security of the protocol is evaluated

and the effectiveness of the proposed method is proved.

关键词

Keywords

references

肖美华 . 安全协议形式化分析与验证 [M ] . 北京 : 科学出版社 , 2019 .

XIAO M H . Formal analysis and verification of security protocols [M ] . Beijing : Science Press , 2019 .

黎波涛 , 罗军舟 . 不可否认协议的Petri网建模与分析 [J ] . 计算机研究与发展 , 2005 , 42 ( 9 ): 1571 - 1577 .

LI B T , LUO J Z . Modeling and analysis of non-repudiation protocols by using petri nets [J ] . Journal of Computer Research and Development , 2005 , 42 ( 9 ): 1571 - 1577 .

XU Y , XIE X , ZHANG H . Modeling and analysis of security protocols using colored petri nets [J ] . Journal of Software , 2011 , 6 ( 7 ): 19 - 27 .

NORTA A , MATULEVICIUS R , LEIDING B . Safeguarding a formalized blockchain-enabled identity-authentication protocol by applying security risk-oriented patterns [J ] . Computers ＆ Security , 2019 , 86 ( 9 ): 253 - 269 .

COHN G K , CREMERS C , DOWLING B , et al . A formal security analysis of the signal messaging protocol [J ] . Journal of Cryptology , 2020 , 33 ( 4 ): 1914 - 1983 .

WANG D , HUANG X , MA X F . Formal analysis of smart contract based on colored petri nets [J ] . IEEE Intelligent Systems , 2020 , 35 ( 3 ): 19 - 30 .

RODRÍGUEZ A , KRISTENSEN L M , RUTLE A . Formal modelling and incremental verification of the MQTT IoT protocol [J ] . Transactions on Petri Nets and Other Models of Concurrency , 2019 , 11 ( XIV ): 126 - 145 .

BECHAR R , TAHAR A M , MEZOUDJ F , et al . On formal modeling and validation of wireless sensor network protocols [J ] . Wireless Personal Communications , 2020 , 114 ( 4 ): 2855 - 2888 .

MACHADO P , SILVA M R , SOUZA L E , et al . Modeling using colored petri net of communication networks based on IEC 61850 in a microgrid context [J ] . Journal of Control,Automation and Electrical Systems , 2018 , 29 ( 6 ): 703 - 717 .

ANSAROUDI Z E , PASHAZADEH S . Modeling and formal verification of the ticket-based handoff authentication protocol for wireless mesh networks [C ] // 2019 International Symposium on Pervasive Systems,Algorithms and Networks . Berlin:Springer , 2019 : 140 - 154 .

鲁晔 . 基于HCPN模型检测方法的DNP3-SA协议形式化安全评估与改进 [D ] . 兰州:兰州理工大学 , 2018 .

LU Y . Formal security assessment and improvement of DNP3-SA protocol based on HCPN model detection [D ] . Lanzhou:Lanzhou University of Technology , 2018 .

姜筱彦 . 基于HCPN模型检测方法的BACnet协议形式化安全评估与改进 [D ] . 兰州:兰州理工大学 , 2020 .

JIANG X Y . Formal security evaluation and improvement of BACnet protocol based on HCPN model detection method [D ] . Lanzhou:Lanzhou University of Technology , 2020 .

冯涛 , 王帅帅 , 龚翔 , 等 . 工业以太网EtherCAT协议形式化安全评估及改进 [J ] . 计算机研究与发展 , 2020 , 57 ( 11 ): 2312 - 2327 .

FENG T , WANG S S , GONG X , et al . Formal security evaluation and improvement of industrial Ethernet EtherCAT protocol [J ] . Journal of Computer Research and Development , 2020 , 57 ( 11 ): 2312 - 2327 .

FAN Y T , SU G P , HE L , et al . Study on a CPN-based auto-analysis tool for security protocols [C ] // 2012 Fourth International Symposium on Information Science and Engineering . Piscataway:IEEE Press , 2012 : 179 - 182 .

IGOREVICH R R , SHIN D , MIN D . CPN Based analysis of in-vehicle secure communication protocol [C ] // 2016 International Conference on Heterogeneous Networking for Quality,Reliability,Security and Robustness . Berlin:Springer , 2016 : 12 - 21 .

WANG C L , TAO Y G , ZHOU Y . Protocol verification by simultaneous reachability graph [J ] . IEEE Communications Letters , 2017 , 21 ( 8 ): 1727 - 1730 .

AMOAH R , CAMTEPE S , FOO E . Formal modelling and analysis of DNP3 secure authentication [J ] . Journal of Network and Computer Applications , 2016 , 59 : 345 - 360 .

田学成 . 工业控制系统 EtherNet/IP 协议安全性分析 [D ] . 兰州:兰州理工大学 , 2020 .

TIAN X C . Safety analysis of EtherNet/IP protocol of industrial control system [D ] . Lanzhou:Lanzhou University of Technology , 2020 .

白云莉 . 基于CP-nets模型的安全协议形式化方法研究 [D ] . 呼和浩特:内蒙古大学 , 2013 .

BAI Y L . Research on security protocol formal method based on colored petri nets model [D ] . Hohhot:Inner Mongolia University , 2013 .

PERMPOONTANALARP Y , SORNKHOM P . On-the-fly trace generation approach to the security analysis of cryptographic protocols:coloured petri nets-based method [J ] . Fundamenta Informaticae , 2014 , 130 ( 4 ): 423 - 466 .

SUN T , ZHANG W , GUO X , et al . Research on CPN model reduction focus on parallel tested behaviors [C ] // 2017 IEEE International Symposium on Parallel and Distributed Processing with Applications and 2017 IEEE International Conference on Ubiquitous Computing and Communications . Piscataway:IEEE Press , 2017 : 827 - 833 .

DRESP W , . Security analysis of the secure authentication protocol by means of coloured petri nets [C ] // 2005 IFIP International Conference on Communications and Multimedia Security . Berlin:Springer , 2005 : 230 - 239 .

DOLEV D , YAO A . On the security of public key protocols [J ] . IEEE Transactions on Information Theory , 1983 , 29 ( 2 ): 198 - 208 .

刘秀英 , 张玉清 , 杨波 , 等 . 协议的形式化分析 [J ] . 西安电子科技大学学报自然科学版 , 2004 , 31 ( 5 ): 785 - 790 .

LIU X Y , ZHANG Y Q , YANG B , et al . An approach to the formal analysis of the TMN protocol [J ] . Journal of Xidian University-Natural Science , 2004 , 31 ( 5 ): 785 - 790 .

赵华伟 , 李大兴 . 密钥交换协议的安全性分析 [J ] . 山东大学学报(理学版) , 2006 , 41 ( 4 ): 101 - 106 .

ZHAO H W , LI D X . Key-exchange protocols' security analysis [J ] . Journal of Shandong University (Natural Science) , 2006 , 41 ( 4 ): 101 - 106 .

浏览量

232

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于CPN的车载网络无证书匿名认证和密钥协商方案研究

基于计算模型的安全协议Swift语言实施安全性分析

基于身份认证的BACnet/IP分析与改进

室内定位隐私保护综述

面向智能渗透攻击的欺骗防御方法