Checking trace equivalence: how to get rid of nonces? (English) Zbl 1499.68048

Chrétien, Rémy; Cortier, Véronique; Delaune, Stéphanie

Pernul, Günther (ed.) et al., Computer security – ESORICS 2015. 20th European symposium on research in computer security, Vienna, Austria, September 21–25, 2015, Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 9327, 230-251 (2015).

Summary: 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.
For the entire collection see [Zbl 1492.68027].

MSC:

68M25	Computer security
94A60	Cryptography