通信学报 ›› 2021, Vol. 42 ›› Issue (9): 240-253.doi: 10.11959/j.issn.1000-436x.2021175
• 学术通信 • 上一篇
龚翔, 冯涛, 杜谨泽
修回日期:
2021-04-03
出版日期:
2021-09-25
发布日期:
2021-09-01
作者简介:
龚翔(1986− ),男,上海人,兰州理工大学博士生,主要研究方向为制造业信息化系统与网络安全、工业物联网协议安全的形式化验证等基金资助:
Xiang GONG, Tao FENG, Jinze DU
Revised:
2021-04-03
Online:
2021-09-25
Published:
2021-09-01
Supported by:
摘要:
为了解决有色Petri网(CPN)对安全协议进行形式化建模分析时,仅能判断协议是否存在漏洞而无法找出漏洞具体位置和攻击路径的问题,以及 CPN 建模时随着攻击者模型引入,安全协议的形式化模型可能的消息路径数量激增,状态空间容易发生爆炸导致难以提取准确攻击路径的问题,改进了基于 CPN 的安全协议形式化建模方法,验证并提取攻击路径的同时,采用更细粒度的协议建模及控制。在状态空间收敛方面提出了 CPN 模型不同进程在各分层模型中等待-同步的方法控制状态空间规模。通过针对TMN协议的安全评估分析,成功提取出该协议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.
[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. |
[1] | 陈晋音, 胡书隆, 邢长友, 张国敏. 面向智能渗透攻击的欺骗防御方法[J]. 通信学报, 2022, 43(10): 106-120. |
[2] | 王文娟, 杜学绘, 单棣斌. 基于动态概率攻击图的云环境攻击场景构建方法[J]. 通信学报, 2021, 42(1): 1-17. |
[3] | 朱辉,武衡,赵海强,赵玉清,李晖. 适用于双层卫星网络的星间组网认证方案[J]. 通信学报, 2019, 40(3): 1-9. |
[4] | 庄陵,马靖怡,王光宇,关鹃. FIR数字滤波器零极点灵敏度分析及优化实现[J]. 通信学报, 2018, 39(9): 168-177. |
[5] | 孟博,何旭东,张金丽,尧利利,鲁金钿. 基于计算模型的安全协议Swift语言实施安全性分析[J]. 通信学报, 2018, 39(9): 178-190. |
[6] | 余盼,李斌,赵成林. 基于能量检测的异步感知算法[J]. 通信学报, 2017, 38(3): 165-173. |
[7] | 谷文,韩继红,袁霖. SSMCI:以攻击者为中心的安全协议验证机制[J]. 通信学报, 2017, 38(10): 175-188. |
[8] | 王硕,汤光明,寇广,宋海涛. 基于因果知识网络的攻击路径预测方法[J]. 通信学报, 2016, 37(10): 188-198. |
[9] | 杨京,范丹,张玉清. 改进的安全协议自适应分析算法[J]. 通信学报, 2015, 36(Z1): 266-276. |
[10] | 李永凯,刘树波,杨召唤,刘梦君. 机会网络中用户属性隐私安全的高效协作者资料匹配协议[J]. 通信学报, 2015, 36(12): 163-171. |
[11] | 朱玉娜,韩继红,袁 霖,陈韩托,范钰丹. 基于主体行为的多方安全协议会话识别方法[J]. 通信学报, 2015, 36(11): 190-200. |
[12] | 孙梦巍,赵龙,许巧春,李斌,赵成林. 动态时变衰落信道下的频谱感知算法[J]. 通信学报, 2014, 35(7): 63-69. |
[13] | 孙梦巍,赵 龙,许巧春,李 斌,赵成林. 一种动态时变衰落信道下的频谱感知算法[J]. 通信学报, 2014, 35(7): 8-69. |
[14] | 顾纯祥,王焕孝,郑永辉,辛丹,刘楠. 基于SAT的安全协议惰性形式化分析方法[J]. 通信学报, 2014, 35(11): 117-125. |
[15] | 焦政达,马建峰,孙聪,姚青松. 新的车辆远程诊断授权协议[J]. 通信学报, 2014, 35(11): 146-153. |
阅读次数 | ||||||
全文 |
|
|||||
摘要 |
|
|||||
|