Loading article…
| 開発者 | ブルーノ・ブランシェ |
|---|---|
| 初回リリース | 2002年6月1日 |
| 安定版リリース | 2.04 / 2021年12月1日[1] |
| 書かれた | オカムル |
| 利用可能 | 英語 |
| ライセンス | 主にGNU GPL、Windowsバイナリ、BSDライセンス |
| Webサイト | prosecco.gforge.inria.fr/personal/bblanche/proverif/ |
ProVerifは、暗号化プロトコルのセキュリティ特性について自動的に推論するソフトウェア ツールです。このツールは、Bruno Blanchet らによって開発されました。
対称および非対称暗号化、デジタル署名、ハッシュ関数、ビットコミットメント、および署名による知識証明などの暗号化プリミティブがサポートされています。このツールは、到達可能性プロパティ、対応アサーション、および観測等価性を評価することができます。これらの推論機能は、機密性と認証プロパティの分析を可能にするため、コンピューター セキュリティドメインに特に役立ちます。プライバシー、追跡可能性、検証可能性などの新しいプロパティも考慮できます。プロトコル分析は、無制限のセッション数と無制限のメッセージ スペースに関して考慮されます。このツールは攻撃の再構築が可能です。プロパティを証明できない場合、目的のプロパティを偽造する実行トレースが構築されます。
ProVerifの適用範囲
ProVerif は、実際のネットワーク プロトコルのセキュリティ分析を含む次のケース スタディで使用されています。
- アバディとブランシェット[2]は、通信アサーションを使用して認証された電子メールプロトコルを検証しました。[3]
- Abadi、Blanchet、Fournet [4]は、手動証明とProVerifの対応および同等性の証明を組み合わせて、 IPsecの鍵交換プロトコルとしてインターネット鍵交換（IKE）を置き換える候補の1つであったJust Fast Keying [ 5]プロトコルを分析しました。
- BlanchetとChaudhuri [6]は、対応アサーションを使用して信頼できないストレージ上のPlutusファイルシステム[7]の整合性を研究し、その結果、初期システムの弱点を発見し、その後修正しました。
- Bhargavanら[8] [9] [10]はProVerifを使用してF#で記述された暗号化プロトコルの実装を分析しており、特にトランスポート層セキュリティ(TLS)プロトコルがこの方法で研究されています。
- ChenとRyan [11]は、広く導入されているハードウェアチップであるTrusted Platform Module （TPM）の認証プロトコルを評価し、脆弱性を発見しました。
- Delaune、Kremer & Ryan [12] [13]とBackes、Hritcu & Maffei [14]は、観測等価性を用いて電子投票のプライバシー特性を形式化し、分析した。
- Delaune、Ryan & Smyth [15]とBackes、Maffei & Unruh [16]は、観測等価性を用いて信頼できるコンピューティングスキームである直接匿名証明（DAA）の匿名性特性を分析している。
- KustersとTruderung [17] [18]は、Diffie-Hellman指数計算とXORを使用したプロトコルを研究している。
- Smyth、Ryan、Kremer、Kourjieh [19]は、到達可能性を用いた電子投票の検証可能性を形式化し、分析した。
- Google [20]はトランスポート層プロトコルALTSを検証した。
- Sardarら[21] [22]はIntel SGXのリモート認証プロトコルを検証した。
さらなる例はオンラインで見つけることができます：[1]。
代替案
代替分析ツールには、AVISPA (到達可能性と対応アサーション用)、KISS (静的等価性用)、YAPA (静的等価性用) などがあります。計算モデルにおける多項式時間攻撃者に対するセキュリティの検証にはCryptoVerif を使用します。Tamarin Prover はProVerif の最新の代替ツールであり、Diffie-Hellman 方程式推論と観測等価性プロパティの検証を強力にサポートします。
参考文献
- ^ 新リリース: ProVerif 2.04 - コミュニティ - OCaml
- ^ Abadi, Martín; Blanchet, Bruno (2005). 「認証済み電子メールのプロトコルのコンピュータ支援検証」.コンピュータプログラミングの科学. 58 (1–2): 3–27. doi : 10.1016/j.scico.2005.02.002 .
- ^ Abadi, Martín; Glew, Neal (2002)。「軽量オンラインの信頼できる第三者による認証メール」。第11回国際ワールド ワイド ウェブ会議議事録。WWW '02。ニューヨーク、ニューヨーク、米国: ACM。pp. 387–395。doi :10.1145/511446.511497。ISBN 978-1581134490. S2CID 9035150。
- ^ Abadi, Martín; Blanchet, Bruno; Fournet , Cédric ( 2007年7 月)。「円周率計算における高速キー入力」。ACM Transactions on Information and System Security。10 ( 3): 9–es。CiteSeerX 10.1.1.3.3762。doi : 10.1145 /1266977.1266978。ISSN 1094-9224。S2CID 2371806 。
- ^ Aiello, William; Bellovin, Steven M.; Blaze, Matt; Canetti, Ran; Ioannidis, John; Keromytis, Angelos D.; Reingold, Omer (2004 年 5 月)。「Just Fast Keying: 敵対的なインターネットでの鍵の合意」。ACM Transactions on Information and System Security。7 (2): 242–273。doi : 10.1145 /996943.996946。ISSN 1094-9224。S2CID 14442788 。
- ^ Blanchet, B.; Chaudhuri, A. (2008 年 5 月)。「信頼できないストレージ 上での安全なファイル共有プロトコルの自動形式分析」。2008 IEEE セキュリティとプライバシーに関するシンポジウム (Sp 2008) 。pp . 417–431。CiteSeerX 10.1.1.362.4343。doi : 10.1109/ SP.2008.12。ISBN 978-0-7695-3168-7. S2CID 6736116。
- ^ Kallahalla, Mahesh; Riedel, Erik; Swaminathan, Ram; Wang, Qian; Fu, Kevin (2003)。「Plutus: 信頼できないストレージでのスケーラブルで安全なファイル共有」。第 2 回 USENIX ファイルおよびストレージ テクノロジ カンファレンスの議事録。FAST '03: 29–42。
- ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D. (2006-09-08). 「WS-Security プロトコルの検証済みリファレンス実装」。Webサービスと形式手法。コンピュータ サイエンスの講義ノート。第 4184 巻。Springer、ベルリン、ハイデルベルク。pp . 88–106。CiteSeerX 10.1.1.61.3389。doi :10.1007 / 11841197_6。ISBN 9783540388623。
- ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Swamy, Nikhil (2008). 「情報カード連合アイデンティティ管理プロトコルの検証済み実装」。情報、コンピュータ、通信セキュリティに関する 2008 ACM シンポジウム議事録。ASIACCS '08。ニューヨーク、ニューヨーク、米国: ACM。pp. 123–135。doi : 10.1145 / 1368310.1368330。ISBN 9781595939791. S2CID 6821014。
- ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Tse, Stephen (2008 年 12 月). 「検証済みのセキュリティ プロトコルの相互運用可能な実装」. ACM Transactions on Programming Languages and Systems . 31 (1): 5:1–5:61. CiteSeerX 10.1.1.187.9727 . doi :10.1145/1452044.1452049. ISSN 0164-0925. S2CID 14018835.
- ^ Chen, Liqun; Ryan, Mark (2009-11-05). 「TCG TPM の共有認証データに対する攻撃、解決策、検証」。セキュリティと信頼の形式的側面。コンピュータサイエンスの講義ノート。第 5983 巻。Springer、ベルリン、ハイデルベルク。pp . 201–216。CiteSeerX 10.1.1.158.2073。doi : 10.1007 / 978-3-642-12459-4_15。ISBN 9783642124587。
- ^ Delaune, Stéphanie; Kremer, Steve; Ryan, Mark (2009-01-01). 「電子投票プロトコルのプライバシー型プロパティの検証」. Journal of Computer Security . 17 (4): 435–487. CiteSeerX 10.1.1.142.1731 . doi :10.3233/jcs-2009-0340. ISSN 0926-227X.
- ^ Kremer, Steve; Ryan, Mark (2005-04-04). 「応用円周率計算における電子投票プロトコルの分析」。プログラミング言語とシステム。コンピュータサイエンスの講義ノート。第 3444 巻。Springer、ベルリン、ハイデルベルク。pp. 186–200。doi : 10.1007 /978-3-540-31987-0_14。ISBN 9783540254355。
- ^ Backes, M.; Hritcu, C.; Maffei, M. (2008 年 6 月 ) 。「応用円周率計算におけるリモート電子投票プロトコルの自動検証」。2008年21 回 IEEE コンピュータ セキュリティ基盤シンポジウム。pp. 195–209。CiteSeerX 10.1.1.612.2408。doi :10.1109/ CSF.2008.26。ISBN 978-0-7695-3182-3.S2CID 15189878 。
- ^ Delaune, Stéphanie; Ryan, Mark; Smyth, Ben (2008-06-18). 「応用π計算におけるプライバシー特性の自動検証」。Trust Management II。 IFIP – 国際情報処理連盟。 Vol. 263。 Springer、ボストン、MA。 pp. 263–278。doi :10.1007/978-0-387-09428-1_17。ISBN 9780387094274。
- ^ Backes, M.; Maffei, M.; Unruh, D. (2008 年 5 月)。「応用円周率計算におけるゼロ知識と直接匿名認証プロトコルの自動検証」。2008 IEEEセキュリティおよびプライバシーシンポジウム (Sp 2008)。pp. 202–215。CiteSeerX 10.1.1.463.489。doi : 10.1109 / SP.2008.23。ISBN 978-0-7695-3168-7. S2CID 651680。
- ^ Küsters, R.; Truderung, T. ( 2009年7 月)。「ProVerif を使用した Diffie-Hellman 指数によるプロトコルの分析」。2009年 22 回 IEEE コンピュータ セキュリティ基盤シンポジウム。pp . 157–171。CiteSeerX 10.1.1.667.7130。doi : 10.1109/CSF.2009.17。ISBN 978-0-7695-3712-2.S2CID 14185888 。
- ^ Küsters, Ralf; Truderung, Tomasz (2011-04-01). 「ホーン理論に基づくアプローチにおける XOR を使用したプロトコル分析の XOR フリーケースへの縮小」Journal of Automated Reasoning . 46 (3–4): 325–352. arXiv : 0808.0634 . doi :10.1007/s10817-010-9188-8. ISSN 0168-7433. S2CID 7597742.
- ^ Kremer, Steve; Ryan, Mark; Smyth, Ben (2010-09-20). 「電子投票プロトコルにおける選挙の検証可能性」。コンピュータセキュリティ – ESORICS 2010 。コンピュータ サイエンスの講義ノート。第 6345 巻。Springer、ベルリン、ハイデルベルク。pp . 389–404。CiteSeerX 10.1.1.388.2984。doi : 10.1007 /978-3-642-15497-3_24。ISBN 9783642154966。
- ^ 「アプリケーション層トランスポート セキュリティ | ドキュメント」。Google Cloud。
- ^ Sardar, Muhammad Usama; Quoc, Do Le; Fetzer, Christof (2020年8月)。「Intel SGXにおけるEnhanced Privacy ID (EPID)ベースのリモート認証の形式化に向けて」。2020年第23回Euromicroデジタルシステムデザイン会議(DSD)。クラーニ、スロベニア：IEEE。pp. 604–607。doi ：10.1109/ DSD51259.2020.00099。ISBN 978-1-7281-9535-3. S2CID 222297511。
- ^ Sardar, Muhammad Usama; Faqeh, Rasha; Fetzer, Christof (2020). 「Intel SGX データセンター構成証明プリミティブの形式的基盤」。Lin, Shang-Wei; Hou, Zhe; Mahony, Brendan (編)。形式手法とソフトウェアエンジニアリング。コンピューターサイエンスの講義ノート。第 12531 巻。Cham: Springer International Publishing。pp. 268–283。doi : 10.1007 /978-3-030-63406-3_16。ISBN 978-3-030-63406-3. S2CID 229344923。
外部リンク
- 公式サイト