ProVerif users

Research papers

  1. Myrto Arapinis, Eike Ritter, and Mark D. Ryan. StatVerif: Verification of stateful processes. In 24th Computer Security Foundations Symposium (CSF'11), Cernay-la-Ville, France, June 2011. Available at http://www.cs.bham.ac.uk/~arapinmd/pdf/ARR11.pdf.
  2. Michael Backes, Catalin Hritcu, and Matteo Maffei. Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus. In Proceedings of 21st IEEE Computer Security Foundations Symposium (CSF), June 2008. Available at http://www.infsec.cs.uni-sb.de/~backes/papers/index.html
  3. Michael Backes, Matteo Maffei, and Dominique Unruh. Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol. In Proceedings of 29th IEEE Symposium on Security and Privacy, May 2008. Technical report available at http://eprint.iacr.org/2007/289.
  4. Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, and Andrew Gordon. Secure Sessions for Web Services. In 2004 ACM Workshop on Secure Web Services (SWS), Washington DC, October 29, 2004. Available at http://securing.ws/.
  5. Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, and Eugen Zalinescu. Cryptographically Verified Implementations for TLS. In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS'08), pages 459-468, October 2008. Available at http://www.msr-inria.inria.fr/projects/sec/fs2cv/index.html#tls.
  6. Karthikeyan Bhargavan, Cédric Fournet, and Andrew Gordon. Verifying Policy-Based Security for Web Services. In 2004 ACM Conference on Computer and Communications Security (CCS 2004), pp 268-277, Washington DC, October 25-29, 2004. Available at http://securing.ws/.
  7. Karthikeyan Bhargavan, Cédric Fournet, and Andrew Gordon. Verified reference implementations of WS-Security protocols. In 3rd International Workshop on Web Services and Formal Methods (WS-FM 2006), Vienna, September 8-9, 2006. Springer LNCS 4184:88-106. Available at http://securing.ws/.
  8. Karthikeyan Bhargavan, Cédric Fournet, Andrew Gordon, and Riccardo Pucella. TulaFale: A Security Tool for Web Services. In Formal Methods for Components and Objects (FMCO 2003), Springer LNCS, Revised Lecture Series, volume 3188, pages 197-222, 2004. Available at http://securing.ws/.
  9. Karthikeyan Bhargavan, Cédric Fournet, Andrew Gordon, and Nikhil Swamy. Verified implementations of the Information Card Federated Identity-Management Protocol. In ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), pages 123-135, Tokyo, Japan, March 2008. Available at http://securing.ws/.
  10. Karthikeyan Bhargavan, Cédric Fournet, Andrew Gordon, and Stephen Tse. Verified interoperable implementations of security protocols. In 19th IEEE Computer Security Foundations Workshop (CSFW 2006), pages 139-152, Venice, Italy, July 2006. IEEE Computer Society. Available at http://securing.ws/.
  11. Karthikeyan Bhargavan, Cédric Fournet, Andrew Gordon, and Stephen Tse. Verified interoperable implementations of security protocols. ACM Transactions on Programming Languages and Systems, 31(1):5, 2008. Available at http://research.microsoft.com/en-us/um/people/karthb/pubs/verified-interoperable-implementations-toplas08.pdf.
  12. Mayla Brusó, Konstantinos Chatzikokolakis and Jerry den Hartog. Formal verification of privacy for RFID systems. 23rd IEEE Computer Security Foundations Symposium, 2010. Available at http://www.win.tue.nl/~kostas/papers/rfid_privacy.pdf.
  13. Ran Canetti and Jonathan Herzog. Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). Cryptology ePrint Archive, Report 2004/334, 2004. Available at http://eprint.iacr.org/2004/334
  14. Richard Chang and Vitaly Shmatikov. Formal Analysis of Authentication in Bluetooth Device Pairing. In Proc. of LICS/ICALP Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA), Wroclaw, Poland, July 2007. Available at http://www.cs.utexas.edu/~shmat/abstracts.html#blue
  15. Liqun Chen and Mark D. Ryan. Attack, solution and verification for shared authorisation data in TCG TPM. In Proceedings of Sixth International Workshop on Formal Aspects in Security and Trust (FAST'09). LNCS, Springer, 2010. Available at http://www.cs.bham.ac.uk/~mdr/research/papers/pdf/09-FAST.pdf.
  16. Stéphanie Delaune, Steve Kremer, and Mark Ryan. Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security 17(4), pages 435-487, 2009. Available at http://www.lsv.ens-cachan.fr/~delaune/mes-publis.php?onlykey=DKR-jcs08.
  17. Stéphanie Delaune, Steve Kremer, Mark Ryan, and Graham Steel. Formal analysis of protocols based on TPM state registers. In 24th Computer Security Foundations Symposium (CSF'11), Cernay-la-Ville, France, June 2011. Available at http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKRS-csf11.pdf.
  18. Gilberto Filé and Roberto Vigo. Expressive power of definite clauses for verifying authenticity. In 22nd IEEE Computer Security Foundations Symposium (CSF'09), pages 251-265, Port Jefferson, New-York, USA, July 2009. IEEE Computer Society.
  19. Alexey Gotsman, Fabio Massacci, Marco Pistore. Towards an Independent Semantics and Verification Technology for the HLPSL Specification Language. In Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA-2005), Electronic Notes in Theoretical Computer Science, volume 135, issue 1, pages 59-77, 2005. doi:10.1016/j.entcs.2005.06.004.
  20. Himanshu Khurana and Hyung-Seok Hahm. Certified Mailing Lists. In Proceedings of the ACM Symposium on Communication, Information, Computer and Communication Security (ASIACCS'06), Taipei, Taiwan, March 2006. Available at http://www.ncsa.uiuc.edu/People/hkhurana/AsiaCCS06.pdf.
  21. Ralf Küsters and Tomasz Truderung. Reducing Protocol Analysis with XOR to the XOR-free case in the Horn Theory Based Approach. In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS'08), pages 129-138, October 2008. Available at http://www.infsec.uni-trier.de/publications_html/KuestersTruderung-CCS-2008.pdf.
  22. Ralf Küsters and Tomasz Truderung. Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation. In 22nd IEEE Computer Security Foundations Symposium (CSF'09), pages 157-171, Port Jefferson, New-York, USA, July 2009. IEEE Computer Society. Available at http://www.infsec.uni-trier.de/publications/paper/KuestersTruderung-CSF-2009.pdf.
  23. Steve Kremer and Mark D. Ryan. Analysing the vulnerability of protocols to produce known-pair and chosen-text attacks. Electronic Notes in Theoretical Computer Science -- Special Issue for CONCUR'04 Workshop on Security Issues in Coordination Models, Languages and Systems (SecCo'04), 2004. 18 pages. Available at http://www.cs.bham.ac.uk/~mdr/research/papers/index.html
  24. Steve Kremer and Mark D. Ryan. Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. In Proceedings of the European Symposium on Programming (ESOP'05), Lecture Notes in Computer Science series, volume 3444, pages 186-200, Springer Verlag, 2005. Available at http://www.cs.bham.ac.uk/~mdr/research/papers/index.html
  25. Jens Chr. Godskesen. Formal Verification of the ARAN Protocol Using the Applied Pi Calculus. In Sixth International IFIP WG 1.7 Workshop on Issues in the Theory of Security (WITS'06), 2006. Available here.
  26. Gyesik Lee, Hisashi Oguma, Akira Yoshioka, Rie Shigetomi, Akira Otsuka and Hideki Imai. Formally Verifiable Features in Embedded Vehicular Security Systems. In First IEEE Vehicular Networking Conference, VNC 2009, Tokyo. Available at http://ropas.snu.ac.kr/~gslee/Publi/vnc2009.pdf.
  27. Zhengqin Luo, Xiaojuan Cai, Jun Pang, and Yuxin Deng. Analyzing an Electronic Cash Protocol Using Applied Pi Calculus. In Applied Cryptography and Network Security, 5th International Conference, ACNS 2007, Zhuhai, China. Lecture Notes in Computer Science, volume 4521, pages 87-103. Springer. Available at http://basics.sjtu.edu.cn/~yuxin/publications/ecash.ps.
  28. Kevin D. Lux, Michael J. May, Nayan L. Bhattad, and Carl A. Gunter. WSEmail: Secure Internet Messaging Based on Web Services. In International Conference on Web Services (ICWS'05). Available at http://wsemail.ws/.
  29. Sebastian Mödersheim. Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases, CCS 2010. Available at http://www2.imm.dtu.dk/~samo/setabstraction.pdf.
  30. Frank S. Park, Chinmay Gangakhedkar, and Patrick Traynor. Leveraging Cellular Infrastructure to Improve Fraud Prevention. In 2009 Annual Computer Security Applications Conference (ACSAC-25). Available at http://www.acsac.org/2009/openconf/modules/request.php?module=oc_program&action=summary.php&id=220
  31. Joeri de Ruiter and Erik Poll. Formal Analysis of the EMV Protocol Suite. In Theory of Security and Applications (TOSCA'11), March-April 2011. Available at http://www.cs.ru.nl/E.Poll/papers/emv.pdf.
  32. Ben Smyth, Mark Ryan and Liqun Chen. Formal analysis of anonymity in ECC-based Direct Anonymous Attestation schemes. In Proceedings of the Eighth International Workshop on Formal Aspects of Security and Trust (FAST'11). Available at http://www.cs.bham.ac.uk/~mdr/research/papers/pdf/11-ecc-daa.pdf

Tools

Courses on ProVerif

ProVerif is taught at the MPRI, course 2-30. Here is a list of some courses on ProVerif by other researchers:

If you have written a research paper or a tool using ProVerif, or teach a course on ProVerif, and want it to be added to this page, or if you want the reference to your paper/tool/course to be removed or corrected, please contact Bruno Blanchet.

Bruno Blanchet