A process-based approach to verifying cryptographic protocols

The article presents a new mathematical model of cryptographic protocols and provides examples of using this model to solve problems of verification of cryptographic protocols. Cryptographic protocols are communication protocols implemented using cryptographic algorithms to solve information security problems, within which participants in information interaction consistently perform certain actions and exchange messages. They are used, for example, in electronic payments, electronic voting procedures, systems of access to confidential data, etc. Errors in cryptographic protocols can lead to significant damage, so it is necessary to use mathematical methods to justify various properties of correctness and security of cryptographic protocols. The article presents new methods of formal verification of cryptographic protocols. To model cryptographic protocols, the concepts of sequential and distributed processes are introduced. The proposed approach is intended only to prove the correctness of cryptographic protocols. A feature of the protocol model is its simplicity in comparison with other protocol models based on logical formulas or algebraic expressions of processes. Protocol participants are represented as graphs, which are transition systems. The actions performed by the participants are labels of these transitions. The methods of proving the correctness of protocols considered in the article are associated with reasoning on graphs, which are simpler and more visual compared to methods based on constructing logical inference in logical-algebraic models of protocols.