BlanchetFromherzetalCCS26

Bruno Blanchet Back to publications

Bruno Blanchet, Aymeric Fromherz, Charlie Jacomme, Benjamin Lipp, and Emmanuel Mera. CV2F*: Combining CryptoVerif and F* for Proving Security of Protocol Implementations. In Proceedings of the 2026 ACM SIGSAC Conference on Computer and Communications Security, CCS 2026. ACM Press, November 2026. To appear.

Copyright

© 2026 Copyright held by the owner/author(s). This is the authors' version of The Work. It is posted here for your personal use. Not for redistribution. The definitive version was published in CCS 2026, https://doi.org/10.1145/3830454.3846574.

Get the paper

.pdf, 821 Kb

Links

Long version

Artifact

CV2F* and the case study are also included in CryptoVerif from version 1.13

Abstract

Real-world cryptographic systems build on complex cryptographic operations that are integrated into a wider application layer. For instance, the PQXDH protocol, Signal Messenger's key exchange used to initiate a secure channel between two devices, is integrated in the full Signal Messenger application and notably Sesame, its multi-device and multi-session management algorithm. Proving the security of such systems implies to reason on two aspects: we must be able to perform both cryptographic reasoning to prove the underlying protocol secure and program verification to establish security at the application level. Those two tasks are notoriously difficult and require distinct sets of reasoning capabilities.

In this paper, we propose the CV2F* approach, which relies on three steps: 1) CryptoVerif is used to model and verify a cryptographic component 2) the CryptoVerif model is automatically extracted to F*, yielding executable code which inherits the security proved in CryptoVerif, and 3) this code is then used as an external library for a wider F* implementation, enabling the proof of security guarantees on the entire system. To demonstrate the usefulness of the approach, we use CV2F* to prove message authentication at the level of the Sesame application layer by relying on message authentication in the underlying secure channel. As part of this process, we identify two unknown key-share attacks breaking authentication of Signal Messenger, which we reported and were fixed upstream, and propose two variants of the protocol provably providing authentication.

Bibtex


@INPROCEEDINGS{BlanchetFromherzetalCCS26,
  AUTHOR = {Bruno Blanchet and Aymeric Fromherz and Charlie Jacomme and Benjamin Lipp and Emmanuel Mera},
  TITLE = {CV2F*: Combining CryptoVerif and F* for Proving Security of Protocol Implementations},
  BOOKTITLE = {Proceedings of the 2026 ACM SIGSAC Conference on Computer and Communications Security, CCS 2026},
  YEAR = {2026},
  OPTPAGES = {},
  MONTH = NOV,
  PUBLISHER = {ACM Press},
  NOTE = {To appear}
}

E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)