Publications

This is my old (outdated) webpage. Please visit the new one here.

Conferences

  • A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, and Yi Zhou.
    In 42nd IEEE Symposium on Security and Privacy (S&P’21), Oakland, May 2021 (to appear).
  • Fifty Shades of Ballot Privacy: Privacy against a Malicious Board. Véronique Cortier, Joseph Lallemand, and Bogdan Warinschi.
    In 33rd IEEE Computer Security Foundations Symposium (CSF’20), Boston, June 2020.
  • BeleniosVS: Secrecy and Verifiability against a Corrupted Voting Device. Véronique Cortier, Alicia Filipiak, and Joseph Lallemand.
    In 32nd IEEE Computer Security Foundations Symposium (CSF’19), Hoboken, June 2019.
    Download: [pdf] [pdf (long version)] [model and proofs of the protocol]
  • Voting: You Can’t Have Privacy without Individual Verifiability. Véronique Cortier and Joseph Lallemand.
    In 25th ACM Conference on Computer and Communications Security (CCS’18), Toronto, October 2018.
    Download: [pdf] [pdf (long version)]
  • Equivalence Properties by Typing in Cryptographic Branching Protocols. Véronique Cortier, Niklas Grimm, Joseph Lallemand, and Matteo Maffei.
    In Proceedings of the 7th International Conference on Principles of Security and Trust (POST’18), Thessaloniki, April 2018.
    Download: [pdf (long version)] [implementation files]
  • A Type System for Privacy Properties. Véronique Cortier, Niklas Grimm, Joseph Lallemand, and Matteo Maffei.
    In 24th ACM Conference on Computer and Communications Security (CCS’17), Dallas, October 2017.
    Download: [pdf (long version)] [Typeeq Implementation files] [Example files]
  • Refining Authenticated Key Agreement with Strong Adversaries. Joseph Lallemand, David Basin, and Christoph Sprenger.
    In 2nd European Symposium on Security and Privacy (EuroS&P’17), Paris, April 2017.
    Download: [pdf] [Archive of Formal Proofs entry of Isabelle/HOL development]