Trivializing verification of cryptographic protocols

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.