BlanchetJacommeCSF24

Bruno Blanchet Back to publications

Bruno Blanchet and Charlie Jacomme. Post-quantum sound CryptoVerif and verification of hybrid TLS and SSH key-exchanges. In Proceedings of the 37th IEEE Computer Security Foundations Symposium (CSF'24), pages 543-556, Enschede, The Netherlands, July 2024. IEEE.

Get the paper

.pdf, 401 Kb

Abstract

With the potential arrival of quantum computers, communication protocols are now being updated at a fast pace to be secure even against attackers with access to such a computer. A core issue is that we need to update the existing tools used to verify security protocols, as classical security proofs do not always carry over to quantum attackers.

In this work, we prove the post-quantum soundness of the CryptoVerif prover, a tool used to semi-automatically obtain computational security guarantees over cryptographic constructions. It required an update of the whole semantics in order to define it for any black-box interactive attacker and not just probabilistic Turing machines. We also had to validate the soundness of all its proof techniques, the so-called game transformations.

We used this new post-quantum sound CryptoVerif to obtain the first formal security guarantees over two IETF draft proposals designing post-quantum variants of SSH and TLS.

Bibtex


@INPROCEEDINGS{BlanchetJacommeCSF24,
  AUTHOR = {Bruno Blanchet and Charlie Jacomme},
  TITLE = {Post-quantum sound {CryptoVerif} and verification of hybrid {TLS} and {SSH} key-exchanges},
  BOOKTITLE = {{P}roceedings of the 37th {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'24)},
  YEAR = 2024,
  PAGES = {543--556},
  MONTH = JUL,
  PUBLISHER = {{IEEE}},
  ADDRESS = {Enschede, The Netherlands}
}

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