Tamarinと計算量的証明
Tamarin proverを使って、多重集合書き換えとトレースベース検証を行います。
「Tamarinと計算量的証明」はCoddyKit上の無料Cryptology Academyレッスンです。 これはレッスン4/4です。 下記で完全なレッスンを無料で読むことができます。その後、ブラウザ内の組み込みコードエディタと24時間対応の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。ブラウザー UI に証明課題が表示されます。自動戦略を誘導するか、停止しない場合には手動の手順を適用します。
計算論的健全性
記号的証明（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 は、検証の対象を実装と暗号構成にまで拡張します。
よくある質問
「Tamarinと計算量的証明」レッスンは無料ですか？
はい。「Tamarinと計算量的証明」の完全なテキストはこのウェブで無料で読めます。インタラクティブに演習し（組み込みコードエディタと24時間対応のAIチューター）、Cryptology Academyコースの残りをアンロックするには、CoddyKit PROにアップグレードしてください。 Cryptology Academyコースには全4レッスンが含まれています。
「Tamarinと計算量的証明」で何を学びますか？
Tamarin proverを使って、多重集合書き換えとトレースベース検証を行います。 ブラウザで直接実行するハンズオンコードでCryptology Academyを演習し、24時間対応のAIチューターがレッスンを進める中での質問に答えます。
Cryptology Academyを始めるのに経験は必要ですか？
事前経験は必要ありません。CoddyKitのCryptology Academyは初級者から上級者向けに構成されているため、ここから始めるか最初から始めて、自分のペースで進むことができます。 これはレッスン4/4です。
「Tamarinと計算量的証明」レッスンにはどのくらい時間がかかりますか？
ほとんどのCoddyKitレッスンは約5～10分かかります。各レッスンはコンパクトでインタラクティブなので、着実に進歩し、ウェブとアプリ全体で正確に前回の場所から再開できます。
このCryptology Academyレッスンでコードを書いて実行できますか？
はい。すべてのCryptology Academyレッスンに組み込みコードエディタが含まれているため、ブラウザでリアルコードを書いて実行し、即座のAIフィードバックを取得できます。ローカル設定は不要です。
このコースのすべてのレッスン
- 非形式的な証明だけでは不十分な理由
- Dolev-Yao攻撃者モデルと記号暗号
- ProVerif：自動プロトコル検証
- Tamarinと計算量的証明