Сравнение ProVerif и Tamarin: математическая защита протоколов

«1303-приказ можно выполнить двумя путями: формально закрыть задачу или реально защитить систему. ProVerif и Tamarin, это о реальной защите. Они не просто показывают вам картинку с «бесконечной защитой»

, а требуют строить её кирпич за киркичом, формально, математически. Это скучный и болезненный процесс, но единственный способ понять, где в вашем протоколе скрываются щели для уязвимости.»

Моделирование и проверка протоколов: зачем это вообще нужно

Традиционные методы анализа безопасности — тестирование, пентесты, аудит кода — работают с уже существующими системами. Они могут обнаружить ошибки реализации, но не способны предсказать, что можно спроектировать изначально уязвимый протокол. Пример: механизм аутентификации, где сервер доверяет клиенту на основании непроверяемого утверждения, или схема обмена ключами, в которой теоретически возможен перехват сессии, даже если всё реализовано «по ГОСТу».

Формальная проверка протоколов решает эту проблему. Она рассматривает систему не как набор программных функций, а как математическую модель с набором аксиом, правил и возможных действий участников. В этой модели можно задать свойства безопасности («секретный ключ никогда не станет известен атакующему», «аутентификация успешна только для легального пользователя») и проверить, выполняются они всегда или существуют сценарии, где атакующий может нарушить свойство.

В российском контексте, особенно при работе с требованиями ФСТЭК и 152-ФЗ, формальная проверка становится дополнительным, а иногда обязательным инструментом для подтверждения защищенности критических компонентов инфраструктуры. Если протокол связи или механизм управления доступом проходит формальную проверку, это весомый аргумент для регулятора.

ProVerif: автоматическая верификация на основе исчисления процессов

ProVerif, это инструмент с открытым исходным кодом, разработанный в INRIA (Франция). Его основная идея: представление протокола как набор процессов, взаимодействующих через каналы. Протокол описывается на специальном языке, близком к функциональному программированию. ProVerif затем преобразует это описание в набор логических формул и пытаетс автоматически доказать или опровергнуть заданные свойства.

Как работает ProVerif

Вы описываете участников протокола (клиент, сервер, атакующий) как процессы. Каждый процесс может отправлять и получать сообщения, выполнять криптографические операции (шифрование, дешифрование, генерацию ключей). Сообщения могут быть секретными или публичными.

ProVerif строит возможные трассы выполнения — все комбинации действий, которые могут совершить участники. Затем он анализирует, может атакующий, наблюдая публичные сообщения и взаимодействуя с протоколом, получить секретное значение или нарушить инвариант.

Пример описания простого обмена ключами в стиле ProVerif:

free sKey: bitstring [private].
free cKey: bitstring [private].

process Client =
  new k: bitstring;
  out(channel, encrypt(k, sKey));
  in(channel, msg: bitstring);
  let decrypted = decrypt(msg, cKey) in
  if decrypted = k then end.

Здесь sKey и cKey — секретные ключи сервера и клиента, процесс клиента генерирует новый ключ k, шифрует его ключом сервера и отправляет, затем ожидает ответ и проверяет его.

ProVerif автоматически проверяет, может атакующий, не знающий sKey и cKey, получить значение k или подделать сообщение.

Сильные стороны ProVerif

• Автоматичность: для многих протоколов не требуется дополнительных усилий — описываете модель, задаёте свойства, запускаете проверку.
• Поддержка разнообразных криптографических конструкций: симметричное и асимметричное шифрование, хеши, цифровые подписи.
• Эффективность для протоколов без сложного состояния: где безопасность зависит от текущих сообщений, а не от долгой истории взаимодействий.

Ограничения ProVerif

• Не поддерживает проверку свойств, зависящих от времени (liveness properties) — например, «сообщение обязательно будет доставлено». Он проверяет только сохранение секретности и аутентичности (safety properties).
• Может выдавать ложные положительные результаты: иногда инструмент не может доказать безопасность и сообщает о возможной уязвимости, хотя на практике её нет. Это требует дополнительного анализа.
• Сложность описания протоколов с многоэтапным состоянием: например, протоколы с повторным использованием ключей или сложными условиями обновления.

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

Tamarin — более мощный и гибкий инструмент, разработанный в ETH Zurich. Он использует подход символического моделирования с возможностью интерактивного руководства доказательствами. Tamarin рассматривает протокол как набор правил, которые могут генерировать события (например, «клиент отправляет сообщение», «сервер получает сообщение»).

С помощью Tamarin можно проверять не только базовые свойства сохранения секретности, но и сложные временные свойства, свойства, связанные с очередностью событий, и даже свойства, зависящие от знания атакующего в разные моменты времени.

Как работает Tamarin

Вы описываете протокол в виде правил. Каждое правило имеет предпосылки (что должно быть известно или произойти перед его выполнением) и эффекты (что создаётся или изменяется после выполнения). Tamarin строит граф возможных трасс выполнения, но также позволяет вам вводить дополнительные ограничения и леммы, чтобы направлять поиск.

Пример описания того же обмена ключами в Tamarin:

rule Client_send:
  [ Fr(k) ]
  -->
  [ Out(encrypt(k, sKey)) ]

rule Server_receive:
  [ In(encrypt(k, sKey)) ]
  -->
  [ Out(encrypt(k, cKey)) ]

Tamarin позволяет задавать свойства в виде формул, например: «для каждого события отправки ключа клиентом существует соответствующее событие получения ключа сервером, и между ними ключ не был раскрыт». Проверка таких свойств часто требует интерактивного взаимодействия: инструмент может предложить возможную трассу нарушения, и вы должны либо доказать, что эта трасса невозможна, либо согласиться с уязвимостью.

Сильные стороны Tamarin

• Проверка временных и сложных инвариантов: можно формализовать свойства вроде «после трёх неудачных попыток аутентификации сессия завершается».
• Интерактивный режим: для сложных протоколов вы можете управлять процессом доказательства, добавляя промежуточные леммы.
• Поддержка модернизированных криптографических конструкций: например, доказательства с нулевым разглашением или схемы групповой аутентификации.

Ограничения Tamarin

• Сложность в освоении: требуется понимание не только протокола, но и методов формального доказательства.
• Не полностью автоматичен для сложных свойств: часто требуется участие эксперта для руководства процессом.
• Может требовать значительных ресурсов для протоколов с большим количеством правил и состояний.

Сравнительная таблица: ProVerif vs Tamarin

Критерий	ProVerif	Tamarin
Основной подход	Автоматическая верификация исчисления процессов	Символическое моделирование с интерактивными доказательствами
Типы проверяемых свойств	Сохранение секретности, аутентичность (safety)	Safety + liveness, временные свойства, сложные инварианты
Автоматичность	Высокая для простых протоколов	Средняя, часто требует руководства
Уровень сложности описания протокола	Относительно низкий, язык близок к программированию	Высокий, требует формализации правил и свойств
Поддержка криптографических конструкций	Шифрование, подписи, хеши	Шифрование, подписи, хеши, ZKP, групповые операции
Обработка ложных положительных результатов	Возможны, требуют ручного анализа	Менее вероятны благодаря интерактивному контролю
Требования к ресурсам	Средние	Высокие для сложных моделей
Применимость в контексте ФСТЭК/152-ФЗ	Для проверки базовых криптографических протоколов связи	Для проверки сложных систем управления доступом и многоэтапных протоколов аутентификации

Практическое применение в российских условиях

Оба инструмента могут быть использованы для формального подтверждения защищенности компонентов информационных систем, что актуально при выполнении требований регуляторов. Например:

• При разработке защищённого канала связи для системы, обрабатывающей персональные данные (152-ФЗ), можно использовать ProVerif для проверки, что сессионный ключ не может быть раскрыт даже при активном вмешательстве.
• При проектировании системы управления доступом с многоуровневой аутентификацией Tamarin поможет доказать, что невозможно получить права высокого уровня без последовательного прохождения всех этапов проверки.
• При аудите уже существующих протоколов, особенно в критических инфраструктурах, формальная проверка с помощью этих инструментов может выявить теоретические уязвимости, не обнаруженные при стандартном тестировании.

результаты формальной верификации, это не абсолютная гарантия безопасности реальной системы, но сильное математическое свидетельство отсутствия уязвимости в модели. Реализация должна точно соответствовать модели, иначе доказательство теряет силу.

Выводы и выбор инструмента

ProVerif, это инструмент для быстрой, автоматической проверки базовых криптографических свойств. Если вам нужно убедиться, что ваш протокол обмена ключами или аутентификации сохраняет секретность в условиях стандартных угроз, ProVerif будет эффективным выбором.

Tamarin, это инструмент для глубокого анализа сложных протоколов, где безопасность зависит от последовательности событий, временных ограничений или многоэтапных состояний. Он требует больше экспертных знаний и времени, но даёт более полные и точные результаты.

В российской практике, где часто требуется не просто соответствие формальным требованиям, но и демонстрация глубины анализа безопасности, Tamarin может стать более весомым аргументом. Однако для многих задач, особенно связанных с проверкой криптографических алгоритмов и простых протоколов связи, ProVerif оказывается достаточным и более экономичным по времени.

Ключевое правило: начинать с моделирования в ProVerif для получения быстрой обратной связи. Если он не может доказать безопасность или протокол слишком сложен, переходить к Tamarin для детального интерактивного анализа.