Прувер Tamarin -- a security protocol verification tool that supports both falsification (attack finding) and unbounded verification (proving) in the symbolic model. Security protocols are specified as multiset rewriting systems and analyzed with respect to temporal first-order properties.

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

Кусочки универсальной алгебры, символьные вычисления первого порядка, состояния моделируются через логические формулы (например, в SMT-солверах или в BDD), стандартный модел-чекинг, процесс-алгебры (π-исчисление, ...),.

+перезапись термов конечно - темка топчик, но я рассказывал:
"Компиляторы, автоматы, AST, правила вывода, разбор json, редьюсинг алгебраических выражений, паттерн матчинг и многое многое другое -- это всё про переписывание термов."
Для серьёзных задач требуются сотни гигов оперативки:)

Написан Тамарин кстати на хаскеле, и должен заметить, что сильная система типов при создании подобных фреймворков для работы с ещё более сильной системой типов -- это никакой не плюс, а минус. Я уже писал об этом , Lean (функциональный язык с завтипчиками) -- казалось бы почти готовая HoTT, смоделировать гомотопическую теорию будет легко и просто, но нет. Сильная система содержит уже по своему определению сильные ограничения, никуда из неё уже не рыпнешься.

"...Это как попытка встроить квантовую механику в классическую физику: принципиально новый уровень абстракции."

Казалось бы, ну что, я умнее академиков что-ли, что я это понимаю, а они нет?
Тут сермяга в том, что я смотрю на это с точки зрения опыта и программной инженерии,
а у них это просто классика фейлов стартаперства, любой миддл знает: взялись пилить проект, особенно если он сложный и наукоёмкий, а потенциальные архитектурные ограничения проявились, только когда половина бюджета освоена и поздняк метаться. И "правильно было бы переписать всё заново с нуля" :)
Cобственно выбор хаскеля 💯⛔️

Мой же инсайт, что лучше всего получается на питоне, а начинал я это делать вообще на php, и альфа-версия на сайте работает :)


— Tamarin ограничен моделью маркированных графовых автоматов LTS, сети Петри и т.п., где переходы между состояниями описываются одномерными правилами перезаписи. Сложные структуры (например, гомотопии) требуют ручной абстракции.
— HoTT через высшие индуктивные типы позволяет моделировать многоуровневые переходы и гомотопические пути между состояниями, что особенно полезно для проверки свойств с топологической природой (криптографические протоколы с нелинейными взаимодействиями...).

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

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

— В Tamarin для доказательства эквивалентности требуется явно моделировать обе версии протокола и сравнивать их поведение.
Унивалентность HoTT позволяет легко и просто доказывать эквивалентности между структурами (например, между двумя версиями протокола, если они изоморфны).

— Tamarin работает с формальной общей логикой (AC, ассоциативность, коммутативность), но не поддерживает абстракции высшего уровня.
HoTT позволяет напрямую моделировать сложные математические объекты (группы гомотопий, усечения типов...). Во многих протоколах используются алгебраические структуры (Diffie-Hellman, билинейные формы) или топологические свойства (многомерные состояния...).

Резюме:
Tamarin эффективен для автоматизации проверки стандартных протоколов.

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

(потерпите, немного додумать осталось :)