mermaid-to-proverif — скилл для Claude Code: модель ProVerif
Читает Mermaid-диаграмму криптографического протокола и собирает из неё модель ProVerif — файл .pv, готовый для проверки секретности и аутентификации.
npx skills add trailofbits/skills --skill mermaid-to-proverif -a claude-codeЧто делает mermaid-to-proverif
Скилл берёт Mermaid sequenceDiagram, в которой расписан обмен сообщениями криптографического протокола, и переводит её в модель для ProVerif. На выходе — .pv-файл, который запускают проверяющим инструментом. Диаграммы он не рисует: на вход подаётся готовая разметка со стрелками сообщений и пометками операций вроде Sign, Verify, DH, HKDF, Enc, Dec. Обычно это результат работы скилла crypto-protocol-diagram.
Работа разбита на шаги: участники и каналы, опись криптографических операций, объявления типов и функций, события, запросы безопасности, процессы каждой стороны, главный процесс, проверка. В комплекте есть пример examples/simple-handshake/ — на нём видно, как выглядит годная модель. Из инструментов нужны только Read, Write, Grep и Glob.
Отдельное требование: сначала выписать запросы достижимости событий. Смысл в том, что при недостижимом событии ответы на остальные запросы ничего не доказывают. Сам верификатор скилл не запускает, модель придётся скормить командой proverif model.pv — это повод держать ProVerif под рукой заранее.
Какие задачи решает
- собрать
.pv-модель из Mermaid-диаграммы протокола - доказать секретность сессионного ключа в самодельном рукопожатии
- проверить forward secrecy там, где в диаграмме есть эфемерные ключи
- поискать дыры под replay-атаки до выхода кода в прод
- разобрать чужую диаграмму и увидеть, какие примитивы в ней используются
Примеры запросов агенту
- Собери ProVerif-модель из этой Mermaid-диаграммы рукопожатия и проверь секретность сессионного ключа.
- Переведи диаграмму из `examples/simple-handshake/` в `.pv` и добавь запросы достижимости для каждого события.
- Проверь forward secrecy для этой схемы с эфемерными ключами.
Как установить mermaid-to-proverif
1Через Skills CLI (Vercel)
npx skills add trailofbits/skills --skill mermaid-to-proverif -a claude-code2Вручную: положить файлы
~/.claude/skills/mermaid-to-proverif/SKILL.mdПапка скилла целиком; для одного проекта — .claude/skills/mermaid-to-proverif/
1Через Skills CLI (Vercel)
npx skills add trailofbits/skills --skill mermaid-to-proverif -a codex2Вручную: положить файлы
.agents/skills/mermaid-to-proverif/SKILL.mdДля всех проектов — ~/.agents/skills/
1Через Skills CLI (Vercel)
npx skills add trailofbits/skills --skill mermaid-to-proverif -a cursor2Вручную: положить файлы
.cursor/skills/mermaid-to-proverif/SKILL.mdCursor читает и .agents/skills/, и .claude/skills/
1GitHub CLI
gh skill install trailofbits/skills mermaid-to-proverif2Вручную: положить файлы
.github/skills/mermaid-to-proverif/SKILL.md1Через Skills CLI (Vercel)
npx skills add trailofbits/skills --skill mermaid-to-proverif -a gemini-cli2Командой платформы
gemini skills install https://github.com/trailofbits/skills --path plugins/trailmark/skills/mermaid-to-proverifВручную: положить файлы
.devin/skills/mermaid-to-proverif/SKILL.mdСтарый путь .windsurf/skills/ тоже читается
Через Skills CLI (Vercel)
npx skills add trailofbits/skills --skill mermaid-to-proverif -a opencodeClaude.ai
Упакуйте папку в zip и загрузите в Settings → Capabilities → Skills
Из того же набора35
Весь набор →Похожие
Вопросы о mermaid-to-proverif
Как установить mermaid-to-proverif в Claude Code?
Выполните npx skills add trailofbits/skills --skill mermaid-to-proverif -a claude-code. Файл скилла появится по пути ~/.claude/skills/mermaid-to-proverif/SKILL.md.
Что делает mermaid-to-proverif?
Переводит Mermaid sequenceDiagram с криптографическим протоколом в модель ProVerif в виде .pv-файла. В модель добавляются запросы на секретность, аутентификацию и forward secrecy.
Чем он отличается от crypto-protocol-diagram?
crypto-protocol-diagram создаёт саму диаграмму, а этот скилл её читает. Если sequenceDiagram ещё нет, начинать нужно с первого.
