История двух миров - Hybrid-WireGuard

Статья Лафуркада, Махмуда, Рюо и Талеба (Lafourcade - Mahmoud - Ruhault - Taleb) с USENIX Security 2025 - одна из двух независимых параллельных работ, пересматривающих оригинальный PQ-WireGuard. Вторая - pq-wireguard-revisited (Hashimoto et al., IACR 2025/1758). Лафуркад и др. сосредоточились на формальной верификации и гибридизации, подготовив реализацию на Rust; Хасимото и др. сфокусировались на более компактном криптографическом редизайне с использованием нового примитива RKEM.

Три вклада

Формальный анализ PQ-WireGuard. Авторы моделируют PQ-WireGuard в SAPIC+ - фреймворке, который компилирует единую спецификацию для ProVerif, Tamarin и DeepSec. Это позволяет использовать сильные стороны каждого инструмента (Tamarin: ассоциативно-коммутативный DH; ProVerif: эффективный анализ неограниченного числа сессий; DeepSec: свойства эквивалентности трасс). Они находят пробелы в предшествующем символическом доказательстве (Donenfeld and Milner, Hülsing et al.), в частности упущенный сценарий UKS-атаки (unknown key-share), и показывают, что PQ-WireGuard наследует проблему WireGuard с отсутствием анонимности. Также они указывают на нестандартное определение инкапсуляции KEM в оригинальном PQ-WireGuard, влияющее на реализацию. Исправленная версия названа PQ-WireGuard⋆; для неё формально доказаны анонимность, стойкость к UKS, согласование ключей (agreement) и секретность.

Hybrid-WireGuard. Новый протокол, объединяющий PQ-WireGuard⋆ с классическим WireGuard, спроектирован для обеспечения гибридной безопасности: протокол защищён до тех пор, пока остаётся невзломанной хотя бы одна схема - классическая или постквантовая. Это рекомендуемый формат миграции на переходный период - такова позиция Европейского института телекоммуникационных стандартов (ETSI), гибрид X25519+ML-KEM в OpenSSH 9.9, PQ3 от Apple и др. Главный формальный результат: любая атака на Hybrid-WireGuard сводится к атаке на PQ-WireGuard⋆ и атаке на WireGuard.

Адаптивная стратегия вычислений. Наивная проверка всех необходимых свойств безопасности гибридного протокола в SAPIC+ приводит к комбинаторному взрыву. Авторы предлагают адаптивную стратегию, отсекающую пространство состояний с сохранением корректности (soundness) - на практике это необходимо, поскольку без фильтрации анализ становится невычислимым.

Реализация на Rust. "Универсальная, эффективная и готовая к использованию" реализация Hybrid-WireGuard на Rust с инстанциацией через Classic McEliece и ML-KEM, а также бенчмарки со сравнением против WireGuard, PQ-WireGuard и PQ-WireGuard⋆.

Отличия от работы Hashimoto et al.

Обе статьи независимо пришли к похожим выводам:

Обе выявили UKS-атаку из-за проблем с привязкой KEM
Обе отметили зависимость PQ-WireGuard от дополнительных допущений о KEM

Способы исправления различаются:

Аспект	Lafourcade et al.	Hashimoto et al.
Структурное изменение	Конкатенация статических PK с PSK в `H4`	Редизайн на базе RKEM, устранение дублирующего подмешивания PSK
PSK в key schedule	Два включения (сохранено)	Одно включение (упрощено)
Допущение о сокрытии идентичности	Отказ от "PK скрыты от нарушителя"; добавление PSK в MAC для защиты от DoS	Сохранение исходного допущения; доказательство сокрытия идентичности и несвязываемости
Накладные расходы защиты от DoS	Получатель выполняет операции с PK для поиска PSK (вопреки исходной модели DoS)	Исходная модель защиты от DoS сохранена
Память под PK на сервере	Classic McEliece (большой размер) сохранён	RKEM/Rebar уменьшает размер в 190 - 390 раз
Реализация	Rust с бенчмарками	Ссылка на доступную онлайн реализацию

На практике: работа Хасимото и др. - более удачный инженерный результат для развёртывания на уровне ядра (бюджет по памяти); работа Лафуркада и др. - более сильный результат в области формальных методов, предоставляющий рабочую гибридную реализацию на Rust, которую консервативные пользователи могут внедрять уже сегодня.

Обе работы - необходимые вводные для реального процесса стандартизации PQ-WireGuard.

Почему это важно

Статья также служит наглядным примером применения SAPIC+ к реальному промышленному протоколу - полезный ориентир для всех, кто проектирует постквантовые гибридные рукопожатия (TLS, IKEv2, Signal, IMessage PQ3 относятся к этой же категории).

Ссылки: pq-wireguard, pq-wireguard-revisited, reinforcing-kem, ml-kem, post-quantum-cryptography, crqc-timeline.