ChevalRakotonirinaCSF23

Back to ProVerif

Vincent Cheval and Itsaka Rakotonirina. Indistinguishability Beyond Diff-Equivalence in ProVerif. In Proceedings of the 36th IEEE Computer Security Foundations Symposium (CSF'23), pages 184-199, Dubrovnik, Croatia, July 2023. IEEE. Distinguished paper award. Tool feature Case study

Get the paper

.pdf, 459 Kb

Links

Long version

Abstract

When formalising cryptographic protocols, privacy-type properties such as strong flavours of secrecy, anonymity or unlinkability, are often modelled by indistinguishability statements. Proving them is notoriously more challenging than trace properties which benefit from a well-established tool support today. State-of-the-art techniques often exhibit significant limitations, e.g., consider only a bounded number of protocol sessions, or prove diff-equivalence-a fine-grained, structure-guided notion of indistinguishability that commonly yields unnecessarily pessimistic analyses. In this paper, we design, implement and evaluate the first general framework for proving indistinguishability properties, for an unbounded number of protocol sessions, going beyond the scope of diff-equivalence. For that we relax the structural requirements of ProVerif, a state-of-the-art tool, through a notion of session decomposition, intuitively allowing a dynamic restructuration of the proofs. We can then verify in a modular way various, more realistic models of indistinguishability such as may-testing equivalence, by exhibiting for each relation a sufficient condition on ProVerif's output ensuring that it holds. We implement our approach into a prototype and showcase the gain in scope through several case studies.

Bibtex


@INPROCEEDINGS{ChevalRakotonirinaCSF23,
  AUTHOR = {Cheval, Vincent and Rakotonirina, Itsaka},
  TITLE = {Indistinguishability Beyond Diff-Equivalence in {P}ro{V}erif},
  BOOKTITLE = {{P}roceedings of the 36th {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'23)},
  YEAR = {2023},
  PUBLISHER = {{IEEE}},
  ADDRESS = {Dubrovnik, Croatia},
  PAGES = {184--199},
  MONTH = JUL,
  NOTE = {{\bfseries Distinguished paper award}}
}