ProVerif

ProVerif
ProVerif
개발자브루노 블랑쉐
초기 릴리즈2002년 6월 1일 (2002-06-01)
안정된 릴리스
2.03 / 2021년9월 10일 (2021-09-10)[1]
기입처OCaml
이용가능기간:영어
면허증.주로 GNU GPL, Windows 바이너리, BSD 라이선스
웹 사이트prosecco.gforge.inria.fr/personal/bblanche/proverif/

ProVerif는 암호화 프로토콜에서 발견되는 보안 속성에 대한 자동 추론을 위한 소프트웨어 도구입니다.이 도구는 Bruno Blanchet에 의해 개발되었습니다.

대칭 및 비대칭 암호화, 디지털 서명, 해시 함수, 비트 커밋, 시그니처 지식 증명 등의 암호 원형을 지원합니다.이 도구는 도달 가능성 특성, 대응 어설션 및 관찰 동등성을 평가할 수 있다.이러한 추론 기능은 기밀성 및 인증 속성을 분석할 수 있으므로 컴퓨터 보안 도메인에 특히 유용합니다.프라이버시, 추적성 및 검증성과 같은 새로운 특성도 고려할 수 있다.프로토콜 분석은 무제한 세션 수 및 무제한 메시지 공간에 대해 고려됩니다.이 도구는 재구성을 공격할 수 있습니다.속성을 증명할 수 없는 경우 원하는 속성을 위조하는 실행 트레이스가 구축됩니다.

ProVerif 적용 가능성

ProVerif는 실제 네트워크 프로토콜의 보안 분석을 포함한 다음과 같은 사례 연구에서 사용되고 있습니다.

  • Abadi & Blanchet은[2] 통신 어설션을 사용하여 인증 이메일 [3]프로토콜을 검증했습니다.
  • Abadi, Blanchet 및 Fournet은[4] IPsec의 키 교환 프로토콜로서 Internet Key Exchange(IKE; 인터넷 키 교환)를 대체할 후보 중 하나인 Just[5] Fast Keying 프로토콜을 수동 증명과 일치 및 동등 증명과 조합하여 분석합니다.
  • Blanchet & Chaudhuri는[6] 대응 어설션을 사용하여 신뢰할 수 없는 스토리지 상의 Flutus 파일[7] 시스템의 무결성을 연구하여 초기 시스템의 약점을 발견하여 수정하였습니다.
  • 바르가반 [8][9][10]외ProVerif를 사용하여 F Sharp(프로그래밍 언어)로 작성된 암호화 프로토콜 구현을 분석합니다. 특히 TLS(Transport Layer Security) 프로토콜은 이러한 방식으로 연구되었습니다.
  • Chen과[11] Ryan은 널리 도입된 하드웨어 칩인 Trusted Platform Module(TPM)에서 발견된 인증 프로토콜을 평가하여 취약성을 발견했습니다.
  • 델라우네, 크레머, 라이언[12][13], 백스, Hritcu, 마페이[14] 등은 관찰적 등가성을 사용하여 전자투표의 프라이버시 속성을 공식화하고 분석합니다.
  • Dellaune, Ryan & Smyth[15] 및 Backes, Mafei & Unruh는[16] 관찰적 등가성을 사용하여 신뢰할 수 있는 컴퓨팅 스킴의 익명성 특성을 분석합니다.
  • Kusters & Truderung은[17][18] Diffie-Hellman 확장 및 XOR을 사용하여 프로토콜을 검사합니다.
  • Smyth, Ryan, Kremer 및 Kourjieh는[19] 도달 가능성을 이용하여 전자 투표의 검증 가능성 속성을 공식화하고 분석한다.
  • 구글은[20] 자사의 트랜스포트층 프로토콜 ALTS를 검증했다.
  • Sardar [21][22]등인텔 SGX의 리모트 증명 프로토콜을 확인.

자세한 예는 [1]에서 확인할 수 있습니다.


대체 수단

대체 분석 도구로는 AVISPA(도달 가능성 및 대응 어설션용), KISS(정적 등가용), YAPA(정적 등가용) 등이 있습니다.CryptoVerif는 계산 모델의 다항 시간 적에 대한 보안을 검증합니다.Tamarin Prover는 ProVerif의 현대적인 대안으로, Diffie-Hellman 등가 추론과 관찰 등가성 검증에 탁월한 지원을 제공한다.

레퍼런스

  1. ^ 새로운 릴리즈:ProVerif 2.03 - 커뮤니티 - OCaml
  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. Proceedings of the 11th International Conference on World Wide Web. WWW '02. New York, NY, USA: ACM. pp. 387–395. doi:10.1145/511446.511497. ISBN 978-1581134490. S2CID 9035150.
  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. 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 (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. S2CID 14442788.
  6. ^ Blanchet, B.; Chaudhuri, A. (May 2008). Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage. 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: Scalable Secure File Sharing on Untrusted Storage". Proceedings of the 2Nd USENIX Conference on File and Storage Technologies. FAST '03: 29–42.
  8. ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D. (2006-09-08). Verified Reference Implementations of WS-Security Protocols. Web Services and Formal Methods. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. 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). Verified Implementations of the Information Card Federated Identity-management Protocol. Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security. ASIACCS '08. New York, NY, USA: ACM. pp. 123–135. doi:10.1145/1368310.1368330. ISBN 9781595939791. S2CID 6821014.
  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. CiteSeerX 10.1.1.187.9727. doi:10.1145/1452044.1452049. ISSN 0164-0925. S2CID 14018835.
  11. ^ Chen, Liqun; Ryan, Mark (2009-11-05). Attack, Solution and Verification for Shared Authorisation Data in TCG TPM. Formal Aspects in Security and Trust. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. pp. 201–216. CiteSeerX 10.1.1.158.2073. 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. CiteSeerX 10.1.1.142.1731. 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. Programming Languages and Systems. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. pp. 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. 2008 21st IEEE Computer Security Foundations Symposium. pp. 195–209. CiteSeerX 10.1.1.612.2408. doi:10.1109/CSF.2008.26. ISBN 978-0-7695-3182-3. S2CID 15189878.
  15. ^ Delaune, Stéphanie; Ryan, Mark; Smyth, Ben (2008-06-18). Automatic Verification of Privacy Properties in the Applied pi Calculus. Trust Management II. IFIP – The International Federation for Information Processing. Springer, Boston, MA. pp. 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. 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. (July 2009). Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation. 2009 22nd IEEE Computer Security Foundations Symposium. 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). "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. S2CID 7597742.
  19. ^ Kremer, Steve; Ryan, Mark; Smyth, Ben (2010-09-20). Election Verifiability in Electronic Voting Protocols. Computer Security – ESORICS 2010. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. pp. 389–404. CiteSeerX 10.1.1.388.2984. doi:10.1007/978-3-642-15497-3_24. ISBN 9783642154966.
  20. ^ "Application Layer Transport Security Documentation". Google Cloud.
  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. S2CID 222297511.
  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. Lecture Notes in Computer Science. Cham: Springer International Publishing. 12531: 268–283. doi:10.1007/978-3-030-63406-3_16. ISBN 978-3-030-63406-3. S2CID 229344923.

외부 링크