Tamarin и вычислительные доказательства
Используйте средство доказательств Tamarin для переписывания мультимножеств и проверки на основе трасс
«Tamarin и вычислительные доказательства» — бесплатный урок Cryptology Academy на CoddyKit. Это урок 4 из 4. Ты можешь прочитать весь урок бесплатно ниже — а потом практиковать его прямо в браузере с встроенным редактором кода и ИИ-репетитором 24/7. Это часть пути обучения Cryptology Academy, и твой прогресс синхронизируется между веб-версией и приложением CoddyKit. Курс Cryptology Academy содержит 4 уроков всего.
Что такое Tamarin
Tamarin (ETH Zurich, 2012) — это проверяющий инструмент для протоколов безопасности, основанный на переписывании мультимножеств. В отличие от подхода ProVerif с хорновскими дизъюнктами, Tamarin рассуждает о трассах выполнения протокола с помощью интерактивной системы доказательств.
Tamarin и ProVerif
ProVerif: полностью автоматизирован, но может сообщить, что результат доказать невозможно. Tamarin: интерактивный помощник доказательств и автоматический режим, поддерживает эквациональные теории (XOR, Диффи—Хеллмана, билинейные отображения). Он выразительнее, но его сложнее изучать.
Правила переписывания мультимножеств
Tamarin моделирует протоколы как правила переписывания над фактами. Факты представляют состояние. Правило [ L ] --[ A ]-> [ R ] поглощает левые факты L, создаёт правые факты R и записывает действие A в трассу.
Входной язык Tamarin (.spthy)
Файл теории Tamarin объявляет функции, уравнения, правила и леммы:
/* Diffie-Hellman key exchange */
builtins: diffie-hellman
rule Alice_1:
[ Fr(~a) ] /* fresh random a */
--[ AliceSent($A, $B, 'g'^~a) ]->
[ Alice_St($A, $B, ~a), Out('g'^~a) ]
rule Bob_1:
[ In(ga), Fr(~b) ]
--[ BobReceived($A, $B, ga) ]->
[ Bob_St($A, $B, ~b, ga^~b), Out('g'^~b) ]Формулировка лемм
Цели безопасности выражаются как леммы над трассами:
/* Secrecy: shared secret not known to attacker */
lemma secret_key:
"All A B k #i #j.
AliceKey(A, B, k) @ i &
BobKey(A, B, k) @ j
==> not (Ex #r. K(k) @ r)"
/* Authentication: if Bob has key, Alice sent it */
lemma authentication:
"All A B k #j. BobKey(A, B, k) @ j
==> Ex #i. AliceKey(A, B, k) @ i & i < j"Запуск Tamarin
Запустите интерактивный GUI Tamarin: tamarin-prover interactive my_protocol.spthy. Браузерный интерфейс показывает обязательства по доказательству; Вы управляете автоматическими стратегиями или применяете ручные шаги для случаев, в которых выполнение не завершается.
Вычислительная состоятельность
Символические доказательства (ProVerif, Tamarin) гарантируют безопасность при допущении идеальной криптографии. Теоремы о вычислительной состоятельности (Cortier, Backes) переносят символические доказательства на вычислительную безопасность, если используются примитивы с доказанной безопасностью.
F* и HACL*: проверенные реализации
F* (Microsoft Research) — это язык программирования, ориентированный на доказательства. HACL* — криптографическая библиотека, написанная на F*, с машинно проверенными доказательствами корректности и устойчивости к атакам по побочным каналам. Она используется в Firefox NSS и mbedTLS.
EasyCrypt: вычислительные доказательства на основе игр
EasyCrypt позволяет строить полностью вычислительные доказательства безопасности (на основе игр) для криптографических конструкций, а не только протоколов. Слой записей TLS 1.3 и ChaCha20-Poly1305 были проверены в EasyCrypt.
Практическое значение
Формально проверенная криптография внедряется в промышленные системы: NSS (Firefox) использует HACL*, AWS применяет s2n-tls с утверждениями, сопровождающими доказательства, а протокол Signal был проверен в ProVerif и Tamarin. Формальные методы больше не являются исключительно академическими.
Проверка знаний
Чем Tamarin отличается от ProVerif при обработке случаев, в которых автоматизация не справляется?
Итоги урока
Tamarin использует переписывание мультимножеств и рассуждения на основе трасс с интерактивным GUI для доказательств. Он поддерживает эквациональные теории DH и XOR. Леммы выражают цели секретности и аутентификации. Вычислительная состоятельность связывает символические доказательства с реальной безопасностью. HACL* и EasyCrypt расширяют проверку до реализаций и криптографических конструкций.
Изучай Cryptology Academy с ИИ-репетитором — бесплатно
Пиши и запускай код прямо в браузере, получай мгновенную помощь от ИИ-репетитора 24/7 и продолжи учиться на сайте или в приложении.
- Курсы
- 67
- Уроки
- 261
Часто задаваемые вопросы
Урок «Tamarin и вычислительные доказательства» бесплатный?
Да — полный текст урока «Tamarin и вычислительные доказательства» бесплатно доступен здесь в веб-версии. Чтобы практиковать его интерактивно (встроенный редактор кода и ИИ-репетитор 24/7) и разблокировать остальной курс Cryptology Academy, подпишись на CoddyKit PRO. Курс Cryptology Academy содержит 4 уроков всего.
Чему я научусь в уроке «Tamarin и вычислительные доказательства»?
Используйте средство доказательств Tamarin для переписывания мультимножеств и проверки на основе трасс Ты практикуешь Cryptology Academy с помощью реального кода, который запускаешь прямо в браузере, и ИИ-репетитор 24/7 отвечает на твои вопросы во время урока.
Нужен ли мне опыт, чтобы начать Cryptology Academy?
Предыдущий опыт не требуется. Cryptology Academy на CoddyKit структурирован для всех уровней — от новичков до продвинутых, поэтому ты можешь начать отсюда или с самого начала и учиться в своем темпе. Это урок 4 из 4.
Сколько времени занимает урок «Tamarin и вычислительные доказательства»?
Большинство уроков CoddyKit занимают около 5–10 минут. Каждый из них компактный и интерактивный, поэтому ты постоянно делаешь прогресс и продолжаешь с того же места в веб-версии и приложении.
Можно ли писать и запускать код в этом уроке Cryptology Academy?
Да. Каждый урок Cryptology Academy включает встроенный редактор кода, поэтому ты пишешь и запускаешь реальный код прямо в браузере и получаешь моментальную обратную связь от AI — локальная установка не требуется.
Все уроки этого курса
- Почему неформальных доказательств недостаточно
- Модель атакующего Долева—Яо и символьная криптография
- ProVerif: автоматическая проверка протоколов
- Tamarin и вычислительные доказательства