Formal modeling and security analysis method of security protocol based on CPN

Xiang GONG; Tao FENG; Jinze DU

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

您当前的位置：

首页 >

文章列表页 >

Formal modeling and security analysis method of security protocol based on CPN

Correspondences | 更新时间：2024-06-05

- Formal modeling and security analysis method of security protocol based on CPN
- Journal on Communications Vol. 42, Issue 9, Pages: 240-253(2021)
- 作者机构：
  
  兰州理工大学计算机与通信学院，甘肃兰州 730050
- 作者简介：
- 基金信息：
  
  The National Natural Science Foundation of China(62162039);The National Natural Science Foundation of China(61762060);Educational Commission of Gansu Province(2017C-05);The Key Research and De-velopment Program of Gansu Province(20YF3GA016)
- DOI：10.11959/j.issn.1000-436x.2021175
  CLC： TP393.06
- Online First：2021-09，
  
  Published：25 September 2021
- 稿件说明：
移动端阅览
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：

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 .

Views

1310

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Research on certificateless anonymous authentication and key agreement scheme of vehicle network based on CPN

Security analysis of security protocol Swift implementations based on computational model

Analysis and improvement of the BACnet/IP based on identity authentication

Survey on privacy protection indoor positioning

Deception defense method against intelligent penetration attack

Related Author

SU Chunhua

FENG Tao

ZHENG Lu

Bo MENG

Xudong HE

Jinli ZHANG

Lili YAO

Jintian LU

Related Institution

Division of Computer Science, University of Aizu

College of Computer Science,South Central University For Nationalities

School of Mechanical and Electrical Engineering, Lanzhou University of Technology

School of Computer and Communications, Lanzhou University of Technology

State Key Laboratory of Information Engineering in Surveying Mapping and Remote Sensing, Wuhan University

AI问答

⁰