VERIFICATION OF CRYPTOGRAPHIC PROTOCOLS WITH THE SPIN TOOL
The security of any protected system that uses data transfer between two or more parties is based on cryptographic protocols. To assess the quality and safety of the developed protocols, various formal verification tools are used. Formal verification tools, such as Scyther tool, Avispa, ProVerif, used to verify standard properties (confidentiality, authentication), while universal tools are used to verify more complex properties. The universal formal verification tool SPIN uses model checking using temporal logic. SPIN was not specifically designed for protocol security verification. This tool is more complex, but versatile and allows the cryptographic protocol developer to create a model of his protocol at the level of abstractions he needs and check it for compliance with the set verification goals. The purpose of this paper is to describe the verification of the Needham-Schroeder protocol using the SPIN tool. Research objectives: describe the Promela language, which is used to compile the model in the tool in question; show a protocol model to identify attacks on authentication of the parties; describe the interacting parties, the transmitted data, the order of transmitted messages between the parties. The paper describes the security verification of the Needham-Schröder protocol using the formal SPIN verifier for authentication attacks. As a result of the work, attacks on authentication of the parties were detected, the interaction patterns of the parties during these attacks are shown.