ProVerif
ProVerif
開発者ブルーノ・ブランシェ
初回リリース2002年6月1日 （2002年6月1日）
安定版リリース
2.04 / 2021年12月1日[ 1 ] ( 2021-12-01 )
言語OCaml
利用可能な言語英語
ライセンス主にGNU GPL、Windowsバイナリ、BSDライセンス
ウェブサイトprosecco .gforge .inria .fr /personal /bblanche /proverif /

ProVerifは、暗号プロトコルのセキュリティ特性について自動推論を行うソフトウェアツールです。このツールは、Bruno Blanchetらによって開発されました。

対称暗号・非対称暗号、デジタル署名、ハッシュ関数、ビットコミットメント、署名知識証明といった暗号プリミティブをサポートしています。このツールは、到達可能性特性、対応アサーション、観測等価性を評価することができます。これらの推論機能は、機密性と認証特性の分析を可能にするため、コンピュータセキュリティ分野で特に有用です。プライバシー、追跡可能性、検証可能性といった新たな特性も考慮できます。プロトコル分析は、無制限のセッション数と無制限のメッセージ空間を前提としています。このツールは攻撃の再現機能も備えています。ある特性が証明できない場合、その特性を偽造する実行トレースを構築します。

ProVerifの適用性

ProVerifは、実際のネットワークプロトコルのセキュリティ分析を含む以下のケーススタディで使用されています

さらなる例はオンラインで見つけることができます: [1]。

代替手段

代替分析ツールには、AVISPA（到達可能性と対応アサーション用）、KISS（静的同値性用）、YAPA（静的同値性用）などがあります。計算モデルにおける多項式時間攻撃者に対するセキュリティ検証用のCryptoVerif。Tamarin ProverはProVerifの現代的な代替手段であり、Diffie-Hellman方程式推論と観測同値性の検証を優れた形でサポートしています

参考資料

  1. ^新リリース：ProVerif 2.04 - コミュニティ - OCaml
  2. ^ Abadi, Martín; Blanchet, Bruno (2005). 「認証メールプロトコルのコンピュータ支援検証」 . 『コンピュータプログラミングの科学』 . 58 ( 1–2 ): 3–27 . doi : 10.1016/j.scico.2005.02.002 .
  3. ^アバディ、マルティン、グリュー、ニール (2002). 「軽量オンラインの信頼できる第三者による認証メール」.第11回国際ワールドワイドウェブ会議議事録. WWW '02. ニューヨーク、ニューヨーク州、米国: ACM. pp.  387– 395. doi : 10.1145/511446.511497 . ISBN 978-1581134490. S2CID  9035150 .
  4. ^アバディ、マルティン、ブランシェ、ブルーノ、フルネ、セドリック（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   
  5. ^ 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 .  
  6. ^ Blanchet, B.; Chaudhuri, A. (2008年5月). 「信頼できないストレージ上での安全なファイル共有プロトコルの自動形式分析」. 2008 IEEE Symposium on Security and Privacy (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 .
  7. ^ Kallahalla, Mahesh; Riedel, Erik; Swaminathan, Ram; Wang, Qian; Fu, Kevin (2003). 「Plutus：信頼できないストレージ上でのスケーラブルで安全なファイル共有」 .第2回USENIXファイルおよびストレージ技術会議議事録. FAST '03: 29–42
  8. ^ 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.
  9. ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Swamy, Nikhil (2008). 「情報カード連携ID管理プロトコルの検証済み実装」. 2008 ACM 情報・コンピュータ・通信セキュリティシンポジウム議事録. ASIACCS '08. ニューヨーク、ニューヨーク州、米国: ACM. pp.  123– 135. doi : 10.1145/1368310.1368330 . ISBN 9781595939791. S2CID  6821014 .
  10. ^ 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   
  11. ^ 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.
  12. ^ステファニー・ドローヌ、スティーブ・クレマー、マーク・ライアン (2009年1月1日). 「電子投票プロトコルのプライバシー型特性の検証」.コンピュータセキュリティジャーナル. 17 (4): 435–487 . CiteSeerX 10.1.1.142.1731 . doi : 10.3233/jcs-2009-0340 . ISSN 0926-227X  
  13. ^クレマー, スティーブ; ライアン, マーク (2005-04-04). 「応用円周率計算による電子投票プロトコルの分析」.プログラミング言語とシステム. コンピュータサイエンス講義ノート. 第3444巻. シュプリンガー, ベルリン, ハイデルベルク. pp.  186– 200. doi : 10.1007/978-3-540-31987-0_14 . ISBN 9783540254355.
  14. ^ 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 .
  15. ^ステファニー・ドローヌ、マーク・ライアン、ベン・スミス (2008-06-18). 「応用円周率計算におけるプライバシー特性の自動検証」.信頼管理 II . IFIP – 国際情報処理連盟. 第263巻. Springer, Boston, MA. pp.  263– 278. doi : 10.1007/978-0-387-09428-1_17 . ISBN 9780387094274.
  16. ^ Backes, M.; Maffei, M.; Unruh, D. (2008年5月). 「応用π計算におけるゼロ知識と直接匿名認証プロトコルの自動検証」. 2008 IEEE Symposium on Security and Privacy (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 .
  17. ^ 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 .
  18. ^ 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  
  19. ^クレマー, スティーブ; ライアン, マーク; スミス, ベン (2010-09-20). 「電子投票プロトコルにおける選挙の検証可能性」.コンピュータセキュリティ – ESORICS 2010 . コンピュータサイエンス講義ノート. 第6345巻. シュプリンガー, ベルリン, ハイデルベルク. pp.  389– 404. CiteSeerX 10.1.1.388.2984 . doi : 10.1007/978-3-642-15497-3_24 . ISBN  9783642154966.
  20. ^ 「アプリケーション層トランスポートセキュリティ | ドキュメント」Google Cloud
  21. ^ 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 .
  22. ^ Sardar, Muhammad Usama; Faqeh, Rasha; Fetzer, Christof (2020). 「Intel SGXデータセンター構成証明プリミティブの形式的基礎」 . Lin, Shang-Wei; Hou, Zhe; Mahony, Brendan (編).形式手法とソフトウェア工学. コンピュータサイエンス講義ノート. 第12531巻. 出版社: Springer International Publishing. pp.  268– 283. doi : 10.1007/978-3-030-63406-3_16 . ISBN 978-3-030-63406-3. S2CID  229344923 .
「 https://en.wikipedia.org/w/index.php?title=ProVerif&oldid=1332168027」より取得