Benjamin Lipp

3rd year PhD student • Formal methods in cryptography • Prosecco research team at Inria Paris • de, en, fr

I am broadly interested and enthusiastic about cryptography and more specifically cryptographic protocols. My current research focuses on the mechanization of cryptographic security proofs, mainly for real-world protocols, and on formally linking such proofs to implementations. The tools I use are CryptoVerif for game-based cryptographic proofs, and FStar for verified implementations. My PhD advisors are Bruno Blanchet and Karthikeyan Bhargavan. My PhD proposal is available on theses.fr.

My PhD position and conference travel is funded by ERC CIRCUS, ANR AnaStaSec, ANR TECAP, and in the beginning by H2020 NEXTLEAP.

Now: Besides working on a formal link between CryptoVerif and FStar, I am currently involved in a standardization effort of Hybrid Public Key Encryption within IRTF's CFRG. I am writing an F* implementation of HPKE using HACL*.

Publications

Peer-Reviewed Articles

Master's Thesis

A Mechanised Computational Analysis of the WireGuard Virtual Private Network Protocol by Benjamin Lipp. This work has been superseeded by the above-mentioned peer-reviewed article. For completeness, the master's thesis is still made available.

Talks

Teaching

University Year 2020-21

I was a teaching assistant at Université Paris Diderot which has become part of Université de Paris.

University Year 2019-20

I was a teaching assistant at Université Paris Diderot which has become part of Université de Paris.

Academic Community Service

Elsewhere on the Internet