ProVerif

リンクを編集
出典: フリー百科事典『ウィキペディア（Wikipedia）』
ProVerif
開発元 Bruno Blanchet
初版 2002年6月1日 (2002-06-01)
最新版
2.03 / 2021年9月10日 (2年前) (2021-09-10)[1]
プログラミング
言語		 OCaml
対応言語 English
ライセンス Mainly, GNU GPL; Windows binaries, BSD licenses
公式サイト prosecco.gforge.inria.fr/personal/bblanche/proverif/
テンプレートを表示

ProVerifは、暗号化プロトコルの安全性要件に関する自動推論を行うソフトウェアツールであり、ブルーノ ブランシェットによって開発された。

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

ProVerifの適用例[編集]

ProVerifは、以下に示すような、実際のネットワークプロトコルのセキュリティ分析などのケーススタディで使用されている。

  • AbadiとBlanchet [2]は、対応表明を使用して、certified emailプロトコルを検証した。 [3]
  • Abadi、Blanchet、Fournet [4]は、IPsecの鍵交換プロトコルであるInternet Key Exchange （IKE）に代わる候補の1つであるJust Fast Keying [5]プロトコルを、手動の証明とProVerifの対応性と等価性を組み合わせて分析した。
  • BlanchetとChaudhuri [6]は、対応表明を使用して、信頼できないストレージでのPlutusファイルシステム[7]の完全性を調査し、初期システムの弱点を発見してこれを修正した。
  • Bhargavanら[8] [9] [10]はF Sharp（プログラミング言語）で記述された暗号化プロトコル実装を分析するのにProVerifを使用している。特に、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]は、インテルSGX リモートattestationプロトコルを検証した。

他にも多くの利用例がある [1]。


類似した検証ツール[編集]

脚注[編集]

  1. ^ https://discuss.ocaml.org/t/new-release-proverif-2-03/8463
  2. ^ Abadi, Martín; Blanchet, Bruno (2005). “Computer-assisted verification of a protocol for certified email”. Science of Computer Programming 58 (1–2): 3–27. doi:10.1016/j.scico.2005.02.002. 
  3. ^ Abadi, Martín; Glew, Neal (2002). Certified Email with a Light On-line Trusted Third Party: Design and Implementation. WWW '02. New York, NY, USA: ACM. 387–395. doi:10.1145/511446.511497. ISBN 978-1581134490 
  4. ^ Abadi, Martín; Blanchet, Bruno; Fournet, Cédric (July 2007). “Just Fast Keying in the Pi Calculus”. ACM Transactions on Information and System Security 10 (3): 9–es. doi:10.1145/1266977.1266978. ISSN 1094-9224. 
  5. ^ Aiello, William; Bellovin, Steven M.; Blaze, Matt; Canetti, Ran; Ioannidis, John; Keromytis, Angelos D.; Reingold, Omer (May 2004). “Just Fast Keying: Key Agreement in a Hostile Interne”. ACM Transactions on Information and System Security 7 (2): 242–273. doi:10.1145/996943.996946. ISSN 1094-9224. 
  6. ^ Blanchet, B.; Chaudhuri, A. (May 2008). Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage. 417–431. doi:10.1109/SP.2008.12. ISBN 978-0-7695-3168-7 
  7. ^ Kallahalla, Mahesh; Riedel, Erik; Swaminathan, Ram; Wang, Qian; Fu, Kevin (2003). “Plutus: Scalable Secure File Sharing on Untrusted Storage”. Proceedings of the 2Nd USENIX Conference on File and Storage Technologies: 29–42. http://dl.acm.org/citation.cfm?id=1090694.1090698. 
  8. ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D. (2006-09-08) (英語). Verified Reference Implementations of WS-Security Protocols. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. 88–106. doi:10.1007/11841197_6. ISBN 9783540388623 
  9. ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Swamy, Nikhil (2008). Verified Implementations of the Information Card Federated Identity-management Protocol. ASIACCS '08. New York, NY, USA: ACM. 123–135. doi:10.1145/1368310.1368330. ISBN 9781595939791 
  10. ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Tse, Stephen (December 2008). “Verified Interoperable Implementations of Security Protocols”. ACM Transactions on Programming Languages and Systems 31 (1): 5:1–5:61. doi:10.1145/1452044.1452049. ISSN 0164-0925. 
  11. ^ Chen, Liqun; Ryan, Mark (2009-11-05) (英語). Attack, Solution and Verification for Shared Authorisation Data in TCG TPM. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. 201–216. doi:10.1007/978-3-642-12459-4_15. ISBN 9783642124587 
  12. ^ Delaune, Stéphanie; Kremer, Steve; Ryan, Mark (2009-01-01). “Verifying privacy-type properties of electronic voting protocols” (英語). Journal of Computer Security 17 (4): 435–487. doi:10.3233/jcs-2009-0340. ISSN 0926-227X. 
  13. ^ Kremer, Steve; Ryan, Mark (2005-04-04) (英語). Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. 186–200. doi:10.1007/978-3-540-31987-0_14. ISBN 9783540254355 
  14. ^ Backes, M.; Hritcu, C.; Maffei, M. (June 2008). Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus. 195–209. doi:10.1109/CSF.2008.26. ISBN 978-0-7695-3182-3 
  15. ^ Delaune, Stéphanie; Ryan, Mark; Smyth, Ben (2008-06-18) (英語). Automatic Verification of Privacy Properties in the Applied pi Calculus. IFIP – The International Federation for Information Processing. Springer, Boston, MA. 263–278. doi:10.1007/978-0-387-09428-1_17. ISBN 9780387094274 
  16. ^ Backes, M.; Maffei, M.; Unruh, D. (May 2008). Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol. 202–215. doi:10.1109/SP.2008.23. ISBN 978-0-7695-3168-7 
  17. ^ Küsters, R.; Truderung, T. (July 2009). Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation. 157–171. doi:10.1109/CSF.2009.17. ISBN 978-0-7695-3712-2 
  18. ^ Küsters, Ralf; Truderung, Tomasz (2011-04-01). “Reducing Protocol Analysis with XOR to the XOR-Free Case in the Horn Theory Based Approach” (英語). Journal of Automated Reasoning 46 (3–4): 325–352. arXiv:0808.0634. doi:10.1007/s10817-010-9188-8. ISSN 0168-7433. 
  19. ^ Kremer, Steve; Ryan, Mark; Smyth, Ben (2010-09-20) (英語). Election Verifiability in Electronic Voting Protocols. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. 389–404. doi:10.1007/978-3-642-15497-3_24. ISBN 9783642154966 
  20. ^ “Application Layer Transport Security | Documentation” (英語). Google Cloud. 2019年11月21日閲覧。
  21. ^ Sardar, Muhammad Usama; Quoc, Do Le; Fetzer, Christof (August 2020). “Towards Formalization of Enhanced Privacy ID (EPID)-based Remote Attestation in Intel SGX”. 2020 23rd Euromicro Conference on Digital System Design (DSD) (Kranj, Slovenia: IEEE): 604–607. doi:10.1109/DSD51259.2020.00099. ISBN 978-1-7281-9535-3. https://ieeexplore.ieee.org/document/9217791. 
  22. ^ Sardar, Muhammad Usama; Faqeh, Rasha; Fetzer, Christof (2020). Lin, Shang-Wei; Hou, Zhe; Mahony, Brendan. eds. “Formal Foundations for Intel SGX Data Center Attestation Primitives” (英語). Formal Methods and Software Engineering (Cham: Springer International Publishing) 12531: 268–283. doi:10.1007/978-3-030-63406-3_16. ISBN 978-3-030-63406-3. https://link.springer.com/chapter/10.1007%2F978-3-030-63406-3_16. 

参考文献[編集]

 

「https://ja.wikipedia.org/w/index.php?title=ProVerif&oldid=88182686」から取得