Оптимизация программ на ProVerif для криптографических протоколов выработки общего ключа

Криптографические протоколы используются для установления безопасного соединения между “честными” агентами, которые общаются строго в соответствии с правилами протокола. Для того, чтобы убедиться, что спроектированный криптографический протокол является криптографически стойким, обычно используются различные программные инструменты. Однако, адекватная спецификация криптографического протокола обычно представляется в виде набора требований к последовательностям передаваемых сообщений, включая формат таких сообщений. Выполнение всех этих требований приводит к тому, что формальная спецификация для реального криптографического протокола становится громоздкой, в следствии чего её трудно анализировать формальными методами. Одним из таких стремительно развивающихся инструментов для формальной верификации криптографических протоколов является ProVerif. Отличительной особенностью инструмента ProVerif является то, что при больших протоколах он часто не справляется с их анализом, т.е. не может ни доказать безопасность протокола, ни опровергнуть её. В таких случаях прибегают либо к апроксимации задачи, либо к эквивалентным преобразованиям модели программы на языке ProVerif, упрощающих ProVerif-модель. В этой статье мы предлагаем способ для упрощения ProVerif-спецификаций для AKE-протоколов, использующих схему шифрования Эль-Гамаля. А именно, мы предлагаем эквивалентные преобразования, позволяющие построить ProVerif-спецификацию, которая упрощает анализ спецификации для инструмента ProVerif. Экспериментальные результаты для криптопротоколов Нидхема-Шрёдера и Yahalom показывают, что такой подход может быть перспективным для автоматической проверки реальных протоколов.