АНАЛИЗ СТОЙКОСТИ К АТАКАМ КРИПТОГРАФИЧЕСКИХ ПРОТОКОЛОВ С ИСПОЛЬЗОВАНИЕМ ФОРМАЛЬНОГО ВЕРИФИКАТОРА SPIN

Е. А. Перевышина; Л. К. Бабенко

Е. А. Перевышина Южный Федеральный Университет
Л. К. Бабенко Южный Федеральный Университет

Ключевые слова: Верификация, SPIN, протокол Нидхема-Шредера

Аннотация

В основе безопасности любой защищенной системы, в которой используется переда-ча данных между двумя и более сторонами, лежат криптографические протоколы. Для оценки качества и безопасности разрабатываемых протоколов применяют различные инструменты формальной верификации. Инструменты, ориентированные на верификацию протоколов безопасности такие как Scyther tool, AVISPA, ProVerif, используются для вери-фикации стандартных свойств (конфиденциальности, аутентификации), в то время как универсальные средства применяются для верификации более сложных свойств. Универ-сальное средство формальной верификации SPIN использует проверку на моделях с приме-нением темпоральной логики. Он не был специально разработан для проведения верифика-ции безопасности протоколов. Этот инструмент более сложный, но гибкий и позволяет разработчику криптографического протокола создать модель своего протокола на тре-буемом ему уровне абстракций, и проверить его на соблюдение поставленных целей про-верки. Цель данной работы – описать верификацию протокола Нидхема-Шредера с помо-щью средства проверки модели SPIN. Задачи исследования: описать язык Promela, кото-рый используется для составления модели в рассматриваемом инструменте; показать модель протокола для определения атак на аутентификацию сторон; описать взаимодей-ствующие стороны, передаваемые данные, порядок передаваемых сообщений между сто-ронами. В работе описано проведение верификации безопасности протокола Нидхема-Шредера с помощью формального верификатора SPIN на предмет наличия атак на аутентификацию. В результате выполнения работы были обнаружены атаки на аутенти-фикацию сторон, показаны схемы взаимодействия сторон при данных атаках.

Литература

1. Meadows C. Formal Verification of Cryptographic Protocols, Proceedings of the 4th Interna-tional Conference on the Theory and Applications of Cryptology: Advances in Cryptology. Springer-Verlag, 1995, pp. 135-150. 2. Cheremushkin A.V. Kriptograficheskie protokoly. Osnovnye svoystva i uyazvimosti [Crypto-graphic protocols. Basic properties and vulnerabilities]. Moscow: Akademiya, 2009, 272 p. 3. Kosachev A.S., Ponomarenko V.N. Analiz podkhodov k verifikatsii funktsiy bezopasnosti i mobil'nosti [Analysis of approaches to verification of security and mobility functions]. Mos-cow: Institut sistemnogo programmirovaniya RAN, 2004, 101 p.
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.