ProVerif
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プロトコルを検証した。
他にも多くの利用例がある 。
ProVerifは、暗号化プロトコルの安全性要件に関する自動推論を行うソフトウェアツールであり、ブルーノ ブランシェットによって開発された。
対称と非対称暗号、デジタル署名、ハッシュ関数、ビットコミットメント、知識の証明などの暗号化プリミティブがサポートされている。このツールは、到達可能性(reachability)、対応表明(correspondence assertions)、および観測等価性(observational equivalence)を評価することができる。これらの推論機能は、機密性や認証機能の分析を可能にするため、コンピュータセキュリティにおいて特に役立つ。プライバシー、追跡可能性、検証可能性などの新たな性質も解析することができる。プロトコル分析では、無限個のセッションと無限大のメッセージ空間が考慮される。このツールは攻撃の再構築が可能である。つまり、ある特性を持つことが証明できない場合には、その特性を破る実行を得ることができる。