Antoine Delignat-Lavaud, INRIA Paris, PROSECCO

Antoine Delignat-Lavaud

Current occupation

June 23 - September 19, 2014: I am visiting Microsoft Research in Cambridge in the Programming Principles an Tools (PPT) team. I am working with Cedric Fournet to expand my work on the Web PKI started in MSR Silicon Valley last year.

I am a second year PhD student (accredited by ENS Paris) at Inria Paris-Rocquencourt under the direction of Karthikeyan Bhargavan in team PROSECCO (programming securely with cryptography). Our main research goal is to provide practical tools to analyze the security of sensitive web applications, especially those that use cryptographhy.

About myself

More details are available in my academic CV

Recent publications

Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS
(with K. Bhargavan, C. Fournet, A. Pironti and P. Strub), In proceedings of the 35th IEEE Symposium on Security and Privacy (Oakland'14). [PDF] [Slides] [Bib] [Supporting Website]

Discovering Concrete Attacks on Website Authorization by Formal Analysis
(with C. Bansal, K. Bhargavan and S. Maffeis), In Journal of Computer Security, special issue on Web Application Security - Web @ 25, IOS Press, 2014. [Editor Website] [Bib]

Web PKI: Closing the Gap between Guidelines and Practices
(with M. Abadi, A. Birrell, I. Mironov, T. Wobber and Y. Xie), In proceedings of the 21st Annual Network and Distributed System Security Symposium (NDSS'14). [PDF] [Slides] [Bib] [Totient Project at MSR]

Language-Based Defenses Against Untrusted Browser Origins
(with K. Bhargavan and S. Maffeis), In proceedings of the 22th USENIX Security Symposium, 2013. [PDF] [Slides] [Bib] [Presentation] [Supporting Website]

Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage
(with C. Bansal, K. Bhargavan and S. Maffeis), In 2nd Conference on Principles of Security and Trust (POST'13) (David Basin, John Mitchell, eds.), Springer Verlag, 2013. [PDF] [Slides] [Bib]

Web-based Attacks on Host-Proof Encrypted Storage
(with K. Bhargavan), In 6th USENIX Workshop on Offensive Technologies (WOOT'12), 2012. [PDF] [Slides] [Bib]


This year, I am teaching INF431: Algorithmique et programmation at Ecole Polytechnique.

Undergraduate documents

Security Types for Web Applications, master thesis, under the supervision of Karthikeyan Bhargavan, August 2012. [PDF] [Slides]

An automaton model for forest algebras, internship report, under the supervision of Howard Straubing, August 2010. [PDF] [BibTeX entry] [Extended abstract] [Slides]

Partial commutation closures of recognizable languages, internship report, under the supervision of Anca Muscholl and Marc Zeitoun, July 2009. [PDF] [BibTeX entry] [Slides]

An introduction to dependent types, a presentation given for the categories and lambda-calculus course, 2009. [Slides]

Collisions in MD5, a presentation given for an english course, 2009. [Slides]

(in french) Algèbres tropicales et plus court chemin, rapport de TIPE publié dans Quadrature n°72, pp. 22-28, avril 2009. [Version TIPE, PDF] [Errata] [BibTeX] [Version journal]

(in french) Une introduction aux automates cellulaires, 2009. [PDF]

(in french) Précis et formulaire de physique pour la prépa MP, 2008. [PDF]

Actively maintained software

DJS and DJCL: defensive (totally memory isolated) JavaScript, and the defensive JavaScript crypto library. Dedicated website

forestalg (current version: 1.11), a GAP package to handle forest automata, forest algebras and monadic second order logic on forests. Joint work with Howard Straubing. Dedicated page

Outdated software

Network Naval Battle, a client/server game written in C for the network programming course. Download

Cellular Automata Simulator, written in OCaml with a nice GTK interface. OCaml GTK bindings required. Download

Vigenere, a Vigenere encoder/decoder and cracker written in C for the crypto course. Download

Maple C compiler, a set of Maple functions that parse and compile a small subset of the C language into GNU x86 assembly code. Written because of a stupid bet. Download

RSA, a complete implementation in C of the RSA key generation and encryption (along with some attacks on the encoding) written for the crypto course. Download

Graphtools, an OCaml module to work with directed and undirected graphs. Download

Miscellaneous stuff

Some photos I took during my numerous travels.

Last updated July 2014
CSS Valide ! Valid XHTML 1.0 Transitional