Применение TLA+/TLC для моделирования и верификации криптографических протоколов

Взаимодействие в открытых сетях несёт определённые риски. Для обеспечения информационной безопасности участников сетевого взаимодействия используют криптографические протоколы. Высокие гарантии безопасности могут быть достигнуты в результате их формальной верификации. Распространённым формальным методом верификации криптографических протоколов является метод проверки модели.
В работе для проверки модели криптографических протоколов предлагается использовать инструментальное средство TLA+/TLC, широко применяемое на практике в различных прикладных областях. На языке спецификации TLA+ задаётся модель протокола, а также требуемые свойства безопасности в форме инвариантов. Модель протокола описывает его поведение в виде системы переходов, содержащей все возможные состояния модели протокола и переходы между ними. Для проведения автоматической проверки соответствия модели требуемым свойствам задействуется верификатор TLC. Задача верификации криптографических протоколов имеет свою специфику. Настоящее исследование предлагает три приёма моделирования, учитывающих особенности данной задачи и используемого инструментария TLA+/TLC. Первый приём моделирования состоит в замене системы, состоящей из произвольного количества агентов, на трёхагентную систему. Это позволяет упростить модель и уменьшить её пространство состояний. Второй приём связан с представлением передаваемых сообщений в виде иерархической структуры — это даёт возможность вкладывать одни зашифрованные сообщения в другие. Третий приём состоит в оптимизации модели с целью повышения производительности верификатора TLC. Это выполняется путем задания функции, порождающей множество только тех элементов, которые приводят к переходам между состояниями в модели. В итоге предложенные приёмы позволяют упростить модель и снизить время её верификации. Применение результатов демонстрируется на примере простого протокола — протокола Нидхема-Шредера для аутентификации с открытым ключом. После обнаружения верификатором TLC известной уязвимости этого протокола выполняется моделирование и верификация его доработанной версии. Результаты верификации показывают, что новая версия протокола не имеет данной уязвимости.