Security Verification in the Context of 5G Sensor Networks

• Autorzy: Remlein Piotr , Stachowiak Urszula

Identyfikatory

DOI

10.26636/jtit.2021.153221

• Języki publikacji: EN

Abstrakty

EN

In order to develop reliable safety standards for 5G sensor networks (SN) and the Internet of Things, appropriate verification tools are needed, including those offering the ability to perform automated symbolic analysis process. The Tamarin prover is one of such software-based solutions. It allows to formally prove security protocols. This paper shows the modus operandi of the tool in question. Its application has been illustrated using an example of an exchange of messages between two agents, with asynchronous encryption. The scheme may be implemented, for instance, in the TLS/DTLS protocol to create a secure cryptographic key exchange mechanism. The aim of the publication is to demonstrate that automated symbolic analysis may be relied upon to model 5G sensor networks security protocols. Also, a use case in which the process of modeling the DTLS 1.2 handshake protocol enriched with the TCP SYN Cookies mechanism, used to preventing DoS attacks, is presented.

Słowa kluczowe

EN

5G; automated symbolic analysis; Internet of things; security protocols; sensor networks

• Wydawca: Instytut Łączności - Państwowy Instytut Badawczy
• Czasopismo: Journal of Telecommunications and Information Technology
• Rocznik: 2021
• Tom: nr 2
• Strony: 107--119
• Opis fizyczny: Bibliogr. 19 poz., rys.

Twórcy

autor

Remlein Piotr

• Institute of Radiocommunications, Poznań University of Technology, Pl. M. Skłodowskiej-Curie 5, 60-965 Poznań, Poland

• https://orcid.org/0000-0002-7593-839X

autor

Stachowiak Urszula

• Faculty of Computing and Telecommunications, Poznań University of Technology, Pl. M. Skłodowskiej-Curie 5, 60-965 Poznań, Poland

• https://orcid.org/0000-0002-6892-6876

Bibliografia

• [1] M. Nadimpalli, „Internet of Things - future outlook", Int. J. of Innov. Res. in Comp. and Commun. Engin., vol. 5, no. 6, 2017 [Online]. Available: https://www.rroij.com/peer-reviewed/internetof-things-future-outlook-85898.html
• [2] S. Helme, „Perfect forward secrecy - an introduction", 2014 [Online]. Available: https://scotthelme.co.uk/perfect-forward-secrecy
• [3] Tamarin prover [Online]. Available: https://github.com/tamarin-prover/tamarin-prover/blob/develop/examples/classic/TLS Handshake.spthy
• [4] J. Y. Kim, R. Holz, W. Hu, and S. Jha, „Automated analysis of secure Internet of Things protocols", in Proc. of the 33rd Ann. Comp. Secur. Appl. Conf. ACSAC 2017, Orlando, FL, USA, 2017, pp. 238-249 (DOI: 10.1145/3134600.3134624).
• [5] J. Y. Kim, Automated-security-verification-of-IoT-protocols [Online]. Available: https://github.com/jun-kim/Automated-security-verification-of-IoT-protocols/blob/master/CoAP DTLShandshake.spthy
• [6] T. Cole, „Interview with Kevin Ashton - inventor of IoT: Is driven by the users", Smart Industry the IoT Business Magazin, 2018 [Online]. Available: https://www.smart-industry.net/interview-with-iotinventor-kevin-ashton-iot-is-driven-by-the-users/
• [7] T. Salman and R. Jain, „A survey of protocols and standards for Internet of Things", Adv. Comput. and Commun., vol. 1, no. 1, 2017 (DOI: 10.34048/2017.1.f3).
• [8] E. Rescorla, The Transport Layer Security (TLS) Protocol Version 1.3, draft-ietf-tls-tls13-28 - 20, 2018 [Online]. Available: https://tools.ietf.org/html/draft-ietf-tls-tls13-28
• [9] E. Rescorla, H. Tschofenig, and N. Modadugu, The Datagram Transport Layer Security (DTLS) Protocol Version 1.3, draft-rescorla-tlsdtls13-01-13, 2017 [Online]. Available: https://datatracker.ietf.org/doc/html/draft-rescorla-tls-dtls13-01
• [10] S. Meier, B. Schmidt, C. Cremers, and D. Basin, „The Tamarin prover for the symbolic analysis of security protocols", in Computer Aided Verification 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, N. Sharygina and H. Veith, Eds. LNCS, vol. 8044, pp. 696-701. Springer, 2013 (ISBN: 9783642397981).
• [11] J. Thakkar TLS 1.3 Handshake: Taking a Closer Look, 2018 [Online]. Available: https://www.thesslstore.com/blog/tls-1-3-handshake-tls-1-2/
• [12] D. Basin, C. Cremers, J. Dreier, S. Meier, R. Sasse, and B. Schmidt, Tamarin-Prover Manual Security Protocol Analysis in the Symbolic Model, 2019 [Online]. Available: https://tamarin-prover.github.io/manual/tex/tamarin-manual.pdf
• [13] D. Basin, C. Cremers, J. Dreier, R. Sasse, „Symbolically analyzing security protocols using Tamarin", ACM SIGLOG News, vol. 4, no. 4, 2017, pp. 19-30 [Online]. Available: https://hal.archives-ouvertes.fr/hal-01622110/file/tamarin-tool.pdf
• [14] Q. Do, B. Martini, and K. R. Choo, „The role of the adversary model in applied security research", Comp. & Secur., vol. 81, pp. 156-181, 2019 (DOI: 10.1016/j.cose.2018.12.002).
• [15] W. Diffie and M. Hellman, „New directions in cryptography", IEEE Trans. on Inform. Theory, vol. 22, no. 6, pp. 644-654, 1976 (DOI: 10.1109/TIT.1976.1055638).
• [16] The Illustrated TLS Connection [Online]. Available: https://tls.ulfheim.net/
• [17] L. C. Paulson, „Inductive analysis of the Internet protocol TLS", ACM Trans. on Inform. and Syst. Secur., vol. 2, no. 3, pp. 332-351, 1999 (DOI: 10.1145/322510.322530).
• [18] G. Ferro, TCP SYN Cookies - DDoS defence, 2008 [Online]. Available: https://etherealmind.com/tcpsyn-cookies-ddos-defence/
• [19] E. Rescorla and N. Modadugu, “Datagram Transport Layer Security Version 1.2”, 2012 [Online]. Available: https://tools.ietf.org/html/rfc6347