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

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

Abstract

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

CLC Number:

TP393.06

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.

Figures/Tables 17

References 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.

Metrics

Recommended 0

No Suggested Reading articles found!

类型	值
状态空间节点数量/个	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	√

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

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 17

References 25

Related Articles 15

Metrics

Recommended 0

[1]	Jinyin CHEN, Shulong HU, Changyou XING, Guomin ZHANG. Deception defense method against intelligent penetration attack [J]. Journal on Communications, 2022, 43(10): 106-120.
[2]	Wenjuan WANG, Xuehui DU, Dibin SHAN. Construction method of attack scenario in cloud environment based on dynamic probabilistic attack graph [J]. Journal on Communications, 2021, 42(1): 1-17.
[3]	Bo MENG,Xudong HE,Jinli ZHANG,Lili YAO,Jintian LU. Security analysis of security protocol Swift implementations based on computational model [J]. Journal on Communications, 2018, 39(9): 178-190.
[4]	Wen GU,Ji-hong HAN,Lin YUAN. SSMCI:verification mechanism for security protocols centered on the attacker [J]. Journal on Communications, 2017, 38(10): 175-188.
[5]	Shuo WANG,Guang-ming TANG,Guang KOU,Hai-tao SONG. Attack path prediction method based on causal knowledge net [J]. Journal on Communications, 2016, 37(10): 188-198.
[6]	Jing YANG,Dan FAN,Yu-qing ZHANG. Adjusted automata learning algorithm for security protocol adaptive model checking [J]. Journal on Communications, 2015, 36(Z1): 266-276.
[7]	. Towards session identification using principal behavior for multi-party secure protocol [J]. Journal on Communications, 2015, 36(11): 190-200.
[8]	Hai-yan WANG,Si-rui LI. Service substitution method based on composition context [J]. Journal on Communications, 2014, 35(9): 57-66.
[9]	Chun-xiang GU,Huan-xiao WANG,Yong-hui ZHENG,Dan XIN,Nan LIU. SAT-based lazy formal analysis method for security protocols [J]. Journal on Communications, 2014, 35(11): 117-125.
[10]	Zheng-da JIAO,Jian-feng MA,Cong SUN,Qing-song YAO. New remote authorization protocol for vehicle diagnosis [J]. Journal on Communications, 2014, 35(11): 146-153.
[11]	. SAT-based lazy formal analysis method for security protocols [J]. Journal on Communications, 2014, 35(11): 13-116.
[12]	. New remote authorization protocol for vehicle diagnosis [J]. Journal on Communications, 2014, 35(11): 17-154.
[13]	. Analysis and improvement for authentication protocols ofmobile ad hoc network with CSP approach [J]. Journal on Communications, 2013, 34(Z1): 8-66.
[14]	Rong-sen LI,Wen-hua DOU. SIM: a secure IP protocol for MANET [J]. Journal on Communications, 2013, 34(Z1): 116-125.
[15]	Li-cai LIU,Li-hua YIN,Yun-chuan GUO,Yan SUN. Analysis and improvement for authentication protocols of mobile ad hoc network with CSP approach [J]. Journal on Communications, 2013, 34(Z1): 58-66.