Towards formal verification of IoT protocols: A Review

被引:58
作者
Hofer-Schmitz, Katharina [1 ]
Stojanovic, Branka [1 ]
机构
[1] JOANNEUM RES Forsch Gesell MbH, DIGITAL Inst Informat & Commun Technol, 17 Steyrergasse, Graz, Austria
基金
欧盟地平线“2020”;
关键词
Formal verification; Security; Protocols; Model checkers; IoT; SECURITY PROTOCOLS; AUTHENTICATION; IMPLEMENTATION; FRAMEWORK; INTERNET; DESIGN; LTE;
D O I
10.1016/j.comnet.2020.107233
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
Formal Verification is one of the crucial methods to detect possible weaknesses and vulnerabilities at an early stage. This paper reviews formal methods for an extensive variety of protocols used in the IoT environment. It gives detailed descriptions of the considered properties and the applied methods. An in-depth literature review shows that four application fields can be distinguished, namely: (1) functional checks, (2) checks on security properties, (3) suggestions for enhanced schemes including a priori security property checks and (4) implementation checks of protocols. This paper further offers a comprehensive overview of the covered security properties and of commonly used tools for protocols in the field. Additionally, an extensive description and overview of commonly used model checkers is given and open issues and challenges in the IoT field are addressed.
引用
收藏
页数:21
相关论文
共 100 条
[91]  
Radomirovic S., 2010, P 1 INT WORKSH SEC I, P6
[92]  
Rashid A, 2015, 2015 12TH INTERNATIONAL CONFERENCE ON HIGH-CAPACITY OPTICAL NETWORKS AND ENABLING/EMERGING TECHNOLOGIES (HONET), P80
[93]   On Secure Simple Pairing in Bluetooth Standard v5.0-Part I: Authenticated Link Key Security and Its Home Automation and Entertainment Applications [J].
Sun, Da-Zhi ;
Sun, Li .
SENSORS, 2019, 19 (05)
[94]  
Tomasin S, 2017, IEEE WIREL COMMUNN
[95]   Automated Security Protocol Analysis With the AVISPA Tool [J].
Vigano, Luca .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 155 :61-86
[96]  
Whitman M. E., 2011, Principles of Information security
[97]   Security Vulnerabilities in LoRaWAN [J].
Yang, Xueying ;
Karampatzakis, Evgenios ;
Doerr, Christian ;
Kuipers, Fernando .
2018 IEEE/ACM THIRD INTERNATIONAL CONFERENCE ON INTERNET-OF-THINGS DESIGN AND IMPLEMENTATION (IOTDI 2020), 2018, :129-140
[98]   An Enhanced LoRaWAN Security Protocol for Privacy Preservation in IoT with a Case Study on a Smart Factory-Enabled Parking System [J].
You, Ilsun ;
Kwon, Soonhyun ;
Choudhary, Gaurav ;
Sharma, Vishal ;
Seo, Jung Taek .
SENSORS, 2018, 18 (06)
[99]  
Younes H. L. S., 2002, Computer Aided Verification. 14th International Conference, CAV 2002. Proceedings (Lecture Notes in Computer Science Vol.2404), P223
[100]   Formal Analysis of 5G EAP-TLS Authentication Protocol Using Proverif [J].
Zhang, Jingjing ;
Yang, Lin ;
Cao, Weipeng ;
Wang, Qiang .
IEEE ACCESS, 2020, 8 :23674-23688