11, N9 9 (60)
ФИЗИКО-МАТЕМАТИЧЕСКИЕ НАУКИ
УДК 004.414.023
Верификация криптографических протоколов распределения ключей с
использованием раскрашенных сетей Петри <...> Н. С. Могилевская, С. С. Колчанов
(Донской государственный технический университет)
Рассмотрена и оценена возможность применения раскрашенных сетей Петри для анализа криптографических протоколов распределения ключей на примере симметричного протокола Нидхема — Шредера. <...> Ключевые слова: верификация протокола, формальный анализ распределение ключей протокол Нидхема — Шрёаера, раскрашенные сети Петри, CPN Tools. <...> Фактически криптографический протокол — это распределённый алгоритм, определяющий последовательность шагов, точно специфицирующих действия, которые требуются от участников для решения некоторой криптографической задачи, например, обеспечение целопности, секретности, аутентичности информации [2, 3, 4]. <...> Формальный анализ и выявление
недостатков криптографических протоколов на деле оказывается весьма затруднительным. <...> По
итогам исследования моделей сделаны выводы о возможности верификации криптографических
1535
ФИЗИКО-ИЗ тематические науки
протоколов распределения ключей с использованием раскрашенных сетей Петри. <...> Для этого он отправляет А свой нонс в зашифрованном виде. <...> Сети Петри — это весьма востребованный математический аппарат для моделирования динамических дискретных сисгем. <...> Сеть Петри может быть задана как
алгебраически, так и графически. <...> С точки зрения алгебры, сеть Петри задаётся кортежем следующего вида С = (Р, T, I, 0, р), где Р, Т— конечные множества позиций (сосгояний сети) и
переходов (событий сети), I, 0— множества входных и выходных функций, р. — вектор натуральных чисел, определяющий маркировку сети. <...> Графически сеть Петри представляет собой
двудольный ориентированный граф, в котором позициям соответствуют вершины, изображаемые кружками, а переходам — вершины, изображаемые черточками или прямоугольниками;
функциям <...>