Trivializing Verification of Cryptographic Protocols - Piątkowski, Jacek; Szymoniak, Sabina (Computer Assisted Methods in Engineering and Science, 2023)
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.