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 structuresReferences
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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/10.1007/978-3-319-15147-2_20
14. D. Hercog, Communication Protocols. Principles, Methods and Specifications, Springer, 2020, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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 https://doi.org/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.
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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/10.1007/978-3-319-15147-2_20
14. D. Hercog, Communication Protocols. Principles, Methods and Specifications, Springer, 2020, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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, https://doi.org/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 https://doi.org/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.
