Trivializing Verification of Cryptographic Protocols

Jacek Piątkowski; Sabina Szymoniak

doi:10.24423/cames.869

Jacek Piątkowski Department of Computer Science, Czestochowa University of Technology, Czestochowa, Poland
Sabina Szymoniak Department of Computer Science, Czestochowa University of Technology, Czestochowa, Poland

DOI: http://dx.doi.org/10.24423/cames.869

Abstract

One of the main problems of the digital world is information security. Every second, people process millions of pieces of information that must be protected from unauthorized access. Cryptographic protocols that define the communication plan and the cryptographic techniques used to secure the messages come to the rescue. These protocols should also be regularly verified regarding their ability to protect systems from exposure to threats from the computer network. Bearing in mind the need to secure communication, verify the correct operation of security methods and process large amounts of numerical data, we decided to deal with the issues of modeling the execution of cryptographic protocols and their verification based on the CMMTree model. In this article, we present a tool that verifies a protocol’s security. The tool allows for modelling a protocol and verifying that the path in the execution tree represents an attack on that protocol. The tool implements a specially defined hierarchy of protocol classes and a predicate that determines whether a node can be attached to a tree. We conducted a number of tests on well-known cryptographic protocols, which confirmed the correctness and effectiveness of our tool. The tool found the attack on the protocols or built an execution tree for them.

Keywords

security protocols verification, tree visualisation, hierarchical data structures,

References

1. A.V. Aho, J.D. Ullman, Foundations of Computer Science, 1st ed., W.H. Freeman & Co., USA, 1994.
2. G. Barnett, L. Del Tongo, Data Structures and Algorithms: Annotated Reference with Examples, DotNetSlackers, 2008.
3. D.A. Basin, C. Cremers, C.A. Meadows, Model checking security protocols, [in:] Handbook of Model Checking, E. Clarke, T. Henzinger, H. Veith, R. Bloem [Eds], pp. 727–762, Springer, Cham, 2018, doi: 10.1007/978-3-319-10575-8_22.
4. B. Blanchet, Modeling and verifying security protocols with the applied pi calculus and ProVerif, Foundations and Trends in Privacy and Security, 1(1–2): 1–135, 2016, doi: 10.1561/3300000004.
5. B. Blanchet, V. Cheval, V. Cortier, ProVerif with lemmas, induction, fast subsumption, and much more, [in:] IEEE Symposium on Security and Privacy (S&P’22), pp. 205–222, IEEE Computer Society, San Francisco, CA, 2022, https://hal.inria.fr/hal-03366962/.
6. R. Bouroulet, R. Devillers, H. Klaudel, E. Pelz, F. Pommereau, Modeling and analysis of security protocols using role based specifications and petri nets, [in:] K.M. van Hee, R. Valk [Eds], Applications and Theory of Petri Nets, pp. 72–91, Springer, Berlin, Heidelberg, 2008.
7. M. Burrows, M. Abadi, R. Needham, A logic of authentication, ACM Transactions on Computer Systems, 8(1): 18–36, 1990, doi: 10.1145/77648.77649.
8. Y. Chevalier et al., A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols, [in:] Workshop on Specification and Automated Processing of Security Requirements – SAPS’2004, pp. 13, Austrian Computer Society, Linz, Austria, 2004.
9. V. Cortier, S. Delaune, J. Dreier, Automatic generation of sources lemmas in tamarin: Towards automatic proofs of security protocols, [in:] L. Chen, N. Li, K. Liang, S. Schneider [Eds], Computer Security – ESORICS 2020, pp. 3–22, Springer, Cham, 2020.
10. A. David, K.G. Larsen, A. Legay, M. Mikuaionis, D.B. Poulsen, uppaal SMC tutorial, International Journal on Software Tools for Technology Transfer, 17(4): 397–415, 2015, doi: 10.1007/s10009-014-0361-y.
11. D. Dolev, A.C. Yao, On the security of public key protocols, [in:] Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, SFCS ’81, pp. 350–357, IEEE Computer Society, Washington, DC, USA, 1981.
12. D. Gregor, J. Järvi, J. Siek, G. Reis, B. Stroustrup, A. Lumsdaine, Concepts: Linguistic support for generic programming in C++, ACM SIGPLAN Notices, 41(10): 291–310, 2006, doi: 10.1145/1167515.1167499.
13. A. Grosser, M. Kurkowski, J. Piatkowski, S. Szymoniak, ProToc – An universal language for security protocols specifications, [in:] A. Wilinski, I.E. Fray, J. Pejas [Eds], Soft Computing in Computer and Information Science. Advances in Intelligent Systems and Computing, Vol. 342, pp. 237–248, Springer, Cham, 2014, doi: 10.1007/978-3-319-15147-2_20.
14. D. Hercog, Communication Protocols. Principles, Methods and Specifications, Springer, 2020, doi: 10.1007/978-3-030-50405-2.
15. A. Hess, S. Mödersheim, A typing result for stateful protocols, [in:] 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 374–388, IEEE, 2018, doi: 10.1109/CSF.2018.00034.
16. J. Järvi, D. Gregor, J. Willcock, A. Lumsdaine, J. Siek, Algorithm specialization in generic programming – Challenges of constrained generics in C++, ACM SIGPLAN Notices, 41(6): 272–282, 2006, doi: 10.1145/1133255.1134014.
17. A. Kassem, P. Lafourcade, Y. Lakhnech, S. Mödersheim, Multiple independent lazy intruders, [in:] 1st Workshop on Hot Issues in Security Principles and Trust (HotSpot 2013), 15 pages, 2013, http://www.cs.bham.ac.uk/mdr/research/projects/HotSpot-2013/papers/paper%2012.pdf.
18. B. Kordy, S. Mauw, S. Radomirovic, P. Schweitzer, Foundations of attack–defense trees, [in:] P. Degano, S. Etalle, J. Guttman [Eds], International Workshop on Formal Aspects in Security and Trust, FAST 2010. Lecture Notes in Computer Science, Vol. 6561, pp. 80–95, Springer, Berlin, Heidelberg, 2010, doi: 10.1007/978-3-642-19751-2_6.
19. R.L. Kruse, A.J. Ryba, Data Structures and Program Design in C++, Prentice-Hall, USA, 1998.
20. M. Kurkowski, Formalne metody weryfikacji wlasnosci protokolow zabezpieczajcych w sieciach komputerowych [in Polish], Akademicka Oficyna Wydawnicza Exit, Warszawa, 2013.
21. J. Liang, Q. Nguyen, S. Simoff, M. Huang, Divide and conquer treemaps: Visualizing large trees with various shapes, Journal of Visual Languages & Computing, 31: 104–127, 2015, doi: 10.1016/j.jvlc.2015.10.009.
22. S. Liu, T. Xiao, J. Liu, X. Wang, J. Wu, J. Zhu, Visual diagnosis of tree boosting methods, IEEE Transactions on Visualization and Computer Graphics, 24(1): 163–173, 2017, doi: 10.1109/TVCG.2017.2744378.
23. S. Mauw, M. Oostdijk, Foundations of attack trees, [in:] International Conference on Information Security and Cryptology, pp. 186–198, Springer, 2005, doi: 10.1007/11734727_17.
24. J.K. Millen, CAPSL: Common authentication protocol specification language, [in:] NSPW ’96: Proceedings of the 1996 workshop on New security paradigms, 1996, doi: 10.1145/304851.304879.
25. P. Morin, Open Data Structures (in C++), 2013, https://opendatastructures.org/.
26. S. Mödersheim, F. Nielson, H.R. Nielson, Lazy mobile intruders, [in:] D.A. Basin, J.C. Mitchell, [Eds], POST, Lecture Notes in Computer Science, Vol. 7796, pp. 147–166, Springer, 2013.
27. R.M. Needham, M.D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, 21(12): 993–999, 1978, doi: 10.1145/359657.359659.
28. B.C. Neuman, T. Ts’o, Kerberos: An authentication service for computer networks, IEEE Communications Magazine, 32(9): 33–38, 1994, doi: 10.1109/35.312841.
29. J. Piatkowski, The conditional multiway mapped tree: Modeling and analysis of hierarchical data dependencies, IEEE Access, 8: 74083–74092, 2020, doi: 10.1109/ACCESS.2020.2988358.
30. P.Y.A. Ryan, S.A. Schneider, M.H. Goldsmith, G. Lowe, A.W. Roscoe, The Modelling and Analysis of Security Protocols: The CSP Approach, 1st ed., Addison-Wesley Professional, Harlow, London, 2000.
31. O. Siedlecka-Lamch, S. Szymoniak, M. Kurkowski, A fast method for security protocols verification, [in:] Computer Information Systems and Industrial Management: Proceedings of the 18th International Conference, CISIM 2019, Belgrade, Serbia, September 19–21, 2019, pp. 523–534, 2019, doi: 10.1007/978-3-030-28957-7_43.
32. O. Siedlecka-Lamch, S. Szymoniak, M. Kurkowski, I.E. Fray, Towards most efficient method for untimed security protocols verification, [in:] 24th Pacific Asia Conference on Information Systems, PACIS 2020 Proceedings, Dubai, UAE, June 22–24, 2020, p. 189, 2020, https://aisel.aisnet.org/pacis2020/189/.
33. J.G. Siek, A. Lumsdaine, A language for generic programming in the large, Science of Computer Programming, 76(5): 423–465, 2011, doi: 10.1016/j.scico.2008.09.009.
34. S. Szymoniak, Amelia—A new security protocol for protection against false links, Computer Communications, 179: 73–81, 2021, doi: 10.1016/j.comcom.2021.07.030.
35. S. Szymoniak, M. Kurkowski, J. Piatkowski, Timed models of security protocols including delays in the network, Journal of Applied Mathematics and Computational Mechanics, 14(3): 127–139, 2015 doi: 10.17512/jamcm.2015.3.14.
36. J.-P. Tremblay, P.G. Sorenson, An Introduction to Data Structures with Applications, 2nd ed., Computer Science Series, McGraw-Hill, Auckland, 1984.
37. I.H. Witten, E. Frank, M.A. Hall, Data Mining: Practical Machine Learning Tools and Techniques, 3rd ed., Morgan Kaufmann Series in Data Management Systems, Morgan Kaufmann, Amsterdam, 2011.