Benjamin Lipp

Post-doctoral researcher • Computer-aided cryptography / formal methods in cryptography • Max Planck Institute for Security and Privacy (MPI-SP) • de, en, fr

At MPI-SP, I am associated to the research group Foundations of Security and Privacy led by Gilles Barthe. I am interested in computer-aided cryptography and in particular mechanized cryptographic proofs.

Prior to MPI-SP, I was at Inria Paris in the Prosecco research team for my PhD. My PhD advisors were Bruno Blanchet and Karthikeyan Bhargavan. I have been working with the CryptoVerif proof assistant and the F* proof-oriented programming language, to write proofs for real-world protocols like WireGuard and the recent Hybrid Public Key Encryption standard. My PhD position and conference travel was funded by ERC CIRCUS, ANR AnaStaSec, ANR TECAP, and in the beginning by H2020 NEXTLEAP.

Now: Finishing up my work on a formal link between CryptoVerif and FStar (working title: cv2fstar). (last updated mid August 2022)

Blog Posts

Publications

RFCs / Internet Standards

Peer-Reviewed Articles

Theses

PhD Thesis

Mechanized Cryptographic Proofs of Protocols and their Link with Verified Implementations by Benjamin Lipp. The defence took place on June 28, 2022. More information can be found on the page of the PhD defence.

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

Contact

E-Mail: firstname (dot) lastname (ätt) mpi (dash) sp (dot) org

Elsewhere on the Internet