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 that I co-authored.

• 2022-02-25 Hybrid Public Key Encryption: My Involvement in Development and Analysis of a Cryptographic Standard

• RFC 9180: Hybrid Public Key Encryption

Free and Open Source Software

• Rosenpass: hybrid post-quantum security for the WireGuard VPN

Peer-Reviewed Articles

• Analysing the HPKE Standard by Joël Alwen and Bruno Blanchet and Eduard Hauck and Eike Kiltz and Benjamin Lipp and Doreen Riepel. Eurocrypt 2021.
  • IACR preprint: page, PDF (updates in the nominal groups framework and the security bounds since the conference version!)
  • Talk recordings: 26-min prerecorded (slides), 5-min live with Q&A (slides)
  • CryptoVerif models on Zenodo, on Github
  • Conference version of the paper (the eprint contains updates of the nominal groups framework and the security bounds!)
  A previous, very preliminary, non-peer-reviewed analysis is available as a preprint; it is not up-to-date with the HPKE standard draft:
  An Analysis of Hybrid Public Key Encryption by Benjamin Lipp. IACR preprint 2020/243.
  • IACR preprint page, PDF
  • CryptoVerif models
• A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol by Benjamin Lipp, Bruno Blanchet, Karthikeyan Bhargavan. 4th IEEE European Symposium on Security and Privacy, Jun 2019, Stockholm, Sweden. pp.231-246.
  • Open Access version of the published article
  • Open Access long version
  • Additional material: CryptoVerif models, slides of the conference talk
  • Publisher's version behind paywall

Theses

PhD Thesis

Mechanized Cryptographic Proofs of Protocols and their Link with Verified Implementations. 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. This work has been superseeded by the above-mentioned peer-reviewed article. For completeness, the master's thesis is still made available.

Bachelor's Thesis

sPlot-based Training of Multivariate Classifiers in the Belle II Analysis Software Framework, prepared at Karlsruhe Institute of Technology (KIT) during my bachelor studies in physics. (version in the institute's library)

• Analysing the HPKE Standard, Eurocrypt, October 2021. See paper entry (click to jump)
• VeriCrypt, December 2020, an online workshop on tools for verified cryptography, affiliated event to Indocrypt 2020. Bruno Blanchet and me gave a talk on CryptoVerif. Recording of the talk. Workshop material (slides, exercises, installation scripts).

• CryptoVerif tutorial at Summer School On Real-World Crypto And Privacy 2023, together with Charlie Jacomme.

Summer Semester 2022

• Invited lecture about CryptoVerif in the course Authenticated Key Exchange: Formal Models and Applications.

University Year 2020-21

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

• IP1-Python, a programming beginner's course for first-semester bachelor students. I taught practical exercise sessions for one group (TP).
• Object Oriented Programming and Graphical User Interfaces (POOIG), a Java course for third-semester bachelor students. I taught the practical and theoretical exercise sessions for one group (TP and TD).

University Year 2019-20

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

• IP1-Python, a programming beginner's course for first-semester bachelor students. I taught practical exercise sessions for one group (TP).
• Projet Informatique, a course for fourth-semester bachelor students guiding them during the development of a small app. I helped guide 8 groups of 4 students each.

Academic Community Service

• Program Committee member of CRYPTO 2023
• Program Committee member of the FAVPQC 2022 workshop
• 1 sub-review for CANS 2022
• IEEE S&P 2022: Poster Jury
• 1 review for IEEE S&P 2022
• 1 sub-review for IEEE S&P 2021
• 2 reviews for PETS 2021
• 1 sub-review for Eurocrypt 2021
• IEEE Transactions on Dependable and Secure Computing: 1 review
• IEEE S&P 2020: Shadow Program Committee, Poster Jury

• Social Networks (Microblogging): Mastodon, Twitter.
• Research Networks: Google Scholar, dblp, ResearchGate, ORCID, HAL-Inria, Dissemin
• Hypothes.is: public notes and annotations
• Hackernews: I am usually not actively commenting there, but when my work on WireGuard hit the frontpage, I answered some questions there.
• Code Repositories: GitHub, GitLab, Codeberg, Inria's Gitlab
• LinkedIn (currently not up-to-date)