Применение TLA+/TLC для моделирования и верификации криптографических протоколов

Взаимодействие в открытых сетях несёт определённые риски. Для обеспечения информационной безопасности участников сетевого взаимодействия используют криптографические протоколы. Высокие гарантии безопасности могут быть достигнуты в результате их формальной верификации. Распространённым формальным методом верификации криптографических протоколов является метод проверки модели. В работе для проверки модели криптографических протоколов предлагается использовать инструментальное средство TLA+/TLC, широко применяемое на практике в различных прикладных областях. На языке спецификации TLA+ задаётся модель протокола, а также требуемые свойства безопасности в форме инвариантов. Модель протокола описывает его поведение в виде системы переходов, содержащей все возможные состояния модели протокола и переходы между ними. Для проведения автоматической проверки соответствия модели требуемым свойствам задействуется верификатор TLC. Задача верификации криптографических протоколов имеет свою специфику. Настоящее исследование предлагает три приёма моделирования, учитывающих особенности данной задачи и используемого инструментария TLA+/TLC. Первый приём моделирования состоит в замене системы, состоящей из произвольного количества агентов, на трёхагентную систему. Это позволяет упростить модель и уменьшить её пространство состояний. Второй приём связан с представлением передаваемых сообщений в виде иерархической структуры — это даёт возможность вкладывать одни зашифрованные сообщения в другие. Третий приём состоит в оптимизации модели с целью повышения производительности верификатора TLC. Это выполняется путем задания функции, порождающей множество только тех элементов, которые приводят к переходам между состояниями в модели. В итоге предложенные приёмы позволяют упростить модель и снизить время её верификации. Применение результатов демонстрируется на примере простого протокола — протокола Нидхема-Шредера для аутентификации с открытым ключом. После обнаружения верификатором TLC известной уязвимости этого протокола выполняется моделирование и верификация его доработанной версии. Результаты верификации показывают, что новая версия протокола не имеет данной уязвимости.

1. “PNST 799-2022. Information Technologies. Cryptographic Protection of Information. Terms and Definitions.” [Online]. Available: https://protect.gost.ru/document.aspx?control=7&id=246680.

2. D. Basin, C. Cremers, and C. Meadows, “Model Checking Security Protocols,” in Handbook of Model Checking, Springer, 2018, pp. 727–762.

3. “GOST R ISO 7498-2-99. Information technology. Open systems interconnection. Basic reference model. Part 2. Security Architecture.” [Online]. Available: 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.” [Online]. Available: https://protect.gost.ru/document.aspx?control=7&id=201374.

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

6. M. Pourpouneh and R. Ramezanian, “A Short Introduction to Two Approaches in Formal Verification of Security Protocols: Model Checking and Theorem Proving,” ISeCure, vol. 8, no. 1, pp. 3–24, 2016, doi: 10.22042/isecure.2016.8.1.1.

7. C. Meadows, “Formal Analysis of Cryptographic Protocols,” in Encyclopedia of Cryptography, Security and Privacy, Springer, 2019, pp. 1–3.

8. E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, 1st ed., vol. 10. Springer, 2018.

9. “TLA+ Home.” [Online]. Available: https://lamport.azurewebsites.net/tla/tla.html.

10. R. M. Needham and M. D. Schroeder, “Using Encryption for Authentication in Large Networks of Computers,” Communications of the ACM, vol. 21, no. 12, pp. 993–999, 1978.

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

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

13. W. Mao, Modern Cryptography: Theory and Practice. Williams Publishing House, 2005, p. 768.

14. G. Lowe, “An Attack on the Needham-Schroeder Public-Key Authentication Protocol,” Information Processing Letters, vol. 56, no. 3, pp. 131–133, 1995.

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

16. M. A. Kuppe, L. Lamport, and D. Ricketts, “The TLA+ Toolbox,” Electronic Proceedings in Theoretical Computer Science, vol. 310, pp. 50–62, 2019, doi: 10.4204/eptcs.310.6.

17. R. Beers, “Pre-RTL Formal Verification: an Intel Experience,” in Proceedings of the 45th annual Design Automation Conference, 2008, pp. 806–811, doi: 10.1145/1391469.1391675.

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

19. C. Newcombe, T. Rath, F. Zhang, and et al., “How Amazon Web Services Uses Formal Methods,” Communications of the ACM, vol. 58, no. 4, pp. 66–73, 2015, doi: 10.1145/2699417.

20. Y.-M. Kim and M. Kang, “Formal Verification of SDN-based Firewalls by using TLA+,” IEEE Access, vol. 8, pp. 52100–52112, 2020, doi: 10.1109/ACCESS.2020.2979894.

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 ed. Springer, 2011.

22. V. A. Kukharenko, K. V. Ziborov, R. F. Sadykov, and et al., “Innochain: a Distributed Ledger for Industry with Formal Verification on All Implementation Levels,” Modeling and Analysis of Information Systems, vol. 27, no. 4, pp. 454–471, 2020, doi: 10.18255/1818-1015-2020-4-454-471.

23. V. Kukharenko, K. Ziborov, R. Sadykov, and et al., “Verification of Hotstuff BFT Consensus Protocol with TLA+/TLC in an Industrial Setting,” in SHS Web of Conferences, 2021, vol. 93, pp. 77–95, doi: 10.1051/shsconf/20219301006.

24. H. Guo, Y. Ji, and X. Zhou, “The Development of a TLA+ Verified Correctness Raft Consensus Protocol,” in Web and Big Data, 2024, vol. 14965, pp. 459–469, doi: 10.1007/978-981-97-7244-5_40.

25. R. Niyogi and A. Nath, “Formal Specification and Verification of a Team Formation Protocol using TLA+,” Software: Practice and Experience, vol. 54, no. 6, pp. 961–984, 2024, doi: 10.1002/spe.3307.

26. A. Jandoubi, M. T. Bennani, O. Mosbahi, and A. El Fazziki, “Analyzing MQTT Attack Scenarios: A Systematic Formalization and TLC Model Checker Simulation,” in Evaluation of Novel Approaches to Software Engineering, 2024, vol. 1, pp. 370–378, doi: 10.5220/0012625600003687.

27. J.-Q. Yin, H.-B. Zhu, and Y. Fei, “Specification and Verification of the Zab Protocol with TLA+,” Journal of Computer Science and Technology, vol. 35, pp. 1312–1323, 2020, doi: 10.1007/s11390-020-0538-7.

28. L. Ouyang, X. Sun, R. Tang, and et al., “Multi-Grained Specifications for Distributed System Model Checking and Verification.” 2024.

29. D. Dolev and A. Yao, “On the Security of Public Key Protocols,” IEEE Transactions on Information Theory, vol. 29, no. 2, pp. 198–208, 1983, doi: 10.1109/TIT.1983.1056650.

30. T. G. Keerthan Kumar and S. Ramu, “Formal Verfication of Security Protocol Using Spin Tool,” in International Conference on Advances in Information Technology, 2019, pp. 393–399, doi: 10.1109/ICAIT47043.2019.8987376.

31. S. Basagiannis, P. Katsaros, and A. Pombortsis, “An Intruder Model with Message Inspection for Model Checking Security Protocols,” Computers & Security, vol. 29, no. 1, pp. 16–34, 2010, doi: 10.1016/j.cose.2009.08.003.

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

33. G. Lowe, “Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 1996, vol. 1055, pp. 147–166, doi: 10.1007/3-540-61042-1_43.