Stéphanie Delaune: Checking trace equivalence: How to get rid of nonces?

Checking trace equivalence: How to get rid of nonces?

Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. Checking trace equivalence: How to get rid of nonces?. In Proceedings of the 20th European Symposium on Research in Computer Security (ESORICS'15), pp. 230–251, Lecture Notes in Computer Science, Springer, Vienna, Austria, September 2015.

Download

[PDF]

Abstract

Security protocols can be successfully analysed using formal methods. When proving security in symbolic settings for an unbounded number of sessions, a typical technique consists in abstracting away fresh nonces and keys by a bounded set of constants. While this abstraction is clearly sound in the context of secrecy properties (for protocols without else branches), this is no longer the case for equivalence properties.
In this paper, we study how to soundly get rid of nonces in the context of equivalence properties. We show that nonces can be replaced by constants provided that each nonce is associated to two constants (instead of typically one constant for secrecy properties). Our result holds for deterministic (simple) protocols and a large class of primitives that includes e.g. standard primitives, blind signatures, and zero-knowledge proofs.

BibTeX

@inproceedings{CCD-esorics15,
  abstract =      {Security protocols can be successfully analysed using
                   formal methods. When proving security in symbolic
                   settings for an unbounded number of sessions, a
                   typical technique consists in abstracting away fresh
                   nonces and keys by a bounded set of constants. While
                   this abstraction is clearly sound in the context of
                   secrecy properties (for protocols without else
                   branches), this is no longer the case for equivalence
                   properties.\par In this paper, we study how to
                   soundly get rid of nonces in the context of
                   equivalence properties. We show that nonces can be
                   replaced by constants provided that each nonce is
                   associated to two constants (instead of typically one
                   constant for secrecy properties). Our result holds
                   for deterministic (simple) protocols and a large
                   class of primitives that includes e.g. standard
                   primitives, blind signatures, and zero-knowledge
                   proofs.},
  address =       {Vienna, Austria},
  author =        {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and
                   Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 20th {E}uropean {S}ymposium on
                   {R}esearch in {C}omputer {S}ecurity ({ESORICS}'15)},
  OPTDOI =           {10.1007/978-3-319-24177-7_12},
  editor =        {Ryan, Peter and Weippl, Edgar},
  month =         sep,
  pages =         {230-251},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Checking trace equivalence: How to get rid of
                   nonces?},
  year =          {2015},
  acronym =       {{ESORICS}'15},
  nmonth =        {9},
  OPTLONGPDF =       {https://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/
                  rr-lsv-2015-07.pdf},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}