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.