Using TLA+/TLC for modeling and verification of cryptographic protocols

M. V. Neyzov ; E. V. Kuzmin

Modelirovanie i analiz informacionnyh sistem, Tome 31 (2024) no. 4, pp. 446-473.

Résumé

Interacting in open networks carries certain risks. To ensure the information security of network interaction participants, cryptographic protocols (CrP) are used. High levels of security can be achieved through their formal verification. A common formal method for verifying CrP is model checking. In this work, we propose using the TLA+/TLC toolset to check models of CrP. This toolset is widely applied in various practical fields. The protocol model is defined in the TLA+ specification language, as well as the required security properties in the form of invariants. The model of a protocol describes its behavior as a transition system containing all possible states of the protocol model and transitions between them. The TLC model checker is employed to automatically verify that the model meets the required properties. The task of verifying CrP has its specifics. This study proposes three modeling techniques that take into account the specifics of both the task and the TLA+/TLC toolset being used. The first technique involves replacing a system consisting of an arbitrary number of agents with a three-agent system. This simplifies the model and reduces its state space. The second technique is related to representing transmitted messages as a hierarchical structure, allowing encrypted messages to be nested within others. The third technique consists of optimizing the model to improve the performance of the TLC model checker by defining a function that generates only those elements leading to transitions between states in the model. These techniques simplify the model and reduce verification time. We demonstrate the application of these results on a simple protocol example — the Needham-Schroeder public key authentication protocol. After detecting a known vulnerability in the original protocol by using TLC, we model and verify an improved version. Verification results show that the new version of the protocol does not have this vulnerability.

Détail

Keywords: protocol vulnerability, security properties, authentication, Needham-Schroeder protocol, asymmetric encryption system, formal verification, verification duration, model checking, transition system, protocol model, modeling techniques, generating function.

Bibliographie

[1] PNST 799-2022. Information Technologies. Cryptographic Protection of Information. Terms and Definitions (in Russian) https://protect.gost.ru/document.aspx?control=7&id=246680

[2] D. Basin, C. Cremers, C. Meadows, “Model Checking Security Protocols”, Handbook of Model Checking, ch. 22, Springer, 2018, 727–762 | DOI | MR | Zbl

[3] GOST R ISO 7498-2-99. Information technology. Open systems interconnection. Basic reference model. Part 2. Security Architecture (in Russian) https://protect.gost.ru/document.aspx?control=7&id=131456

[4] GOST R 56545-2015. Information protection. Vulnerabilities in information systems. Rules of vulnerabilities description (in Russian) https://protect.gost.ru/document.aspx?control=7&id=201374

[5] M. Roggenbach, S. A. Shaikh, H. N. Nguyen, “Formal Verification of Security Protocols”, Formal Methods for Software Engineering: Languages, Methods, Application Domains, Springer, 2022, 395–451 | DOI

[6] M. Pourpouneh, R. Ramezanian, “A Short Introduction to Two Approaches in Formal Verification of Security Protocols: Model Checking and Theorem Proving”, ISeCure, 8:1 (2016), 3–24 | DOI

[7] C. Meadows, “Formal Analysis of Cryptographic Protocols”, Encyclopedia of Cryptography, Security and Privacy, Springer, 2019, 1–3 | DOI | Zbl

[8] E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, Handbook of Model Checking, 10, 1st, Springer, 2018 | DOI | MR

[9] TLA+home, https://lamport.azurewebsites.net/tla/tla.html

[10] R. M. Needham, M. D. Schroeder, “Using Encryption for Authentication in Large Networks of Computers”, Communications of the ACM, 21:12 (1978), 993–999 | DOI | Zbl

[11] ISO/IEC 9798-1:2010. Information technology — Security techniques — Entity authentication — Part 1: General https://www.iso.org/ru/standard/53634.html

[12] ISO/IEC 11770-3:2021. Information security — Key management — Part 3: Mechanisms using asymmetric techniques https://www.iso.org/ru/standard/82709.html

[13] W. Mao, Modern Cryptography: Theory and Practice, Williams Publishing House, 2005, 768 (in Russian)

[14] G. Lowe, “An Attack on the Needham-Schroeder Public-Key Authentication Protocol”, Information Processing Letters, 56:3 (1995), 131–133 | DOI | Zbl

[15] L. Lamport, Specifying Systems: the TLA+ Language and Tools for Hardware and Software Engineers, 1st., Addison-Wesley, 2002, 364

[16] M. A. Kuppe, L. Lamport, D. Ricketts, “The TLA+ Toolbox”, Electronic Proceedings in Theoretical Computer Science, 310 (2019), 50–62 | DOI

[17] R. Beers, “Pre-RTL Formal Verification: an Intel Experience”, Proceedings of the 45th annual Design Automation Conference, 2008, 806–811 | DOI

[18] F. Hackett, J. Rowe, M. A. Kuppe, “Understanding Inconsistency in Azure Cosmos DB with TLA+”, 2023 IEEE/ACM 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), IEEE, 2023, 1–12 | DOI

[19] C. Newcombe, T. Rath, F. Zhang, and et al, “How Amazon Web Services Uses Formal Methods”, Communications of the ACM, 58:4 (2015), 66–73 | DOI

[20] Y. M. Kim, M. Kang, “Formal Verification of SDN-based Firewalls by using TLA+”, IEEE Access, 8 (2020), 52100–52112 | DOI

[21] E. Verhulst, R. T. Boute, J. M. S. Faria, and et al, Formal Development of a Network-Centric RTOS: Software Engineering for Reliable Embedded Systems, 1st, Springer, 2011 | DOI

[22] V. A. Kukharenko, K. V. Ziborov, R. F. Sadykov, and et al, “Innochain: a Distributed Ledger for Industry with Formal Verification on All Implementati on Levels”, Modeling and Analysis of Information Systems, 27:4 (2020), 454–471 (in Russian) | DOI | MR

[23] V. Kukharenko, K. Ziborov, R. Sadykov, and et al, “Verification of Hotstuff BFT Consensus Protocol with TLA+/TLC in an Industrial Setting”, SHS Web of Conferences, 93, Springer, 2021, 77–95 | DOI

[24] H. Guo, Y.Ji, X. Zhou, “The Development of a TLA+Verified Correctness Raft Consensus Protocol”, Web and Big Data, 14965, Springer, 2024, 459–469 | DOI

[25] R. Niyogi, A. Nath, “Formal Specification and Verification of a Team Formation Protocol using TLA+”, Software: Practice and Experience, 54:6 (2024), 961–984 | DOI

[26] A. Jandoubi, M. T. Bennani, O. Mosbahi, A. El Fazziki, “Analyzing MQTT Attack Scenarios: A Systematic Formalization and TLC Model Checker Simulation”, Evaluation of Novel Approaches to Software Engineering, v. 1, SciTePress, 2024, 370–378 | DOI

[27] J. Q. Yin, H. B. Zhu, Y. Fei, “Specification and Verification of the Zab Protocol with TLA+”, Journal of Computer Science and Technology, 35 (2020), 1312–1323 | DOI

[28] L. Ouyang, X. Sun, R. Tang, and et al, Multi-Grained Specifications for Distributed System Model Checking and Verification, 2024, arXiv: 2409.14301 [cs.DC]

[29] D. Dolev, A. Yao, “On the Security of Public Key Protocols”, IEEE Transactions on Information Theory, 29:2 (1983), 198–208 | DOI | MR | Zbl

[30] T. Keerthan Kumar, S. Ramu, “Formal Verfication of Security Protocol Using Spin Tool”, International Conference on Advances in Information Technology, IEEE, 2019, 393–399 | DOI

[31] S. Basagiannis, P. Katsaros, A. Pombortsis, “An Intruder Model with Message Inspection for Model Checking Security Protocols”, Computers Security, 29:1 (2010), 16–34 | DOI

[32] Needham-Schroeder Public Key Protocol Model Checking with TLA+/TLC https://github.com/MaximNeyzov/NSPK-model-checking

[33] G. Lowe, “Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR”, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, 1055, Springer, 1996, 147–166 | DOI