セキュリティプロトコルの形式検証（Tamarin / ProVerif）

人手のレビューでは設計欠陥を取り逃す

暗号プリミティブが安全でも、それらを組み合わせたプロトコルには別種の欠陥が生じます。メッセージの順序、再利用、なりすまし、リフレクションといった論理的な穴です。古典的な Needham–Schroeder 公開鍵プロトコルは17年間「安全」と信じられた後、Lowe が中間者攻撃を発見しました。人間のレビューは攻撃者の組み合わせ爆発を追い切れないのです。

形式検証（formal verification）は、この探索を機械に委ねます。プロトコルと攻撃者を数学的モデルとして書き下し、「攻撃者がある秘密を知る状態」や「片方が認証成功と判断したのに相手が別人」といった到達不能であってほしい状態へ、本当に到達できないかを網羅的に調べます。到達できればそれが攻撃手順（反例）、できないと証明できれば安全性の保証です。

Dolev-Yao 攻撃者モデル：回線は攻撃者のもの

形式検証の前提となる攻撃者像が Dolev-Yao モデルです。その能力は極端に強く、しかし明確に区切られています。

要するにネットワーク＝攻撃者です。攻撃者は自分が握る知識集合から、公開された構成規則（連結・暗号化・復号は鍵を持つときのみ、など）に従って導出できるあらゆる項を作り出せます。検証ツールは「この知識集合から秘密の項を導出できるか」を、プロトコルが回せる全実行と並行して判定します。攻撃者が鍵を割れない以上、見つかる攻撃はすべてプロトコル設計そのものの論理欠陥であり、これがこのモデルの狙いです。

Tamarin：多重集合書き換えで無限セッションを扱う

Tamarin prover はプロトコルを**多重集合書き換え規則（multiset rewriting rules）**で記述します。システムの状態は「ファクト（fact）」の多重集合で、各規則が「左辺のファクトがあれば消費し、右辺のファクトを生成する」と遷移を定義します。

規則の形:   [ 左辺ファクト ] --[ アクション ]-> [ 右辺ファクト ]

例（送信者がノンスを作って暗号化送信する）:
  [ Fr(~n), !Pk($B, pkB) ]
    --[ Send($A, ~n) ]->
  [ Out( aenc(~n, pkB) ), St_A($A, ~n) ]

Fr(~n) は新鮮な乱数の生成、Out(...) は攻撃者の知識へメッセージを渡す送信、St_A(...) は参加者の内部状態を表します。--[ Send(...) ]-> のアクションは実行トレース上に記録され、安全性の主張（補題）はこのアクションの並びに対する一階論理式として書きます。たとえば秘匿性は「Secret(x) が起きたなら K(x)（攻撃者が x を知る）は決して起きない」と表現します。

Tamarin の強みは、セッション数や参加者数を有限に固定せず無限の並行実行を扱える点です。状態空間は無限になり得るため、Tamarin は後ろ向き探索と帰納的な補題を組み合わせ、必要なら人手の補助補題（helping lemma）を与えて証明を閉じます。完全自動で終わらない場合は対話的に証明木を操作できます。Diffie–Hellman の指数法則のような等式理論を組み込めるのも特徴で、鍵共有プロトコル の代数的性質をそのまま扱えます。

ProVerif：Horn 節への抽象化で速く反例を探す

ProVerif は applied pi calculus でプロトコルを記述し、内部で** Horn 節（一階の論理規則）**へ変換して解析します。攻撃者の導出可能性を「ある述語が導けるか」という論理プログラムの問題に落とし込み、解決（resolution）で判定します。

両ツールの設計思想は対照的です。

ProVerif の Horn 節抽象化は、新鮮な乱数の一意性などを意図的に緩めるため健全だが完全ではありません。すなわち「安全」と出れば本当に安全ですが、抽象化が生む偽の反例（実際には起きない攻撃）を報告することがあり、その場合は人手で精査します。一方で多くの実用プロトコルを数秒〜数分で自動判定でき、設計の反復に向きます。両ツールとも検査するのは主にトレース性質――秘匿性（攻撃者が秘密を導けない）と各種認証（後述）です。

何を検証するのか：秘匿性と対応認証

形式検証で扱う安全性は、実行トレース上の論理式として厳密に定義されます。

• 秘匿性（secrecy）：ある項が攻撃者の知識に決して入らない。前方秘匿性を見るときは、セッション後に長期鍵を攻撃者へ渡すルールを足し、それでも過去のセッション鍵が漏れないかを検査します。
• 認証（authentication）：Lowe の**対応性（agreement）**の階層で表します。弱い順に、aliveness（相手が動いていた）、weak agreement（相手も自分と通信していた）、（non-injective）agreement（やり取りした値まで一致）、そして injective agreement（さらにセッションが1対1で対応し、リプレイされていない）です。

認証の強さ（弱 → 強）
  aliveness            : 相手は確かに存在し動作した
  weak agreement       : 相手も「自分」を相手として認識していた
  non-injective agree. : 合意した鍵やノンスなどの値まで一致
  injective agreement  : 上記に加え 1 応答 1 対応（リプレイ不可）

injective agreement が崩れるとリプレイ攻撃が成立します。これらを補題として書き、ツールが反例トレース（＝具体的な攻撃シナリオ）を返すか、性質が全実行で成り立つことを証明します。証明書による相手認証の前提は 公開鍵基盤（PKI） が担い、形式モデルではしばしば「正しい公開鍵が結びつく」と理想化されます。

実例：TLS 1.3 と Signal が形式検証で鍛えられた

形式検証は学術的な道具にとどまりません。主要プロトコルの設計に直接組み込まれています。

Signal プロトコルも、X3DH とダブルラチェットが手証明と機械支援の解析で評価され、前方秘匿性と post-compromise security の主張が裏づけられています。原理の詳細は 前方秘匿性と Signal のダブルラチェット を参照してください。ほかにも 5G-AKA、Noise プロトコルフレームワーク、EMV、WireGuard、TLS のクライアント証明書再ネゴシエーション欠陥など、形式検証が実際の攻撃や設計欠陥を発見・修正した事例は枚挙にいとまがありません。

まとめ

形式検証は、プロトコルを記号モデルに落とし、Dolev-Yao 攻撃者――回線を完全支配するが暗号は割れない――が到達できる全状態を機械的に網羅探索して、秘匿性や対応認証の破れを反例として暴き出します。Tamarin は多重集合書き換えと帰納証明で無限の並行セッションと等式理論を精密に扱い、ProVerif は Horn 節抽象化で高速に自動判定します。TLS 1.3 や Signal が示すとおり、形式検証はいまや主要プロトコル設計の標準工程です。

ただし保証はモデルの内側に閉じます。計算量的な安全性は 証明可能安全性 と CryptoVerif の領域、鍵共有の代数は Diffie-Hellman、相手の身元の根拠は PKI と分担して読むと、形式検証が「何を保証し、何を保証しないか」が原理から腑に落ちます。