Formal modeling and analysis of security schemes of RPL protocol using colored Petri nets

被引：0

作者：

Ahmad, Farooq ^{[1
]}

Chaudhry, Muhammad Tayyab ^{[1
]}

Jamal, Muhammad Hasan ^{[1
]}

Sohail, Muhammad Amar ^{[1
]}

Gavilanes, Daniel ^{[1
,2
,4
,5
]}

Masias Vergara, Manuel ^{[2
,3
,6
]}

Ashraf, Imran ^{[1
,7
]}

机构：

[1] COMSATS Univ Islamabad, Dept Comp Sci, Lahore Campus, Lahore, Pakistan

[2] Univ Europea Atlantico, Santander, Spain

[3] Univ Int Iberoamer, Campeche, Mexico

[4] Univ Int Iberoamer, Arecibo, PR USA

[5] Univ Int Cuanza, Cuito, Bie, Angola

[6] Fdn Univ Int Colombia, Bogota, Colombia

[7] Yeungnam Univ, Dept Informat & Commun Engn, Gyongsan, South Korea

来源：

PLOS ONE | 2023年 / 18卷 / 08期

关键词：

THINGS IOT; INTERNET; VERIFICATION; MITIGATION;

D O I：

10.1371/journal.pone.0285700

中图分类号：

O [数理科学和化学]; P [天文学、地球科学]; Q [生物科学]; N [自然科学总论];

学科分类号：

07 ; 0710 ; 09 ;

摘要：

In the Internet of things (IoT), data packets are accumulated and disseminated across IoT devices without human intervention, therefore the privacy and security of sensitive data during transmission are crucial. For this purpose, multiple routing techniques exist to ensure security and privacy in IoT Systems. One such technique is the routing protocol for low power and lossy networks (RPL) which is an IPv6 protocol commonly used for routing in IoT systems. Formal modeling of an IoT system can validate the reliability, accuracy, and consistency of the system. This paper presents the formal modeling of RPL protocol and the analysis of its security schemes using colored Petri nets that applies formal validation and verification for both the secure and non-secure modes of RPL protocol. The proposed approach can also be useful for formal modeling-based verification of the security of the other communication protocols.

引用

页数：23

共 50 条

[1] Formal Modeling and Analysis of SIP Using Colored Petri Nets
Bai, Yunli
Ye, Xinming
Ma, Yuanfei
[J]. 2011 7TH INTERNATIONAL CONFERENCE ON WIRELESS COMMUNICATIONS, NETWORKING AND MOBILE COMPUTING (WICOM), 2011,
[2] Modeling and Analysis of Security Protocols Using Colored Petri Nets
Xu, Yang
Xie, Xiaoyao
[J]. JOURNAL OF COMPUTERS, 2011, 6 (01) : 19 - 27
[3] Considering Time in Formal Analysis of Security Protocols Using Colored Petri Nets
Xu, Meng
Su, Guiping
Ding, Yanlan
[J]. 2008 INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE AND SYSTEMS SYMPOSIA, PROCEEDINGS, 2008, : 63 - 68
[4] Formal Analysis of FPH Contract Signing Protocol Using Colored Petri Nets
Payeras-Capella, Magdalena
Mut-Puigserver, Macia
Isern-Deya, Andreu Pere
Ferrer-Gomila, Josep L.
Huguet-Rotger, Llorenc
[J]. SECURITY AND PRIVACY IN COMMUNICATION NETWORKS, 2009, 19 : 101 - 120
[5] Modeling and Security Analysis of IEEE 802.1AS Using Hierarchical Colored Petri Nets
Tang, Siyu
Hu, Xiaoya
Zhao, Lian
[J]. 2020 IEEE GLOBAL COMMUNICATIONS CONFERENCE (GLOBECOM), 2020,
[6] Analysis of Concurrent Security Protocols Using Colored Petri Nets
Long, Shigong
[J]. 2009 INTERNATIONAL CONFERENCE ON NETWORKING AND DIGITAL SOCIETY, VOL 1, PROCEEDINGS, 2009, : 227 - 230
[7] Modeling and analysis of reliable Contract Net Protocol Using Timed Colored Petri Nets
Boukredera, Djamila
Maamri, Ramdane
Aknine, Samir
[J]. 2013 IEEE/WIC/ACM INTERNATIONAL CONFERENCE ON INTELLIGENT AGENT TECHNOLOGY (IAT 2013), 2013, : 17 - 24
[8] Modeling and Analysis of Inventory System by Using Colored Petri Nets
Lu, Xiaochun
Liu, Dongyuan
Ni, Zhiwei
[J]. IEEE/SOLI'2008: PROCEEDINGS OF 2008 IEEE INTERNATIONAL CONFERENCE ON SERVICE OPERATIONS AND LOGISTICS, AND INFORMATICS, VOLS 1 AND 2, 2008, : 1359 - 1364
[9] Modeling and Analysis of the 1-Wire Communication Protocol Using Timed Colored Petri Nets
Emilia Cambronero, Maria
Macia, Hermenegilda
Valero, Valentin
Orozco Barbosa, Luis
[J]. IEEE ACCESS, 2018, 6 : 27356 - 27372
[10] Modeling system integrity of a security critical system using Colored Petri Nets
Houmb, SH
Salhammar, K
[J]. Safety and Security Engineering, 2005, 82 : 3 - 12

← 1 2 3 4 5 →