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. In Proceedings of the 20th European Symposium on Research in Computer Security (ESORICS'15), Lecture Notes in Computer Science, Springer, Vienna, Austria, 2015.

Download

[PDF] [HTML]

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,
  	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)},
  	publisher =	{Springer},
  	series =	{Lecture Notes in Computer Science},
  	title =	{Checking trace equivalence: How to get rid of nonces?},
  	year =	{2015},
	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.},
  doi = {10.1007/978-3-319-24177-7_12},
}