Talks / Exposés

• Escape Analysis. Applications to ML and Java(TM). PhD defense, Ecole Polytechnique, December 2000.
• Abstract interpretation. Application to stack allocation and synchronization elimination in Java(TM). Colloquium junior, INRIA, February 2001.
• An Efficient Protocol Verifier based on Logic Programming. Seminar of the Laboratoire Spécification et Vérification, ENS Cachan, France, January 2002.
• Analyzing Security Protocols with Secrecy Types and Logic Programs. POPL'2002, Portland, Oregon, January 2002 (joint work with Martín Abadi).
• Action Spécifique Sécurité, ENST, Paris, France, May 2002.
• From Secrecy to Authenticity in Security Protocols. Seminar Semantics and Abstract Interpretation, ENS Ulm, Paris, France, June 2002.
• From Secrecy to Authenticity in Security Protocols. SAS'02, Madrid, Spain, September 2002.
• From Secrecy to Authenticity in Security Protocols. Joint security seminar, DFKI-MPII, November 20, 2002.
• A Calculus for Locations, Mobility, and Cryptography. Shloss Dagstuhl, seminar "Reasoning about shape". March 2003 (joint work with Benjamin Aziz).
• Verification of Cryptographic Protocols: Tagging Enforces Termination. MPII, March 2003 (joint work with Andreas Podelski).
• Verification of Cryptographic Protocols: Tagging Enforces Termination. FoSSaCS'03, Warsaw, April 2003 (joint work with Andreas Podelski).
• Automatic Proof of Authenticity for Security Protocols. MINERVA Workshop, MPII, Mai 2003.
• Computer-Assisted Verification of a Protocol for Certified Email. SAS'03, San Diego, CA, June 2003 (joint work with Martín Abadi).
• Computer-Assisted Verification of a Protocol for Certified Email. Microsoft Research, Cambridge, UK, August 2003 (joint work with Martín Abadi).
• Automatic Verification of Cryptographic Protocols: A Logic Programming Approach (invited talk). PPDP'03, Uppsala, Sweden, August 2003.
• Automatic Proof of Strong Secrecy for Security Protocols. Shloss Dagstuhl, seminar "Language-Based Security". October 2003.
• A Calculus for Secure Mobility. ASIAN'03, Mumbai, India, December 2003 (joint work with Benjamin Aziz).
• Automatic Proof of Strong Secrecy for Security Protocols. INRIA Rocquencourt, January 2004.
• Automatic Proof of Strong Secrecy for Security Protocols. Seminar Semantics and Abstract Interpretation, ENS Ulm, Paris, France, February 2004.
• Automatic Proof of Strong Secrecy for Security Protocols. IEEE Symposium on Security and Privacy, Oakland, California, May 2004.
• A Computationally Sound Automatic Prover for Cryptographic Protocols. Workshop on the link between formal and computational models. Paris, France. June 2005.
• Automated Verification of Selected Equivalences for Security Protocols. LICS'05, Chicago, IL, June 2005 (joint work with Martín Abadi and Cédric Fournet).
• An Automatic Security Protocol Verifier based on Resolution Theorem Proving (invited tutorial). CADE'05, Tallinn, Estonia, July 2005.
• Automated Verification of Selected Equivalences for Security Protocols. LSV, ENS Cachan, December 2005 (joint work with Martín Abadi and Cédric Fournet).
• Automated Verification of Selected Equivalences for Security Protocols. PPS, Université Paris VII, January 2006 (joint work with Martín Abadi and Cédric Fournet).
• An Automatic Security Protocol Verifier based on Resolution Theorem Proving. IRMAR, Rennes, January 2006.
• A Computationally Sound Mechanized Prover for Cryptographic Protocols. ENS, Paris, January 2006.
• Automated Security Proofs with Sequences of Games. Formacrypt meeting, ENS, Paris, March 2006 (joint work with David Pointcheval).
• A Computationally Sound Mechanized Prover for Cryptographic Protocols. IEEE S&P, Oakland, CA, May 2006. pdf
• A Computationally Sound Mechanized Prover for Cryptographic Protocols. Seminar of the Microsoft INRIA joint lab, June 2006. pdf
• Automated Security Proofs with Sequences of Games. CRYPTO'06, August 2006 (joint work with David Pointcheval). pdf
• Automated Security Proofs with Sequences of Games. Seminaire, Université de Caen, October 2006 (joint work with David Pointcheval). pdf
• Computationally Sound Mechanized Proofs of Correspondence Assertions. CSF'07, Venice, Italy, July 2007.
• CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols. Shloss Dagstuhl, seminar "Formal Protocol Verification Applied", October 2007.
• Automated Security Proofs with Sequences of Games. Seminaire, IRIT, Toulouse, January 2008 (joint work with David Pointcheval).
• Automated Security Proofs with Sequences of Games. Seminaire, RCIS, AIST, Tokyo, March 2008 (joint work with David Pointcheval).
• Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos. CSF'08 five minute talk, Pittsburgh, PA, June 2008 (joint work with Aaron D. Jaggard, Andre Scedrov, and Joe-Kai Tsay).
• Automatic verification of security protocols: formal model and computational model. Exposé d'habilitation à diriger des recherches, Université Paris-Dauphine, November 2008.
• Course on the verification of security protocols, Padova University, March 2009. Introduction to security protocols The verifier ProVerif
• CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols. University of Padova, Italy, March 2009.
• CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols. Computational and Symbolic Proofs of Security, Spring School and French-Japanese collaboration workshop, Atagawa Heights, Japan, April 2009.
• Models and Proofs of Protocol Security: A Progress Report. (with Martín Abadi and Hubert Comon-Lundh) FormaCrypt meeting, ENS, Paris, June 2009.
• Diffie-Hellman in CryptoVerif FormaCrypt meeting, ENS, Paris, June 2009.
• CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols. MITACS workshop, Grenoble, June 2009.
• CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols. Stony Brook University, NY, July 2009.
• CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols. Ecrypt-2 summer school on provable security, Barcelona, Spain, September 2009. enc-then-MAC.cv fdh.cv
• Automatic, computational proof of EKE using CryptoVerif. Computational and Symbolic Proofs of Security, Spring School and French-Japanese collaboration workshop, Barbizon, France, April 2010.
• CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols . CryptoForma workshop, IHP, Paris, France, May 2010.
• Automatic, computational proof of EKE using CryptoVerif. University of Padova, Italy, May 2010.
• The automatic protocol verifier ProVerif. SecRet workshop, Valencia, Spain, June 2010.
• The computational and decisional Diffie-Hellman assumptions in CryptoVerif (with David Pointcheval). Workshop on formal and computational cryptography (FCC'10), Edinburgh, UK, July 2010.
• Automatic verification of security protocols: formal model and computational model. Exposé au comité des projets de l'INRIA, décembre 2010.
• Automatically Verified Mechanized Proof of One-Encryption Key Exchange (with David Pointcheval). Seminar, Munich, December 2010.
• From a Concurrency Course to Automatic Verification of Process Equivalences. Anniversary workshop in honour of Gérard Berry and Jean-Jacques Lévy, Gérardmer, February 2011.
• A second look at Shoup's lemma. Workshop on Formal and Computational Cryptography (FCC'11), Paris, June 2011.
• Mechanizing proofs by sequences of games. Marktoberdorf Summer School, Bayrischzell, Germany, August 2011.
• Course on ProVerif. VTSA Summer School, Liege, Belgium, September 2011. Slides: introduction ProVerif
• Automatic verification of security protocols: the tools ProVerif and CryptoVerif, seminar, Rennes, France, October 2011.
• Automatically Verified Mechanized Proof of One-Encryption Key Exchange, Workshop on Computed-Aided Security, Grenoble, France, January 2012.
• Automatically Verified Mechanized Proof of One-Encryption Key Exchange, Prosecco day, Paris, France, March 2012.
• Security Protocol Verification: Symbolic and Computational Models, ETAPS invited talk, Tallinn, Estonia, March 2012.
• From CryptoVerif Specifications to Computationally Secure Implementations of Protocols, Workshop on Formal and Computational Cryptographic Proofs, Cambridge, UK, April 2012.
• Automatically Verified Mechanized Proof of One-Encryption Key Exchange, CSF'12, Cambridge, MA, USA, June 2012.
• FOSAD'13 summer school, Bertinoro, Italy, September 2013: introduction, ProVerif.
• Protocoles cryptographiques: Attaques Vérification, L'entreprise dématérialisée, Chambre de Commerce et d'Industrie de Versailles, juin 2014.
• Vérification de protocoles et programmes cryptographiques, Rencontre Inria - Industrie Télécoms du futur, Table ronde Sécurité des Réseaux et Contenus, novembre 2014.
• CryptoVerif course, joint EasyCrypt - F* - CryptoVerif school, November 2014. General introductory talk, Course, enc-then-MAC.cv, FDH.cv, Tutorial.
• From CryptoVerif Specifications to Computationally Secure Implementations of Protocols, Seminar "The synergy between programming languages and cryptography", Schloss Dagstuhl, Wadern, Germany, December 2014.
• The Applied Pi Calculus... with Proofs. Prosecco seminar, April 2015 (joint work with Martín Abadi and Cédric Fournet).
• The automatic protocol verifier CryptoVerif. Seminar at the CEA, April 2015.
• Proving observational equivalence with ProVerif. Colloquium in honour of Martin Abadi, ENS Cachan, June 2015.
• The applied pi calculus... with proofs. CSF'15 five-minute talk, Verona, Italy, July 2015 (joint work with Martín Abadi and Cédric Fournet).
• On some Logic-Based Approaches to Security Protocol Verification. Workshop to celebrate John Mitchell's 60th birthday, Stanford University, CA, May 2016.
• 2nd IEEE European Symposium on Security and Privacy, conference announcement. IEEE Symposium on Security and Privacy, 5 minute talk, May 2016.
• Automatic Verification of Security Protocols: ProVerif and CryptoVerif. Facebook, Menlo Park, CA, May 2016.
• Automated Proof Techniques for Cryptographic Assurance. European Brokerage meeting, Paris, September 2016.
• CryptoVerif: automating computational security proofs. IoTSec: Workshop on Tools and Techniques for Security Analysis. Oslo University, Norway, December 2016.
• CryptoVerif: state of the art, perspectives, and relations to other tools. Models and Tools for Security Analysis and Proofs. Paris, France, April 2017.
• Mechanized Computational Proof of the TLS 1.3 Standard Candidate. TLS 1.3: Design, Implementation & Verification Workshop. Paris, France, April 2017.
• Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. Summer Research Institute, EPFL, Lausanne, June 2017 (joint work with Karthikeyan Bhargavan and Nadim Kobeissi).
• Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols. IEEE Computer Security Foundations Symposium, August 2017.
• The Applied Pi Calculus... with Proofs. 5 minute talk, IEEE Computer Security Foundations Symposium, August 2017 (joint work with Martín Abadi and Cédric Fournet).
• Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. TMSP: Trends in Mechanized Security Proofs, September 2017 (joint work with Karthikeyan Bhargavan and Nadim Kobeissi).
• Composition Theorems for CryptoVerif and Application to TLS 1.3. ANR TECAP meeting, LSV, ENS Cachan, March 2018.
• Composition Theorems for CryptoVerif and Application to TLS 1.3. Prosecco seminar, June 2018.
• Composition Theorems for CryptoVerif and Application to TLS 1.3. CSF'18, Oxford, UK, July 2018.
• CryptoVerif: mechanizing game-based proofs. VeriCrypt'20, virtual, December 2020.
• Vérification de protocoles cryptographiques. ENS, Paris, September 2021.
• Introduction to Symbolic and Computational Proofs. VeriCrypt'21, virtual, December 2021.
• The security protocol verifier ProVerif and its major recent improvements. 2022 Annual Meeting of the WG "Formal Methods for Security", Fréjus, France, March 2022 (joint work with Vincent Cheval and Véronique Cortier).
• The security protocol verifier ProVerif and its Horn clause resolution algorithm. 9th Workshop on Horn Clauses for Verification and Synthesis (HCVS'22), Munich, Germany, April 2022.
• The security protocol verifier ProVerif and its recent improvements: lemmas, induction, fast subsumption, and much more. UK Security and Privacy seminar, zoom, May 2022. Video
• CV2EC : Getting the Best of Both Worlds. Joint Hubert Comon Retirement Workshop - TECAP Workshop, June 2022 (joint work with Pierre Boutry, Christian Doczkal, Benjamin Grégoire, and Pierre-Yves Strub).
• Dealing with key compromise in CryptoVerif. Journée scientifique en l'honneur de Véronique Cortier, LORIA, January 2023.
• Dealing with key compromise in CryptoVerif. 5-minute at the rump session of GT-MFS, Roscoff, March 2023.
• Recent advances in CryptoVerif. 5-minute at the rump session of GT-MFS, Saint-Pierre-d'Oléron, April 2024.
• CV2EC: Getting the Best of Both Worlds. CSF'24, Enschede, Netherlands, July 2024 (joint work with Pierre Boutry, Christian Doczkal, Benjamin Grégoire, and Pierre-Yves Strub).
• Dealing with Dynamic Key Compromise in CryptoVerif. CSF'24, Enschede, Netherlands, July 2024.
• CryptoVerif: Mechanizing Game-Based Proofs of Security Protocols. FOSAD'24 summer school, Bertinoro, Italy, August 2024.