Users of ProVerif

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.

Research papers

350+ publications have used ProVerif, including 60+ in rank A* or A conferences, according to ICORE conference ranking 2026.

We list publications in rank A* or A conferences below. Click here for the full list.

2004
  1. 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 https://bhargavan.info/pubs/verifying-policy-based-security-ccs04.pdf.
2005
  1. 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 https://markryan.eu/research/papers/pdf/04-eVoting.pdf
2006
  1. 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 https://dl.acm.org/doi/10.1145/1128817.1128828.
  2. 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 https://bhargavan.info/pubs/verified-interoperable-implementations-csfw06.pdf.
2008
  1. 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 https://bhargavan.info/pubs/cryptographically-verified-implementations-for-tls-ccs08.pdf.
  2. 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 https://sec.uni-stuttgart.de/_media/publications/KuestersTruderung-CCS-2008.pdf.
  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, 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 https://bhargavan.info/pubs/verified-implementations-of-cardspace-asiaccs08.pdf.
  5. 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 https://ieeexplore.ieee.org/document/4556687
2009
  1. 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. Available at http://doi.ieeecomputersociety.org/10.1109/CSF.2009.12.
  2. 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 https://sec.uni-stuttgart.de/_media/publications/KuestersTruderung-CSF-2009.pdf.
2010
  1. 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.
  2. Mayla Brusó, Konstantinos Chatzikokolakis and Jerry den Hartog. Formal verification of privacy for RFID systems. 23rd IEEE Computer Security Foundations Symposium, 2010. Available at https://doi.org/10.1109/CSF.2010.13.
2011
  1. Mihhail Aizatulin, Andrew Gordon, and Jan Jürjens. Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution. In CCS 2011. Available at https://doi.org/10.1145/2046707.2046745.
  2. 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 https://markryan.eu/research/papers/pdf/11-state-appi.pdf.
  3. 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.
2012
  1. Myrto Arapinis, Vincent Cheval, and Stéphanie Delaune. Verifying Privacy-Type Properties in a Modular Way, CSF 2012. Available at https://doi.org/10.1109/CSF.2012.16.
  2. Chetan Bansal, Karthikeyan Bhargavan, and Sergio Maffeis. Discovering Concrete Attacks on Website Authorization by Formal Analysis, CSF 2012. Available at https://bhargavan.info/pubs/discovering_concrete_attacks_csf12.pdf.
  3. Alisa Pankova and Peeter Laud. Symbolic Analysis of Cryptographic Protocols Containing Bilinear Pairings, CSF 2012. Available at http://research.cyber.ee/~peeter/research/csf12.pdf.
  4. Naipeng Dong, Hugo Jonker, and Jun Pang. Formal analysis of privacy in an eHealth protocol. In Proc. 17th European Symposium on Research in Computer Security - ESORICS'12, Lecture Notes in Computer Science 7459, pp. 325-342. Springer-Verlag, 2012. Available at http://satoss.uni.lu/members/jun/papers/ESORICS12.pdf.
2013
  1. Guangdong Bai, Guozhu Meng, Jike Lei, Sai Sathyanarayan Venkatraman, Prateek Saxena, Jun Sun, Yang Liu and Jinsong Dong. AuthScan: Automatic Extraction of Web Authentication Protocols From Implementations. In 20th Annual Network & Distributed System Security Symposium (NDSS'13). Available at https://impillar.github.io/files/ndss2013authscan.pdf.
  2. Florian Böhl and Dominique Unruh. Symbolic Universal Composability. In 26th Computer Security Foundations Symposium (CSF'13), pages 257-271, June 2013. Available at http://kodu.ut.ee/~unruh/publications/symbolic-uc.html.
2015
  1. Alessandro Bruni, Sebastian Mödersheim, Flemming Nielson, Hanne Riis Nielson. Set-Pi: Set Membership Pi-Calculus. In Computer Security Foundations Symposium (CSF'15), pages 185-198. Available at https://doi.org/10.1109/CSF.2015.20.
  2. Michael Backes, Fabian Bendun, Matteo Maffei, Esfandiar Mohammadi, Kim Pecina. Symbolic Malleable Zero-Knowledge Proofs. In Computer Security Foundations Symposium (CSF'15), pages 412-480. Available at https://doi.org/10.1109/CSF.2015.35.
2016
  1. Lucca Hirschi, David Baelde, and Stéphanie Delaune. A Method for Verifying Privacy-Type Properties: The Unbounded Case. In IEEE Symposium on Security and Privacy. Available at https://people.irisa.fr/Stephanie.Delaune/PUBLICATIONS-HTML/b2hd-HBD-sp16.html.
  2. Kim Thuat Nguyen, Nouha Oualha, and Maryline Laurent. Authenticated Key Agreement Mediated by a Proxy Re-encryptor for the Internet of Things. In ESORICS'16. Available at http://link.springer.com/chapter/10.1007/978-3-319-45741-3_18.
2018
  1. V. Cheval, V. Cortier and M. Turuani. A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. In Proceedings of the 31th IEEE Computer Security Foundations Symposium (CSF'18). Available at https://chevalvi.gitlabpages.inria.fr/chevalvi/files/CCT-csf18.pdf
  2. Charlie Jacomme and Steve Kremer. An extensive formal analysis of multi-factor authentication protocols. In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18). See https://members.loria.fr/SKremer/files/Publications/b2hd-JK-csf18.html
2019
  1. Di Long Li and Alwen Tiu. Combining ProVerif and Automated Theorem Provers for Security Protocol Verification. In CADE 2019: Automated Deduction - CADE 27, pp. 354-365. Long version available at https://github.com/darrenldl/ProVerif-ATP/blob/master/paper/CADE-27_paper-42_Di_Long_Li_and_Alwen_Tiu_full.pdf.
  2. V. Cortier, A. Filipiak, and J. Lallemand. BeleniosVS: Secrecy and Verifiability Against a Corrupted Voting Device. In 32nd IEEE Computer Security Foundations Symposium (CSF'19). Available at https://members.loria.fr/VCortier/files/Publications/b2hd-beleniosVS-CSF19.html
  3. Nadim Kobeissi, Georgio Nicolas, and Karthikeyan Bhargavan. Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols. In 4th IEEE European Symposium on Security and Privacy (EuroS&P'19). Available at https://eprint.iacr.org/2018/766.
  4. Lucca Hirschi and Cas Cremers. Improving Automated Symbolic Analysis of Ballot Secrecy for E-voting Protocols: A Method Based on Sufficient Conditions. In 4th IEEE European Symposium on Security and Privacy (EuroS&P'19). Available at https://members.loria.fr/LHirschi/pdfs/EuroSP19_evoting.pdf
2021
  1. Haonan Feng, Hui Li, Xuesong Pan, and Ziming Zhao. A Formal Analysis of the FIDO UAF Protocol. In Proceedings of the 28th Annual Network and Distributed System Security Symposium - NDSS 2021. Available at https://www.ndss-symposium.org/ndss-paper/a-formal-analysis-of-the-fido-uaf-protocol/.
  2. Alexander Dax and Robert Künnemann. On the Soundness of Infrastructure Adversaries. In: 2021 IEEE 34th Computer Security Foundations Symposium (CSF). Available at https://doi.ieeecomputersociety.org/10.1109/CSF51468.2021.00039.
2022
  1. Mikael Bougon, Hervé Chabanne, Véronique Cortier, Alexandre Debant, Emmanuelle Dottax, Jannik Dreier, Pierrick Gaudry, Mathieu Turuani. Themis: An On-Site Voting System with Systematic Cast-as-intended Verification and Partial Accountability. In: CCS '22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, November 2022, Pages 397–410. Available at https://doi.org/10.1145/3548606.3560563.
  2. Jianliang Wu, Ruoyu Wu, Dongyan Xu, Dave (Jing) Tian, and Antonio Bianchi. Formal Model-Driven Discovery of Bluetooth Protocol Design Vulnerabilities. In 2022 IEEE Symposium on Security and Privacy, pages 2285-2303. doi: 10.1109/SP46214.2022.9833777.
  3. Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert Künnemann. SAPIC+: protocol verifiers of the world, unite! In USENIX Security Symposium (USENIX Security), 2022. Available at https://www.usenix.org/conference/usenixsecurity22/presentation/cheval.
  4. Jose Moreira-Sanchez, Mark Ryan, and Flavio Garcia. Protocols for a two-tiered trusted computing base. In Computer Security – ESORICS 2022, 27th European Symposium on Research in Computer Security, Copenhagen, Denmark, September 26–30, 2022, Proceedings, Part III, pages 229-249. LNCS, volume 13556, Springer, Cham. Available at https://doi.org/10.1007/978-3-031-17143-7_12.
  5. Stéphanie Delaune and Joseph Lallemand. One vote is enough for analysing privacy. In Proceedings of the 27th European Symposium on Research in Computer Security (ESORICS'22), pp. 173–194, Lecture Notes in Computer Science, Springer, Copenhague, Denmark, 2022. Available at https://doi.org/10.1007/978-3-031-17140-6_9.
2023
  1. Sergiu Bursuc, Ross Horne, Sjouke Mauw, and Semen Yurkov. Provably Unlinkable Smart Card-based Payments. In CCS '23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, November 2023, Pages 1392–1406. Available at https://doi.org/10.1145/3576915.3623109.
  2. Faezeh Nasrabadi, Robert Künnemann, and Hamed Nemati. CryptoBap: A Binary Analysis Platform for Cryptographic Protocols. In CCS '23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, November 2023, Pages 1362–1376. Available at https://doi.org/10.1145/3576915.3623090.
  3. Charlie Jacomme, Elise Klein, Steve Kremer, and Maïwenn Racouchot. A comprehensive, formal and automated analysis of the EDHOC protocol. In USENIX Security '23 - 32nd USENIX Security Symposium, Aug 2023, Anaheim, CA, United States. Available at https://inria.hal.science/hal-03810102/.
  4. David Baelde, Alexandre Debant, and Stéphanie Delaune. Proving Unlinkability using ProVerif through Desynchronized Bi-Processes. In IEEE Computer Security Foundations Symposium, Jul 2023, Dubrovnik, Croatia. Available at https://hal.science/hal-03674979v2.
  5. Sevdenur Baloglu, Sergiu Bursuc, Sjouke Mauw, and Jun Pang. Election Verifiability in Receipt-free Voting Protocols. In IEEE Computer Security Foundations Symposium, Jul 2023, Dubrovnik, Croatia. Available at https://doi.ieeecomputersociety.org/10.1109/CSF57540.2023.00005
2024
  1. Pascal Lafourcade, Dhekra Mahmoud, and Sylvain Ruhault. A Unified Symbolic Analysis of WireGuard. In Usenix Network and Distributed System Security Symposium (NDSS), Feb 2024, San Diego (CA), United States. Available at https://dx.doi.org/10.14722/ndss.2024.24364 and https://uca.hal.science/hal-04615393/.
  2. Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, and Rolfe Schmidt. Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging. USENIX Security Symposium, 2024. Available at https://www.usenix.org/conference/usenixsecurity24/presentation/bhargavan.
  3. Jannik Dreier, Pascal Lafourcade, and Dhekra Mahmoud. Shaken, not Stirred - Automated Discovery of Subtle Attacks on Protocols using Mix-Nets. USENIX Security Symposium, 2024. Available at https://www.usenix.org/system/files/usenixsecurity24-dreier.pdf.
  4. Véronique Cortier, Alexandre Debant, Anselme Goetschmann, and Lucca Hirschi. Election Eligibility with OpenID: Turning Authentication into Transferable Proof of Eligibility. In USENIX Security Symposium, 2024. Available at https://www.usenix.org/conference/usenixsecurity24/presentation/cortier.
  5. Jianliang Wu, Patrick Traynor, Dongyan Xu, Dave (Jing) Tian, and Antonio Bianchi. Finding Traceability Attacks in the Bluetooth Low Energy Specification and Its Implementations. In USENIX Security Symposium, 2024. Available at https://www.usenix.org/conference/usenixsecurity24/presentation/wu-jianliang.
  6. Sevdenur Baloglu, Sergiu Bursuc, Sjouke Mauw, and Jun Pang. Formal Verification and Solutions for Estonian E-Voting. In ASIA CCS'24: Proceedings of the 19th ACM Asia Conference on Computer and Communications Security, Pages 728-741. Available at https://doi.org/10.1145/3634737.3657009.
  7. Binghan Wang, Hui Li, and Jingjing Guan. A Formal Analysis of Data Distribution Service Security. In: ASIA CCS '24: Proceedings of the 19th ACM Asia Conference on Computer and Communications Security, pages 716-727. Available at https://doi.org/10.1145/3634737.3656288.
  8. Véronique Cortier, Alexandre Debant, and Florian Moser. Code voting: when simplicity meets security. In ESORICS 2024, 29th European Symposium on Research in Computer Security, Sep 2024, Bydgoszcz, Poland. Available at https://inria.hal.science/hal-04627733/.
  9. Zichao Zhang, Limin Jia, and Corina Păsăreanu. ProInspector: Uncovering Logical Bugs in Protocol Implementations. In 9th IEEE European Symposium on Security and Privacy (EuroS&P 2024). Available at https://doi.org/10.1109/EuroSP60621.2024.00040.
2025
  1. Karthikeyan Bhargavan, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch, and Bas Spitters. Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust. In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security (CCS '25). Association for Computing Machinery, New York, NY, USA, 2729–2743. Available at https://doi.org/10.1145/3719027.3765213.
  2. Vincent Diemunsch, Lucca Hirschi, and Steve Kremer. A Comprehensive Formal Security Analysis of OPC UA. In: 34th USENIX Security Symposium (USENIX Security 25), pp. 7077--7096. Available at https://www.usenix.org/conference/usenixsecurity25/presentation/diemunsch.
  3. Pascal Lafourcade, Dhekra Mahmoud, Sylvain Ruhault, and Abdul Rahman Taleb. A Tale of Two Worlds, a Formal Story of WireGuard Hybridization. In 34th USENIX Security Symposium (USENIX Security 25), pp. 4937--4956. Available at https://www.usenix.org/conference/usenixsecurity25/presentation/lafourcade.
  4. Xiaofeng Liu, Chaoshun Zuo, Qinsheng Hou, Pengcheng Ren, Jianliang Wu, Qingchuan Zhao, Shanqing Guo. A Thorough Security Analysis of BLE Proximity Tracking Protocols. In: 34th USENIX Security Symposium (USENIX Security 25), pp. 5347-5364. Available at https://www.usenix.org/conference/usenixsecurity25/presentation/liu-xiaofeng.
  5. Ayoub Ben Hassen, Pascal Lafourcade, Dhekra Mahmoud, and Maxime Puys. Formal Analysis of SDNsec: Attacks and Corrections for Payload, Route Integrity and Accountability. In Proceedings of the 20th ACM Asia Conference on Computer and Communications Security (ASIA CCS '25). Association for Computing Machinery, New York, NY, USA, 1476–1489. Available at https://doi.org/10.1145/3708821.3710828.
  6. Ioana Boureanu, Cristina Onete, Stephan Wesemeyer, Léo Robert, Rhys Miller, Pascal Lafourcade, and Fortunat Rajaona. Post-Compromise Security with Application-Level Key-Controls – with a comprehensive study of the 5G AKMA protocol. In: Proceedings of the 20th ACM Asia Conference on Computer and Communications Security (ASIA CCS '25). Association for Computing Machinery, New York, NY, USA, 231–247. Available at https://doi.org/10.1145/3708821.3733910.
  7. Faezeh Nasrabadi, Robert Künnemann, and Hamed Nemati. Symbolic Parallel Composition for Multi-language Protocol Verification. In: 2025 IEEE 38th Computer Security Foundations Symposium (CSF), Santa Cruz, CA, USA, 2025, pp. 378-393. Available at https://doi.org/10.1109/CSF64896.2025.00030.
  8. Véronique Cortier, Alexandre Debant, Pierrick Gaudry, Léo Louistisserand. Vote&Check: Secure Postal Voting with Reduced Trust Assumptions. In Privacy Enhancing Technologies Symposium, 2025, issue 3, pp. 333-348. Available at https://doi.org/10.56553/popets-2025-0101.
2026
  1. Tommaso Sacchetti and Daniele Antonioli. BLERP: BLE Re-Pairing Attacks and Defenses. NDSS 2026, 33rd Network and Distributed System Security Symposium, Feb 2026, San Diego, United States. Available at https://doi.org/10.14722/ndss.2026.240121.
  2. Elsa Lopez Perez, Thomas Watteyne, Cristina Onete, Dhekra Mahmoud, Pascal Lafourcade, Vaishnavi Sundararajan, and Mališa Vučinić. Formal Verification of EDHOC-PSK: A Symbolic Approach with SAPIC. In: Asia CCS'26. Available at https://doi.org/10.1145/3779208.3805979

Tools

Courses on ProVerif

ProVerif was taught at MPRI. Here is a list of some courses on ProVerif by other researchers: