donstuAdvanced Engineering Research (Rostov-on-Don)Advanced Engineering Research (Rostov-on-Don)2687-1653Don State Technical Universitydonstu-887Research ArticlePHYSICAL AND MATHEMATICAL SCIENCESФИЗИКО-МАТЕМАТИЧЕСКИЕ НАУКИVERIFICATION OF KEY MANAGEMENT CRYPTOGRAPHIC PROTOCOLS WITH COLORED PETRI NETSВерификация криптографических протоколов распределения ключей с использованием раскрашенных сетей ПетриМогилевскаяНадежда СергеевнаMogilevskayaNadezhda S.broshka@nm.ruКолчановСергей СергеевичKolchanovSergey S.servatwork@gmail.comДонской государственный технический университетРоссияDon State Technical UniversityRussian Federation20113012201111915351543Copyright © Mogilevskaya N.S., Kolchanov S.S., 20112011Могилевская Н.С., Колчанов С.С.Mogilevskaya N.S., Kolchanov S.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/887

The possibility of using colored Petri nets for the analysis of key distribution cryptographic protocols as an example of symmetric Needham—Schroeder protocol is reviewed and evaluated.

Рассмотрена и оценена возможность применения раскрашенных сетей Петри для анализа криптографических протоколов распределения ключей на примере симметричного протокола Нидхема — Шрёдера.

верификация протоколаформальный анализраспределение ключейпротокол Нидхема — Шрёдерараскрашенные сети ПетриCPN Tools.protocol verificationformal analysiskey managementNeedham—Schroeder protocolcolored Petri netsCPN Tools.ReferencesОсновы криптографии / А. П. Алфёров [и др.]. — Москва: Гелиос АРВ, 2005. — 480 с.Osnovy` kriptografii / A. P. Alfyorov [i dr.]. — Moskva: Gelios ARV, 2005. — 480 s. — In Russian.Denning, D. E. Time stamps in Key Distribution Protocols / D. E. Denning, M. Smid // Com-munications of the ACM. — 1981. — V. 24. — P. 533—536.Denning, D. E. Time stamps in Key Distribution Protocols / D. E. Denning, M. Smid // Com-munications of the ACM. — 1981. — V. 24. — P. 533—536.Котенко, И. В. Верификация протоколов безопасности на основе комбинированного использования существующих методов и средств / И. В. Котенко, С. А. Резник, А. В. Шоров // Труды СПИИРАН. — 2009. — Вып. 8. — С. 292—310.Kotenko, I. V. Verifikaciya protokolov bezopasnosti na osnove kombinirovannogo is-pol`zovaniya sushhestvuyushhix metodov i sredstv / I. V. Kotenko, S. A. Reznik, A. V. Shorov // Trudy` SPIIRAN. — 2009. — Vy`p. 8. — S. 292—310. — In Russian.Могилевская, Н. С. Сравнение возможностей сетей Петри и BAN-логики в анализе криптографических протоколов проверки подлинности и обмена ключами / Н. С. Могилевская, С. С. Колчанов // Системный анализ, управление и обработка информации. — Ростов-на-Дону: Изд. центр ДГТУ, 2011. С. 98—101.Mogilevskaya, N. S. Sravnenie vozmozhnostej setej Petri i BAN-logiki v analize kriptografi-cheskix 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.Смарт, Н. Криптография / Н. Смарт. — Москва: Техносфера, 2006. — 528 с.Smart, N. Kriptografiya / N. Smart. — Moskva: Texnosfera, 2006. — 528 s. — In Russian.Lin, H. Algorithms for Cryptographic Protocol Verification in Presence of Algebraic Properties: diss. for the degree of Doctor of Philosophy (Mathematics). — Clarkson University, 2009.Lin, H. Algorithms for Cryptographic Protocol Verification in Presence of Algebraic Properties: diss. for the degree of Doctor of Philosophy (Mathematics). — Clarkson University, 2009.Nieh, B. Modeling and analyzing cryptographic protocols using Petri nets / B. Nieh, S. Tavares // Auscrypt'92, 1992.Nieh, B. Modeling and analyzing cryptographic protocols using Petri nets / B. Nieh, S. Tavares // Auscrypt'92, 1992.Salah, A. Protocol verification and analysis using colored Petri nets / A. Salah, M. Khaled. — Cairo University, 2003. — P. 3—7.Salah, A. Protocol verification and analysis using colored Petri nets / A. Salah, M. Khaled. — Cairo University, 2003. — P. 3—7.Котов, В. Е. Сети Петри / В. Е. Котов. — Москва: Наука, 1984. — 160 с.Kotov, V. E. Seti Petri / V. E. Kotov. — Moskva: Nauka, 1984. — 160 s. — In Russian.CPN Tools Homepage. Documentation. Electronic resource. Access mode: http://cpntools.org/documentation/start/ (date of access: 11.04.2011).CPN Tools Homepage. Documentation. Electronic resource. Access mode: http://cpntools.org/documentation/start/ (date of access: 11.04.2011).

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