VERIFICATION OF CRYPTOGRAPHIC PROTOCOLS WITH THE SPIN TOOL
Abstract
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 mod-el checking using temporal logic. SPIN was not specifically designed for protocol security verifi-cation. 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 veri-fication of the Needham-Schröder protocol using the formal SPIN verifier for authentication at-tacks. As a result of the work, attacks on authentication of the parties were detected, the interac-tion patterns of the parties during these attacks are shown.
References
4. Scyther tool: automated analysis of security protocols. Available at: https://people.cispa.io/ cas.cremers/scyther/.
5. The AVISPA Project. Available at: http://www.avispa-project.org/. 6. ProVerif: Cryptographic protocol verifier in the formal model. Available at: https://prosecco.gforge.inria.fr/personal/bblanche/proverif/. 7. Kotenko I.V., Reznik S.A., Shorov A.V. Verifikatsiya protokolov bezopasnosti na osnove kombinirovannogo ispol'zovaniya sushchestvuyushchikh metodov i sredstv [Security protocols verification combining existing approaches and tools], Tr. SPIIRAN [SPIIRAS Proceedings], Vol. 8, pp. 292-310.
8. SPIN home page. Available at: http://SPINroot.com. 9. Klark E., Gramberg O., Peled D. Verifikatsiya modeley programm: Model Checking [Program Model Verification: Model Checking]. Moscow: MTSNMO, 2002. 10. Lependin A.A., Ubert A.V. Metod verifikatsii modeley v prilozhenii k analizu protokolov autentifikatsii [Model verification method as applied to authentication protocol analysis], Izvestiya Altayskogo gosudarstvennogo universiteta [Proceedings of the Altai state Universi-ty], 2012, Vol. 2, Issue 1 (73), pp. 84-86.
11. Needham R.M., Schroeder M.D. Using encryption for authentication in large networks of computers, Communications of the ACM, 1978, Vol. 21, No. 12, pp. 993-999. 12. Shoshmina I.V., Karpov Yu.G. Vvedenie v yazyk Promela i sistemu kompleksnoy verifikatsii Spin [Introduction to the language Promela and the verification system of complex Spin]. Saint Petersburg: Sankt-Peterburgskiy gosudarstvennyy politekhnicheskiy universitet, 2009. 13. Mironov A.M. Verifikatsiya programm metodom Model Checking [Verification of programs using Model Checking]. Moscow, 2012, 84 p. 14. Lukin M.A., Shalyto A.A. Verifikatsiya avtomatnykh programm s ispol'zovaniem verifikatora SPIN [Verification of automated programs using the SPIN verifier], Nauchno-tekhnicheskiy vestnik informatsionnykh tekhnologiy, mekhaniki i optiki [Scientific and technical Bulletin of information technologies, mechanics and optics], 2008, No. 8 (53), pp. 145-162. 15. Karpov Yu.G. Temporal'nye logiki dlya spetsifikatsii svoystv programmnykh i apparatnykh sistem [Temporal logics for specifying the properties of software and hardware systems], Komp'yuternye instrumenty v obrazovanii [Computer tools in education], 2009, No. 2, pp. 45-56.
16. Holzmann G.J. The model checker SPIN, IEEE Transactions on software engineering, 1997, Vol. 23, No. 5, pp. 279-295.
17. Barnat J., Brim L., Stříbrná J. Distributed LTL model-checking in SPIN, International SPIN Workshop on Model Checking of Software. Springer, Berlin, Heidelberg, 2001, pp. 200-216.
18. Borkhalenko V.A. Model' narushitelya dlya formal'noy verifikatsii kriptograficheskikh protokolov [The intruder model for cryptographic protocols formal verification], Estestvennye i matematicheskie nauki v sovremennom mire: Cb. st. po mater. XXVI mezhdunar. nauch.-prakt. konf. [Natural and mathematical Sciences in the modern world: a Collection of articles on the materials of the XXVI international scientific and practical conference]. Novosibirsk: SibAK, 2015, No. 1 (25).
19. Corradini A. The SPIN Model Checker. Metodi di Verifica del Software. Lezione 5.2013.
20. Lowe G. An Attack on the Needham – Schroeder Public – Key Authentication Protocol, In-formation processing letters, 1995, Vol. 56, No. 3.
