BlanchetBoutryetalCSF24
Bruno Blanchet
Back to publications
Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, and
Pierre-Yves Strub.
CV2EC: Getting the Best of Both Worlds.
In Proceedings of the 37th IEEE Computer Security
Foundations Symposium (CSF'24), pages 279-294, Enschede, The
Netherlands, July 2024. IEEE.
Get the paper
.pdf, 531 Kb
Links
Case studies
Abstract
We define and implement CV2EC, a translation from CryptoVerif assumptions on primitives to EasyCrypt games.
CryptoVerif and EasyCrypt are two proof tools for mechanizing game-based proofs.
While CryptoVerif is primarily suited for verifying security protocols,
EasyCrypt has the expressive power for verifying cryptographic primitives and schemes.
CV2EC allows us to prove security protocols in CryptoVerif
and then use EasyCrypt to prove the assumptions made in CryptoVerif,
either directly or by reducing them to lower-level or more standard cryptographic assumptions.
We apply this approach to several case studies:
we prove the multikey computational and gap Diffie-Hellman assumptions used in CryptoVerif from the standard version of these assumptions;
we also prove an n-user security property of authenticated key encapsulation mechanisms (KEMs), used in the CryptoVerif study of hybrid public-key encryption (HPKE), from the 2-user version.
By doing that, we discovered errors in the paper proof of this property, which we reported to the authors who then fixed their proof.
Bibtex
@INPROCEEDINGS{BlanchetBoutryetalCSF24,
AUTHOR = {Bruno Blanchet and Pierre Boutry and Christian Doczkal and Benjamin Grégoire and Pierre-Yves Strub},
TITLE = {{CV2EC}: Getting the Best of Both Worlds},
BOOKTITLE = {{P}roceedings of the 37th {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'24)},
YEAR = {2024},
PUBLISHER = {{IEEE}},
ADDRESS = {Enschede, The Netherlands},
PAGES = {279--294},
MONTH = JUL
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)