Skip to Main content Skip to Navigation
New interface
Conference papers

Decidability of trace equivalence for protocols with nonces

Rémy Chrétien 1, 2 Véronique Cortier 2 Stéphanie Delaune 1 
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Privacy properties such as anonymity, unlinkability, or vote secrecy are typically expressed as equivalence properties. In this paper, we provide the first decidability result for trace equivalence of security protocols, for an unbounded number of sessions and unlimited fresh nonces. Our class encompasses most symmetric key protocols of the literature, in their tagged variant.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download
Contributor : Véronique Cortier Connect in order to contact the contributor
Submitted on : Monday, September 28, 2015 - 4:45:23 PM
Last modification on : Friday, January 21, 2022 - 3:09:00 AM
Long-term archiving on: : Tuesday, December 29, 2015 - 10:52:33 AM


Files produced by the author(s)



Rémy Chrétien, Véronique Cortier, Stéphanie Delaune. Decidability of trace equivalence for protocols with nonces. 28th IEEE Computer Security Foundations Symposium (CSF'15), Jul 2015, Verona, Italy. ⟨10.1109/CSF.2015.19⟩. ⟨hal-01206276⟩



Record views


Files downloads