Publications

Copyright / Droits d'auteur.

Journals/Journaux

[1]

David Cadé and Bruno Blanchet. From Computationally-Proved Protocol Specifications to Implementations and Application to SSH. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), 4(1):4-31, March 2013. Special issue ARES'12.

[2]

Bruno Blanchet. Automatic Verification of Correspondences for Security Protocols. Journal of Computer Security, 17(4):363-434, July 2009.

[3]

Bruno Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. IEEE Transactions on Dependable and Secure Computing, 5(4):193-207, October-December 2008. Special issue IEEE Symposium on Security and Privacy 2006. Electronic version available at http://doi.ieeecomputersociety.org/10.1109/TDSC.2007.1005.

[4]

Bruno Blanchet, Martín Abadi, and Cédric Fournet. Automated Verification of Selected Equivalences for Security Protocols. Journal of Logic and Algebraic Programming, 75(1):3-51, February-March 2008.

[5]

Martín Abadi, Bruno Blanchet, and Cédric Fournet. Just Fast Keying in the Pi Calculus. ACM Transactions on Information and System Security (TISSEC), 10(3):1-59, July 2007.

[6]

Martín Abadi and Bruno Blanchet. Computer-Assisted Verification of a Protocol for Certified Email. Science of Computer Programming, 58(1-2):3-27, October 2005. Special issue SAS'03.

[7]

Bruno Blanchet. Security Protocols: From Linear to Classical Logic by Abstract Interpretation. Information Processing Letters, 95(5):473-479, September 2005.

[8]

Bruno Blanchet and Andreas Podelski. Verification of Cryptographic Protocols: Tagging Enforces Termination. Theoretical Computer Science, 333(1-2):67-90, March 2005. Special issue FoSSaCS'03.

[9]

Martín Abadi and Bruno Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM, 52(1):102-146, January 2005.

[10]

Bruno Blanchet. Escape Analysis for Java(TM). Theory and Practice. ACM Transactions on Programming Languages and Systems, 25(6):713-775, November 2003.

[11]

Martín Abadi and Bruno Blanchet. Secrecy Types for Asymmetric Communication. Theoretical Computer Science, 298(3):387-415, April 2003. Special issue FoSSaCS'01.

Chapters in books/Chapitres de livres

[1]

Bruno Blanchet. Mechanizing Game-Based Proofs of Security Protocols. In Tobias Nipkow, Olga Grumberg, and Benedikt Hauptmann, editors, Software Safety and Security - Tools for Analysis and Verification, volume 33 of NATO Science for Peace and Security Series - D: Information and Communication Security, pages 1-25. IOS Press, May 2012. Proceedings of the summer school MOD 2011.

[2]

Bruno Blanchet. Using Horn Clauses for Analyzing Security Protocols. In Véronique Cortier and Steve Kremer, editors, Formal Models and Techniques for Analyzing Security Protocols, volume 5 of Cryptology and Information Security Series, pages 86-111. IOS Press, March 2011.

[3]

Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software, invited chapter. In T. Mogensen, D. A. Schmidt, and I. H. Sudborough, editors, The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, volume 2566 of Lecture Notes in Computer Science, pages 85-108. Springer, December 2002.

Invited Conferences/Conférences invitées

[1]

Bruno Blanchet. Security Protocol Verification: Symbolic and Computational Models. In Pierpaolo Degano and Joshua Guttman, editors, First Conference on Principles of Security and Trust (POST'12), volume 7215 of Lecture Notes in Computer Science, pages 3-29, Tallinn, Estonia, March 2012. Springer.

[2]

Bruno Blanchet. An Automatic Security Protocol Verifier based on Resolution Theorem Proving (invited tutorial). In 20th International Conference on Automated Deduction (CADE-20), Tallinn, Estonia, July 2005.

[3]

Bruno Blanchet. Automatic Verification of Cryptographic Protocols: A Logic Programming Approach (invited talk). In 5th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'03), pages 1-3, Uppsala, Sweden, August 2003. ACM.

[4]

Bruno Blanchet. Abstracting Cryptographic Protocols by Prolog Rules (invited talk). In Patrick Cousot, editor, 8th International Static Analysis Symposium (SAS'2001), volume 2126 of Lecture Notes in Computer Science, pages 433-436, Paris, France, July 2001. Springer.

Conferences/Conférences

[1]

David Cadé and Bruno Blanchet. Proved Generation of Implementations from Computationally-Secure Protocol Specifications. In David Basin and John Mitchell, editors, 2nd Conference on Principles of Security and Trust (POST 2013), volume 7796 of Lecture Notes in Computer Science, pages 63-82, Rome, Italy, March 2013. Springer.

[2]

Vincent Cheval and Bruno Blanchet. Proving More Observational Equivalences with ProVerif. In David Basin and John Mitchell, editors, 2nd Conference on Principles of Security and Trust (POST 2013), volume 7796 of Lecture Notes in Computer Science, pages 226-246, Rome, Italy, March 2013. Springer.

[3]

David Cadé and Bruno Blanchet. From Computationally-proved Protocol Specifications to Implementations. In 7th International Conference on Availability, Reliability and Security (AReS 2012), pages 65-74, Prague, Czech Republic, August 2012. IEEE.

[4]

Bruno Blanchet. Automatically Verified Mechanized Proof of One-Encryption Key Exchange. In 25th IEEE Computer Security Foundations Symposium (CSF'12), pages 325-339, Cambridge, MA, USA, June 2012. IEEE.

[5]

Miriam Paiola and Bruno Blanchet. Verification of security protocols with lists: from length one to unbounded length. In Pierpaolo Degano and Joshua Guttman, editors, First Conference on Principles of Security and Trust (POST'12), volume 7215 of Lecture Notes in Computer Science, pages 69-88, Tallinn, Estonia, March 2012. Springer. Available at http://prosecco.gforge.inria.fr/personal/mpaiola/publications/PaiolaBlanchetPOST12.html.

[6]

Martín Abadi (invited speaker), Bruno Blanchet, and Hubert Comon-Lundh. Models and Proofs of Protocol Security: A Progress Report. In Ahmed Bouajjani and Oded Maler, editors, 21st International Conference on Computer Aided Verification (CAV'09), volume 5643 of Lecture Notes in Computer Science, pages 35-49, Grenoble, France, June 2009. Springer.

[7]

Bruno Blanchet and Avik Chaudhuri. Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage. In IEEE Symposium on Security and Privacy, pages 417-431, Oakland, CA, May 2008. IEEE.

[8]

Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, and Joe-Kai Tsay. Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos. In ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), pages 87-99, Tokyo, Japan, March 2008. ACM.

[9]

Bruno Blanchet. Computationally Sound Mechanized Proofs of Correspondence Assertions. In 20th IEEE Computer Security Foundations Symposium (CSF'07), pages 97-111, Venice, Italy, July 2007. IEEE.

[10]

Bruno Blanchet and David Pointcheval. Automated Security Proofs with Sequences of Games. In Cynthia Dwork, editor, CRYPTO'06, volume 4117 of Lecture Notes in Computer Science, pages 537-554, Santa Barbara, CA, August 2006. Springer.

[11]

Bruno Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. In IEEE Symposium on Security and Privacy, pages 140-154, Oakland, California, May 2006.

[12]

Bruno Blanchet, Martín Abadi, and Cédric Fournet. Automated Verification of Selected Equivalences for Security Protocols. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), pages 331-340, Chicago, IL, June 2005. IEEE Computer Society.

[13]

Xavier Allamigeon and Bruno Blanchet. Reconstruction of Attacks against Cryptographic Protocols. In 18th IEEE Computer Security Foundations Workshop (CSFW-18), pages 140-154, Aix-en-Provence, France, June 2005. IEEE Computer Society.

[14]

Bruno Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. In IEEE Symposium on Security and Privacy, pages 86-100, Oakland, California, May 2004.

[15]

Martín Abadi, Bruno Blanchet, and Cédric Fournet. Just Fast Keying in the Pi Calculus. In David Schmidt, editor, Programming Languages and Systems: Proceedings of the 13th European Symposium on Programming (ESOP'04), volume 2986 of Lecture Notes in Computer Science, pages 340-354, Barcelona, Spain, March 2004. Springer.

[16]

Bruno Blanchet and Benjamin Aziz. A Calculus for Secure Mobility. In Vijay Saraswat, editor, Eighth Asian Computing Science Conference (ASIAN'03), volume 2896 of Lecture Notes in Computer Science, pages 188-204, Mumbai, India, December 2003. Springer.

[17]

Martín Abadi and Bruno Blanchet. Computer-Assisted Verification of a Protocol for Certified Email. In Radhia Cousot, editor, Static Analysis, 10th International Symposium (SAS'03), volume 2694 of Lecture Notes in Computer Science, pages 316-335, San Diego, California, June 2003. Springer.

[18]

Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. A Static Analyzer for Large Safety-Critical Software. In ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI'03), pages 196-207, San Diego, California, June 2003. ACM.

[19]

Bruno Blanchet and Andreas Podelski. Verification of Cryptographic Protocols: Tagging Enforces Termination. In Andrew Gordon, editor, Foundations of Software Science and Computation Structures (FoSSaCS'03), volume 2620 of Lecture Notes in Computer Science, pages 136-152, Warsaw, Poland, April 2003. Springer.

[20]

Bruno Blanchet. From Secrecy to Authenticity in Security Protocols. In Manuel Hermenegildo and Germán Puebla, editors, 9th International Static Analysis Symposium (SAS'02), volume 2477 of Lecture Notes in Computer Science, pages 342-359, Madrid, Spain, September 2002. Springer.

[21]

Martín Abadi and Bruno Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. In 29th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL 2002), pages 33-44, Portland, Oregon, January 2002. ACM Press.

[22]

Bruno Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82-96, Cape Breton, Nova Scotia, Canada, June 2001. IEEE Computer Society.

[23]

Martín Abadi and Bruno Blanchet. Secrecy Types for Asymmetric Communication. In F. Honsell and M. Miculan, editors, Foundations of Software Science and Computation Structures (FoSSaCS 2001), volume 2030 of Lecture Notes in Computer Science, pages 25-41, Genova, Italy, April 2001. Springer.

[24]

Bruno Blanchet. Escape Analysis for Object Oriented Languages. Application to Java(TM). In Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'99), pages 20-34, Denver, Colorado, November 1999.

[25]

Bruno Blanchet. Escape Analysis: Correctness Proof, Implementation and Experimental Results. In 25th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'98), pages 25-37, San Diego, California, January 1998. ACM Press.

Workshops

[1]

Bruno Blanchet. A second look at Shoup's lemma. In Workshop on Formal and Computational Cryptography (FCC 2011), Paris, France, June 2011.

[2]

Bruno Blanchet and David Pointcheval. The computational and decisional Diffie-Hellman assumptions in CryptoVerif. In Workshop on Formal and Computational Cryptography (FCC 2010), Edimburgh, United Kingdom, July 2010.

[3]

Bruno Blanchet, Aaron D. Jaggard, Jesse Rao, Andre Scedrov, and Joe-Kai Tsay. Refining Computationally Sound Mechanized Proofs for Kerberos. In Workshop on Formal and Computational Cryptography (FCC 2009), Port Jefferson, NY, July 2009.

[4]

Bruno Blanchet. CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols. In Dagstuhl seminar Formal Protocol Verification Applied, October 2007.

[5]

Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, and Joe-Kai Tsay. Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos. In Dagstuhl seminar Formal Protocol Verification Applied, October 2007.

[6]

Bruno Blanchet. A Computationally Sound Automatic Prover for Cryptographic Protocols. In Workshop on the link between formal and computational models, Paris, France, June 2005.

[7]

Bruno Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. In Dagstuhl seminar Language-Based Security, October 2003.

[8]

Bruno Blanchet and Benjamin Aziz. A Calculus for Locations, Mobility, and Cryptography. In Dagstuhl seminar Reasoning about Shape, March 2003.

[9]

Martín Abadi and Bruno Blanchet. Secrecy Types for Asymmetric Communication. In Dagstuhl seminar Security through Analysis and Verification, December 2000.

Theses/Mémoires et thèse

[1]

Bruno Blanchet. Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire. Automatic verification of security protocols: formal model and computational model. Mémoire d'habilitation à diriger des recherches, Université Paris-Dauphine, November 2008. En français avec publications en anglais en annexe. In French with publications in English in appendix.

[2]

Bruno Blanchet. Analyse d'échappement. Applications à ML et Java(TM). Escape Analysis. Applications to ML and Java(TM). PhD thesis, École Polytechnique, 7 December 2000. En anglais. In English. Prix de thèse de l'École Polytechnique. Thesis prize of Ecole Polytechnique.

[3]

Bruno Blanchet. Rapport de magistère MMFAI. Master's thesis, ENS, October 1997. En français.

[4]

Bruno Blanchet. Garbage Collection statique. Rapport de DEA, INRIA, Rocquencourt, September 1996. En français.

Reports/Rapports

[1]

Bruno Blanchet. Automatically verified mechanized proof of one-encryption key exchange. Cryptology ePrint Archive, Report 2012/173, April 2012. Available at http://eprint.iacr.org/2012/173.

[2]

Bruno Blanchet. Automatic verification of correspondences for security protocols. Report arXiv:0802.3444v1, February 2008. Available at http://arxiv.org/abs/0802.3444v1.

[3]

Bruno Blanchet. Computationally sound mechanized proofs of correspondence assertions. Cryptology ePrint Archive, Report 2007/128, April 2007. Available at http://eprint.iacr.org/2007/128.

[4]

Bruno Blanchet and David Pointcheval. Automated security proofs with sequences of games. Cryptology ePrint Archive, Report 2006/069, February 2006. Available at http://eprint.iacr.org/2006/069.

[5]

Bruno Blanchet. A computationally sound mechanized prover for security protocols. Cryptology ePrint Archive, Report 2005/401, November 2005. Available at http://eprint.iacr.org/2005/401.

[6]

Bruno Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. Technical Report MPI-I-2004-NWG1-001, Max-Planck-Institut für Informatik, Saarbrücken, Germany, July 2004.