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プロトコルがこの手法で研究されている。