No Access

Modeling and Verification of IEEE 802.11i Security Protocol in UPPAAL for Internet of Things

Yuteng Lu

LMAM, School of Mathematical Sciences, Peking University, Beijing 100871, P. R. China

Department of Informatics, School of Mathematical Sciences, Peking University, Beijing 100871, P. R. China

E-mail Address: luyuteng@pku.edu.cn

Search for more papers by this author

and

Meng Sun

LMAM, School of Mathematical Sciences, Peking University, Beijing 100871, P. R. China

Department of Informatics, School of Mathematical Sciences, Peking University, Beijing 100871, P. R. China

E-mail Address: sunm@pku.edu.cn

Corresponding author.

Search for more papers by this author

https://doi.org/10.1142/S021819401840020XCited by:9 (Source: Crossref)

This article is part of the issue:

Special Issue — Best Papers from SEKE 2018; Guest Editors: S.-K. Chang, O. M. Pereira and A. Perkusich

Abstract

IEEE 802.11i is the IEEE standard that provides enhanced MAC security and has been widely used in wireless networks and Internet of Things. It improves IEEE 802.11 (1999) by providing a Robust Security Network (RSN) with two new protocols: the Four-Way Handshake and the Group Key Handshake. These protocols utilize the authentication services and port access control described in IEEE 802.1X to establish and change the appropriate cryptographic keys. In this paper, we carry out a formal modeling and verification approach based on timed automata for IEEE 802.11i protocol, using the UPPAAL model checker, to check correctness of the changes in IEEE 802.11i protocol and provide better security.

Keywords:

References

1. A. Alabdulatif, X. Ma and L. Nolle, Analysing and attacking the 4-Way Handshake of IEEE 802.11i Standard, in Proc. 8th Int. Conf. Internet Technology and Secured Transactions, 2013, pp. 382–387. Google Scholar
2. R. Alur and D. L. Dill, A theory of timed automata, Theor. Comput. Sci. 126 (2) (1994) 183–235. Crossref, Web of Science, Google Scholar
3. C. Baier and J.-P. Katoen, Principles of Model Checking (MIT Press, 2008). Google Scholar
4. G. Behrmann, A. David and K. G. Larsen, A tutorial on UPPAAL, in SFM-RT Formal Methods for the Design of Real-Time Systems, 2004, pp. 200–236. Crossref, Google Scholar
5. P. R. D’Argenio, J. Katoen, T. C. Ruys and J. Tretmans, The bounded retransmission protocol must be on time!, in Proc. Int. Workshop Tools and Algorithms for the Construction and Analysis of Systems, 1997, pp. 416–431. Google Scholar
6. S. Dustdar, S. Nastic and O. Scekic, Smart Cities: The Internet of Things, People and Systems (Springer, 2017). Crossref, Google Scholar
7. K. Havelund, A. Skou, K. G. Larsen and K. Lund, Formal modeling and analysis of an audio/video protocol: An industrial case study using UPPAAL, in Proc. 18th IEEE Real-Time Systems Symp., 1997, pp. 2–13. Google Scholar
8. C. He, M. Sundararajan, A. Datta, A. Derek and J. C. Mitchell, A modular correctness proof of IEEE 802.11i and TLS, in Proc. 12th ACM Conf. Computer and Communications Security, 2005, pp. 2–15. Google Scholar
9. IEEE Standards Association, IEEE Std 802-2014: IEEE Standard for Local and Metropolitan Area Networks: Overview and Architecture (2014), https://standards.ieee.org/standard/802-2014.html. Google Scholar
10. IEEE Standards Association, IEEE Std 802.1X-2010: IEEE Standard for Local and metropolitan area networks — Port-Based Network Access Control (2010), https://standards.ieee.org/standard/802_IX-2010.html. Google Scholar
11. J. H. Kim, K. G. Larsen, B. Nielsen, M. Mikučionis and P. Olsen, Formal analysis and testing of real-time automotive systems using UPPAAL tools, in FMICS 2015: Formal Methods for Industrial Critical Systems, 2015, pp. 47–61. Crossref, Google Scholar
12. K. G. Larsen, P. Pettersson and W. Yi, Diagnostic model-checking for real-time systems, in Proc. 4th DIMACS Workshop Verification and Control of Hybrid Systems, LNCS Vol. 1066 (Springer, 1996), pp. 575–586. Google Scholar
13. J. Liu, X. Ye, J. Zhang and J. Li, Security verification of 802.11i 4-Way Handshake protocol, in Proc. Int. Conf. Commun., 2008, pp. 1642–1647. Google Scholar
14. X. Liu and A. O. Fapojuwo, Formal evaluation of major authentication methods for IEEE 802.11i WLAN standard, in Proc.Vehicular Technology Conf., 2006, pp. 1–5. Google Scholar
15. S. P. Hong and J. Lee, Supporting secure authentication and privacy in wireless computing, in Proc. Int. Conf. Hybrid Information Technology, 2006, pp. 594–599. Google Scholar
16. K. V. K. Raju, V. Vallikumari and K. Raju, Modeling and analysis of IEEE802.11i WPA-PSK authentication protocol, in Proc. 3rd Int. Conf. Electronics Computer Technology, 2011, pp. 72–76. Google Scholar
17. S. Saini and A. Fehnker, Evaluating the stream control transmission protocol using UPPAAL, arXiv:1703.06568 [cs. LO]. Google Scholar
18. L. Shuxin and N. Yoshiura, Model checking of TTCAN protocol using UPPAAL, in ICCSA 2018: Computational Science and Its Applications, LNCS Vol. 10963 (Springer, 2018), pp. 550–564. Crossref, Google Scholar
19. P. Singh, M. Mishra and P. N. Barwal, Analysis of security issues and their solutions in wireless LAN, in Int. Conf. Information Communication and Embedded Systems, 2014, pp. 1–6. Google Scholar
20. R. Singh and T. P. Sharma, A key refreshing technique to reduce 4-Way Handshake latency in 802.11i based networks, in Proc. 4th Int. Conf. Computer and Communication Technology, 2013, pp. 157–162. Google Scholar
21. E. Sithirasenan, S. Zafar and V. Muthukkumarasamy, Formal verification of the IEEE 802.11i WLAN security protocol, in Proc. Australian Software Engineering Conf., 2006. Google Scholar
22. R. H. Weber and R. Weber, Internet of Things: Legal Perspectives (Springer, 2010). Crossref, Google Scholar
23. X. Xing, E. M. Shakshuki, D. G. Benoit and T. R. Sheltami, Security analysis and authentication improvement for IEEE 802.11i specification, in Proc. Global Telecommunications Conf., 2008, pp. 1887–1891. Google Scholar