Наконец, ProVerif: символьный подход к анализу протоколов, аналогично Tamarin, но с акцентом на автоматизированное рассуждение о криптографических свойствах. База -- типизированное расширение пи-исчисления с криптографией, язык моделирования параллельных процессов...
Криптографические примитивы (шифрование, хэширование, подписи) моделируются через функции и уравнения. Символьная модель криптографии Долева-Яо, клаузы Хорна (привет, Пролог), по сути абстрактные методы анализа, которые авторы сами придумали:)
Сложные структуры данных (например, вложенные списки или рекурсивные типы) требуют ручного моделирования.

=> ProVerif будет более практичным -- для автоматического анализа криптографических протоколов в символической модели.

В HoTT же например, можно определить тип "протокол с условиями на последовательность шагов", которые автоматически проверяются системой, и так можно верифицировать протоколы с жёсткими структурными ограничениями,

HoTT интегрирует категориальную логику и теорию гомотопий -- мощные математические инструменты для доказательства свойств безопасности, что особенно полезно для анализа протоколов с распределённой логикой или сложными взаимодействиями (можно например формализовать, что протокол удовлетворяет условию инъективной эквивалентности.)

В общем, HoTT превосходит и ProVerif, и все остальные, уверен 💯, в таких аспектах:
- строгая семантика эквивалентности через гомотопии.
- моделирование сложных структур данных с зависимыми типами.
- интеграция с категориальной логикой для доказательства сложных свойств.
- гомотопическая эквивалентность позволяет строго моделировать инварианты протоколов.
- высшие индуктивные типы могут описывать сложные взаимодействия (например, распределённые протоколы).

=

Всё, с темкой разобрался, я красавчик :)
В заключение остаётся ещё подумать, какие сделать правильные выводы из этого всего.

Вообще, как я начал делать курсы по HoTT, в плане математики голова за считанные месяцы прямо ощутимо прокачалась чисто на базе этой теории.