ProVerif：自動プロトコル検証
ProVerifでTLSハンドシェイクの性質を記述し、検証します。
「ProVerif：自動プロトコル検証」はCoddyKit上の無料Cryptology Academyレッスンです。 これはレッスン3/4です。 下記で完全なレッスンを無料で読むことができます。その後、ブラウザ内の組み込みコードエディタと24時間対応のAIチューターでハンズオン演習できます。 これはCryptology Academy学習パスの一部であり、ウェブとCoddyKitアプリ全体で進捗が同期されます。 Cryptology Academyコースには全4レッスンが含まれています。
ProVerif とは
ProVerif（Bruno Blanchet、2001 年）は、自動暗号プロトコル検証器です。Applied Pi Calculus で記述されたプロトコルを受け取り、秘匿性と認証の特性を自動的に判定します。
ProVerif の仕組み
ProVerif はプロトコルをホーン節に変換し、解決に基づくアルゴリズムを適用して、攻撃者が何を学習できるかを導出します。秘匿性に関する事実が導出可能であればプロトコルは破られており、そうでなければ安全であることが証明されます。
ProVerif の入力言語
プロトコルは宣言的に記述します。チャネル、型、関数（enc、dec、sign、verify）、等式（dec(enc(m,k),k)=m）、およびチャネルを介して通信するプロセスを宣言します。
暗号プリミティブの宣言
ProVerif の宣言例：
(* Symmetric encryption *)
fun senc(bitstring, key): bitstring.
fun sdec(bitstring, key): bitstring.
equation forall m: bitstring, k: key; sdec(senc(m, k), k) = m.
(* Asymmetric encryption *)
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring.
equation forall m: bitstring, sk: skey; adec(aenc(m, pk(sk)), sk) = m.単純なプロトコルプロセスの記述
Alice と Bob を並列プロセスとしてモデル化します。
(* Alice sends nonce to Bob, encrypted *)
let Alice(skA: skey, pkB: pkey) =
new na: nonce;
out(c, aenc((na, pk(skA)), pkB));
in(c, m: bitstring);
let nb = adec(m, skA) in
out(c, aenc(nb, pkB)).
(* Main process: run attacker with full channel control *)
process
new skA: skey; new skB: skey;
out(c, pk(skA)); out(c, pk(skB)); (* publish public keys *)
(Alice(skA, pk(skB)) | Bob(skB, pk(skA)))セキュリティクエリの記述
ProVerif では、次のようなクエリを検証します。
(* Secrecy: attacker cannot learn na *)
query attacker(na).
(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).ProVerif の出力の解釈
ProVerif は「RESULT ... is true」（安全性が証明された）または「RESULT ... is false」を出力します。後者の場合は、攻撃者のメッセージを示す反例として攻撃トレースを出力します。このトレースから、攻撃がどのように成立するかを正確に確認できます。
ProVerif による TLS 1.3 の検証
Bhargavan ら（2016 年）は、ProVerif を使って TLS 1.3 のモデルを解析しました。0-RTT 再開メカニズムに対する攻撃を発見して報告し、この問題は RFC の最終確定前に修正されました。
限界：近似とループ
ProVerif は過近似を行います。そのため、実際には安全なプロトコルに対して偽の攻撃を報告することはありますが、実際の攻撃を見落とすことはありません。プロトコルセッション数が無制限の場合は停止しないことがあり、ProVerif はヒューリスティックにループを展開します。
ProVerif が「証明できない」と出力した場合
ProVerif が近似の範囲内で結果を判定できない場合は、「CANNOT BE PROVED」と出力します。これは安全でないことの証明ではなく、ツールがヒューリスティックによる解析能力を使い果たしたことを意味します。このような場合は Tamarin で成功する可能性があります。
理解度チェック
秘匿性クエリに対して ProVerif が「RESULT ... is false」と出力した場合、何を意味しますか。
レッスンのまとめ
ProVerif は、ホーン節の解決によってプロトコル検証を自動化します。プロトコルは、暗号の等式を含む Applied Pi Calculus で記述します。クエリでは秘匿性と認証について検証します。false は安全性が証明されたことを、true はプロトコルが破られたことを意味し、攻撃トレースが示されます。限界として、近似によって「証明できない」と出力されることがあります。
よくある質問
「ProVerif：自動プロトコル検証」レッスンは無料ですか？
はい。「ProVerif：自動プロトコル検証」の完全なテキストはこのウェブで無料で読めます。インタラクティブに演習し（組み込みコードエディタと24時間対応のAIチューター）、Cryptology Academyコースの残りをアンロックするには、CoddyKit PROにアップグレードしてください。 Cryptology Academyコースには全4レッスンが含まれています。
「ProVerif：自動プロトコル検証」で何を学びますか？
ProVerifでTLSハンドシェイクの性質を記述し、検証します。 ブラウザで直接実行するハンズオンコードでCryptology Academyを演習し、24時間対応のAIチューターがレッスンを進める中での質問に答えます。
Cryptology Academyを始めるのに経験は必要ですか？
事前経験は必要ありません。CoddyKitのCryptology Academyは初級者から上級者向けに構成されているため、ここから始めるか最初から始めて、自分のペースで進むことができます。 これはレッスン3/4です。
「ProVerif：自動プロトコル検証」レッスンにはどのくらい時間がかかりますか？
ほとんどのCoddyKitレッスンは約5～10分かかります。各レッスンはコンパクトでインタラクティブなので、着実に進歩し、ウェブとアプリ全体で正確に前回の場所から再開できます。
このCryptology Academyレッスンでコードを書いて実行できますか？
はい。すべてのCryptology Academyレッスンに組み込みコードエディタが含まれているため、ブラウザでリアルコードを書いて実行し、即座のAIフィードバックを取得できます。ローカル設定は不要です。
このコースのすべてのレッスン
- 非形式的な証明だけでは不十分な理由
- Dolev-Yao攻撃者モデルと記号暗号
- ProVerif：自動プロトコル検証
- Tamarinと計算量的証明