ProVerifは、暗号化プロトコルの安全性要件に関する自動推論を行うソフトウェアツールであり、ブルーノ ブランシェットによって開発された。
対称と非対称暗号、デジタル署名、ハッシュ関数、ビットコミットメント、知識の証明などの暗号化プリミティブがサポートされている。このツールは、到達可能性(reachability)、対応表明(correspondence assertions)、および観測等価性(observational equivalence)を評価することができる。これらの推論機能は、機密性や認証機能の分析を可能にするため、コンピュータセキュリティにおいて特に役立つ。プライバシー、追跡可能性、検証可能性などの新たな性質も解析することができる。プロトコル分析では、無限個のセッションと無限大のメッセージ空間が考慮される。このツールは攻撃の再構築が可能である。つまり、ある特性を持つことが証明できない場合には、その特性を破る実行を得ることができる。
ProVerifの適用例
ProVerifは、以下に示すような、実際のネットワークプロトコルのセキュリティ分析などのケーススタディで使用されている。
AbadiとBlanchet は、対応表明を使用して、certified emailプロトコルを検証した。 Abadi、Blanchet、Fournet は、IPsecの鍵交換プロトコルであるInternet Key Exchange （IKE）に代わる候補の1つであるJust Fast Keying プロトコルを、手動の証明とProVerifの対応性と等価性を組み合わせて分析した。 BlanchetとChaudhuri は、対応表明を使用して、信頼できないストレージでのPlutusファイルシステムの完全性を調査し、初期システムの弱点を発見してこれを修正した。 Bhargavanら はF Sharp（プログラミング言語）で記述された暗号化プロトコル実装を分析するのにProVerifを使用している。特に、TLSプロトコルがこの手法で研究されている。 ChenとRyan は、広く展開されているハードウェアチップであるTrusted Platform Module （TPM）にある認証プロトコルを評価し、脆弱性を発見した。 Delaune、Kremer、Ryan およびBackes、Hritcu、Maffei は、観測等価性を使用して、電子投票のプライバシーを形式化し分析している。 Delaune、Ryan、Smyth およびBackes、Maffei、Unruh は、観測等価性を使用して、信頼できるコンピューティングスキームである直接匿名認証（DAA）の匿名性を解析している。 KustersとTruderung は、Diffie-Hellmanの指数とXORを使用したプロトコルを調べている。 Smyth、Ryan、Kremer、およびKourjieh は、到達可能性を使用して、電子投票の検証可能性を形式化し分析している。 Google は、トランスポート層プロトコルALTSを検証した。 Sardarら は、インテルSGX リモートattestationプロトコルを検証した。
他にも多くの利用例がある 。
類似した検証ツール
脚注
参考文献