ProVerifの適用例
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/02/22 09:49 UTC 版)
「ProVerif」の記事における「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プロトコルを検証した。 他にも多くの利用例がある 。
※この「ProVerifの適用例」の解説は、「ProVerif」の解説の一部です。
「ProVerifの適用例」を含む「ProVerif」の記事については、「ProVerif」の概要を参照ください。
- ProVerifの適用例のページへのリンク
