Tamarin 与计算型证明
使用 Tamarin 证明器进行多重集重写和基于轨迹的验证
Tamarin 与计算型证明 是 CoddyKit 上的免费 Cryptology Academy 课时。 这是第 4 节课，共 4 节。 你可以在下方免费阅读本课时的完整内容 — 然后在浏览器中使用内置代码编辑器和全天候 AI 导师进行实践。 这是 Cryptology Academy 学习路径的一部分，你的进度在网页和 CoddyKit 应用中同步。 Cryptology Academy 课程共包含 4 节课。
什么是 Tamarin
Tamarin（ETH Zurich，2012）是一种基于多重集重写的安全协议验证器。与 ProVerif 的霍恩子句方法不同，Tamarin 使用交互式证明器对协议执行的轨迹进行推理。
Tamarin 与 ProVerif 的比较
ProVerif：完全自动化，但可能报告“无法证明”。Tamarin：交互式证明助手 + 自动化模式，能够处理等式理论（XOR、Diffie-Hellman、双线性映射）。表达能力更强，但学习曲线更陡峭。
多重集重写规则
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
启动 Tamarin 的交互式 GUI：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 将验证扩展到实现和构造。
用 AI 导师学习 Cryptology Academy — 免费
在浏览器中编写并运行真实代码，获得全天候 AI 导师的即时帮助，并在网页或应用中继续学习。
- 课程
- 67
- 课程
- 261
常见问题解答
「Tamarin 与计算型证明」课时是免费的吗？
是的 — 「Tamarin 与计算型证明」的完整文本可在网页上免费阅读。要进行交互式练习（内置代码编辑器和全天候 AI 导师）并解锁 Cryptology Academy 课程的其余内容，请升级到 CoddyKit PRO。 Cryptology Academy 课程共包含 4 节课。
「Tamarin 与计算型证明」这节课中我会学到什么？
使用 Tamarin 证明器进行多重集重写和基于轨迹的验证 你通过在浏览器中直接运行的动手代码来练习 Cryptology Academy，全天候 AI 导师会在你学习这节课的过程中回答你的问题。
学习 Cryptology Academy 需要有经验吗？
无需任何先前经验。CoddyKit 上的 Cryptology Academy 课程适合初学者到高级学习者，你可以从这里开始或从头开始，按照自己的节奏学习。 这是第 4 节课，共 4 节。
「Tamarin 与计算型证明」课时需要多长时间？
大多数 CoddyKit 课程大约需要 5–10 分钟。每节课都很精短且互动，所以你能稳步进步，并在网页和应用中从离开的地方继续。
我能在这节 Cryptology Academy 课中编写并运行代码吗？
能。每节 Cryptology Academy 课都包含内置代码编辑器，你可以在浏览器中直接编写并运行真实代码，并获得即时 AI 反馈 — 无需本地设置。
此课程中的所有课时
- 为何非正式证明还不够
- Dolev-Yao 攻击者模型与符号密码学
- ProVerif：自动化协议验证
- Tamarin 与计算型证明