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

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

摘要/Abstract

摘要：

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

关键词: 有色Petri网, 安全协议, 形式化分析, 状态空间, 攻击路径

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.

Key words: colored Petri net, security protocol, formal analysis, state space, attack path

中图分类号:

TP393.06

龚翔, 冯涛, 杜谨泽. 基于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.

图/表 17

图1

图2

图3

图4

图5

图6

图7

图8

图9

表1

图10

图11

图12

表2

表3

表4

表5

参考文献 25

[1]	肖美华 . 安全协议形式化分析与验证[M]. 北京: 科学出版社, 2019.
	XIAO M H . Formal analysis and verification of security protocols[M]. Beijing: Science Press, 2019.
[2]	黎波涛, 罗军舟 . 不可否认协议的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.
[3]	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.
[4]	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.
[5]	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.
[6]	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.
[7]	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.
[8]	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.
[9]	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.
[10]	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.
[11]	鲁晔 . 基于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.
[12]	姜筱彦 . 基于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.
[13]	冯涛, 王帅帅, 龚翔 ,等. 工业以太网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.
[14]	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.
[15]	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.
[16]	WANG C L , TAO Y G , ZHOU Y . Protocol verification by simultaneous reachability graph[J]. IEEE Communications Letters, 2017,21(8): 1727-1730.
[17]	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.
[18]	田学成 . 工业控制系统 EtherNet/IP 协议安全性分析[D]. 兰州:兰州理工大学, 2020.
	TIAN X C . Safety analysis of EtherNet/IP protocol of industrial control system[D]. Lanzhou:Lanzhou University of Technology, 2020.
[19]	白云莉 . 基于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.
[20]	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.
[21]	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.
[22]	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.
[23]	DOLEV D , YAO A . On the security of public key protocols[J]. IEEE Transactions on Information Theory, 1983,29(2): 198-208.
[24]	刘秀英, 张玉清, 杨波 ,等. 协议的形式化分析[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.
[25]	赵华伟, 李大兴 . 密钥交换协议的安全性分析[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.

类型	值
状态空间节点数量/个	4 252
有向弧数量/条	5 319
状态	完全
强联通节点数量/个	4 252
强联通弧数量/条	5 319
死节点数量/个	333

安全测试规则	攻击路径数量/条
规则1	6
规则2	6
规则3	6
规则4	7
合计	25

控制方法	节点/个	弧/条	死节点/个
Line-Up引入前	41 501	62 540	4 560
Line-Up引入后	4 252	5 319	333
缩减	91.27%	93.13%	94.93%

方法	协议	节点/个	弧/条	死节点/个
文献[19]方法	TMN	79 722	418 627	8 655
文献[20]方法	TMN	106 962	116 040	未知
本文方法	TMN	4 252	5 319	333

方法	状态空间搜索	状态空间控制	状态空间规模	状态空间完整	提取攻击路径	攻击路径数量	批量搜索状态
文献[7]方法	×	√	可变	×	×	0	×
文献[11]方法	×	√	数万	×	×	1	×
文献[15]方法	×	×	×	×	×	2	×
文献[19]方法	√	√	10万	×	√	5	√
文献[20]方法	√	√	10万	×	√	10	√
文献[22]方法	√	√	数百	×	×	0	×
本文方法	√	√	数千	√	√	25	√