非形式的な証明だけでは不十分な理由

プロトコル設計者は、攻撃者が成功できない理由を文章で説明する、非形式的なセキュリティ議論を日常的に作成します。しかし歴史が示すように、専門家が設計したプロトコルでさえ、こうした議論は頻繁に誤っています。

Needham-Schroeder（1978）は相互認証のために設計されました。1995年、Gavin Loweは自動検証を使って中間者攻撃を発見しました。発表から17年後のことです。非形式的な証明では、巧妙なリプレイ攻撃を見落としていました。

WEPは非形式的なセキュリティ主張とともに、1997年にIEEEで承認されました。2001年までに、研究者はRC4キーストリームの再利用、IVの衝突、完全性保護の欠如を発見し、数分でWEPを破れることを示しました。非形式的な推論では、そのすべてを見落としていました。

プロトコルのセキュリティは、多数の同時セッション、能動的な攻撃者、暗号学的な仮定の相互作用に依存します。人間の推論では、状態の爆発や、同時実行が入り交じる状況を扱うのは困難です。

形式手法はプロトコルを数学的にモデル化し、設計者が想定したものだけでなく、攻撃者が取り得るすべての戦略について、セキュリティ特性（秘匿性、認証、前方秘匿性）を証明または反証します。

記号モデル（Dolev-Yao）：暗号を完全なブラックボックスとして扱い、プロトコルの論理に焦点を当てます。計算モデル：実際の確率的なセキュリティゲームを扱い、現実世界の保証により近いモデルです。どちらも実際のバグを発見できます。

POODLE（2014）は、SSL 3.0のCBCにあるパディングオラクルを悪用しました。この脆弱性は実装のバグではなく、プロトコルレベルの設計上の欠陥でした。SSL 3.0の仕様を形式解析していれば、デプロイ前にこのオラクルを発見できたはずです。

TLS 1.3（RFC 8446）は、ProVerifとmiTLSを使った形式解析と並行して設計されました。仕様は形式解析の結果に基づいて改訂されました。これは標準化団体が形式手法を採用した画期的な出来事です。

形式ツールが検証するのはプロトコルモデルであり、実装ではありません。形式検証済みのプロトコルでも、実装が安全であるとは限りません。F*／HACL*は、暗号コード自体にも検証を拡張します。

形式検証にはコストがかかります。プロトコルのモデル化には数週間かかり、専門的な知識も必要です。しかしTLS、SSH、Signalのような価値の高い対象では、そのコストは正当化されます。1つのプロトコル上の欠陥が、数十億人のユーザーに影響する可能性があるためです。

Loweによる1995年のNeedham-Schroeder攻撃の発見が重要だったのはなぜですか？

非形式的な証明が失敗するのは、人間の推論では同時セッション間の相互作用や攻撃者の戦略を見落とすためです。Needham-Schroeder、WEP、POODLEはいずれも非形式的なセキュリティ議論に基づいていました。TLS 1.3では、設計中に形式解析が取り入れられました。形式ツールは、デプロイ前にプロトコルレベルのバグを発見します。