donstuAdvanced Engineering Research (Rostov-on-Don)Advanced Engineering Research (Rostov-on-Don)2687-1653Don State Technical Universitydonstu-491Research ArticlePHYSICAL AND MATHEMATICAL SCIENCESФИЗИКО-МАТЕМАТИЧЕСКИЕ НАУКИSOFTWARE TOOL FOR LOGICAL VALIDATION OF CRYPTOGRAPHIC KEY GENERATION PROTOCOLS BASED ON BAN-LOGICПрограммное средство логической проверки корректности криптографических протоколов распределения ключей на основе BANлогикиМогилевскаяНадежда СергеевнаMogilevskayaNadezhda S.broshka@nm.ruДонской государственный технический университетРоссияDon State Technical UniversityRussian Federation201230122012121-2515Copyright © Mogilevskaya N.S., 20122012Могилевская Н.С.Mogilevskaya N.S.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.vestnik-donstu.ru/jour/article/view/491

The idea of analyzing cryptographic key generation protocols through BAN - logic methods is considered. An e xample of Kerberos protocol analysis is given. The software tool that automates the analysis of key g eneration protocols is built. Its v alidation is investigated

Рассмотрена идея анализа криптографических протоколов распределения ключей методами BAN - логики; привед ё н пример анализа протокола Керберос; построено программное средство, автоматизирующее ан ализ протоколов распределения ключей; исследована корректность его работы.

формальный анализ протоколовкриптографические протоколыпротоколы распред еления ключейсредства автоматизированного анализа протоколовпротокол Керберос.ormal protocol analysiscryptographic protocolskey generation protocolscomputer - aided protocol analysis toolsKerberos protocol.ReferencesМогилевская, Н. С. Верификация криптографических протоколов распределения ключей с использованием раскрашенных сетей Петри / Н. С. Могилевская, С. С. Колчанов // Вестник Донского гос. техн. ун-та. — 2011. — Т. 11. — № 9. — С. 1535—1543.Mogilevskaya, N. S. Verifikaciya kriptograficheskix protokolov raspredeleniya klyuchej s ispol`zovaniem raskrashenny`x setej Petri / N. S. Mogilevskaya, S. S. Kolchanov // Vestnik Donskogo gos. texn. un-ta. — 2011. — T. 11. — № 9. — S. 1535—1543. — In Russian.Черёмушкин, А. В. Криптографические протоколы: основные свойства и уязвимости / А. В. Черёмушкин. — Москва: Ин-т криптографии, 2009. — 272 с.Cheryomushkin, A. V. Kriptograficheskie protokoly`: osnovny`e svojstva i uyazvimosti / A. V. Cheryomushkin. — Moskva: In-t kriptografii, 2009. — 272 s. — In Russian.Шнайер, Б. Прикладная криптография. Протоколы, алгоритмы, исходные тексты на языке Си / Б. Шнайер. — Москва: Триумф, 2002. — 816 с.Shnajer, B. Prikladnaya kriptografiya. Protokoly`, algoritmy`, isxodny`e teksty` na yazy`ke Si / B. Shnajer. — Moskva: Triumf, 2002. — 816 s. — In Russian.Burrows, M. A logic of authentication / M. Burrows, M. Abadi, R. Needham // ACM Transactions on Computer System. — V. 8. — № 1. — Feb. 1990. — P. 18—36.Burrows, M. A logic of authentication / M. Burrows, M. Abadi, R. Needham // ACM Transactions on Computer System. — V. 8. — № 1. — Feb. 1990. — P. 18—36.Могилевская, Н. С. Основы BАN-логики: метод. указания к практическим занятиям по курсу «Криптографические протоколы» [Электрон. ресурс] / Н. С. Могилевская. — Режим доступа: http://de.dstu.edu.ru/CDOCourses/3/3/20125c3d5375-aa2f-41fe-ac35-b71dc060ae20/1001/metho d/index.html (дата обращения: 15.10.2011).Mogilevskaya, N. S. Osnovy` BAN-logiki: metod. ukazaniya k prakticheskim zanyatiyam po kursu «Kriptograficheskie protokoly`» [E`lektron. resurs] / N. S. Mogilevskaya. — Rezhim dostupa: http://de.dstu.edu.ru/CDOCourses/3/3/20125c3d5375-aa2f-41fe-ac35-b71dc060ae20/1001/method/in dex.html (data obrashheniya: 15.10.2011). — In Russian.Могилевская, Н. С. Сравнение возможностей сетей Петри и BAN-логики в анализе криптографических протоколов проверки подлинности и обмена ключами / Н. С. Могилевская, С. С. Колчанов // Системный анализ, управление и обработка информации. — Ростов-на-Дону: Изд. центр ДГТУ, 2011. — С. 98—101.Mogilevskaya, N. S. Sravnenie vozmozhnostej setej Petri i BAN-logiki v analize kriptograficheskix protokolov proverki podlinnosti i obmena klyuchami / N. S. Mogilevskaya, S. S. Kolchanov // Sistemny`j analiz, upravlenie i obrabotka informacii. — Rostov-na-Donu: Izd. centr DGTU, 2011. — S. 98—101. — In Russian.Aly, S. Protocol verification and analysis using colored Petri nets. Technical report / S. Aly. — Cairo: Cairo University, 2003. — 26 p.Aly, S. Protocol verification and analysis using colored Petri nets. Technical report / S. Aly. — Cairo: Cairo University, 2003. — 26 p.

The authors declare that there are no conflicts of interest present.