BlanchetCSF24

Bruno Blanchet Back to publications

Bruno Blanchet. Dealing with Dynamic Key Compromise in CryptoVerif. In Proceedings of the 37th IEEE Computer Security Foundations Symposium (CSF'24), Enschede, The Netherlands, July 2024. IEEE. To appear.

Get the paper

.pdf, 409 Kb

Links

Case studies

Abstract

CryptoVerif is a mechanized security protocol verifier sound in the computational model. In this paper, we explore and extend its treatment of dynamic key compromise. First, we present a basic treatment of compromise and explain its limitations. Next, we introduce several extensions in order to remove these limitations: improved proof of secrecy; building different proofs for the various properties to prove; removing code that cannot be executed when the adversary breaks the desired security properties; and guessing tested sessions, values, and branches. We illustrate how these extensions improve the treatment of key compromise on protocols ranging from toy examples to filling gaps in previous large case studies including TLS 1.3 and the WireGuard VPN protocol.

Bibtex


@INPROCEEDINGS{BlanchetCSF24,
  AUTHOR = {Bruno Blanchet},
  TITLE = {Dealing with Dynamic Key Compromise in {CryptoVerif}},
  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},
  OPTPAGES = {},
  MONTH = JUL,
  NOTE = {To appear}
}

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