Trivializing verification of cryptographic protocols

• Autorzy: Piątkowski Jacek , Szymoniak Sabina

Identyfikatory

DOI

10.24423/cames.869

• Języki publikacji: EN

Abstrakty

EN

One of the main problems of the digital world is information security. Every second, peopleprocess millions of pieces of information that must be protected from unauthorized access. Cryptographic protocols that define the communication plan and the cryptographictechniques used to secure the messages come to the rescue. These protocols should alsobe regularly verified regarding their ability to protect systems from exposure to threatsfrom the computer network. Bearing in mind the need to secure communication, verify thecorrect 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 theirverification based on the CMMTree model. In this article, we present a tool that verifiesa protocol’s security. The tool allows for modelling a protocol and verifying that the pathin 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 nodecan be attached to a tree. We conducted a number of tests on well-known cryptographicprotocols, which confirmed the correctness and effectiveness of our tool. The tool foundthe attack on the protocols or built an execution tree for them.

Słowa kluczowe

EN

security protocol verification; tree visualisation; hierarchical data structure

PL

weryfikacja protokołu bezpieczeństwa; wizualizacja drzewa; hierarchiczna struktura danych

• Wydawca: Instytut Podstawowych Problemów Techniki PAN
• Czasopismo: Computer Assisted Methods in Engineering and Science
• Rocznik: 2023
• Tom: Vol. 30, no. 4
• Strony: 389--406
• Opis fizyczny: Bibliogr. 37 poz., rys., tab.

Twórcy

autor

Piątkowski Jacek

• Department of Computer Science, Czestochowa University of Technology, Czestochowa, Poland

autor

Szymoniak Sabina

• Department of Computer Science, Czestochowa University of Technology, Czestochowa, Poland

Bibliografia

• 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.