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 metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-01206276
Contributor : Véronique Cortier <>
Submitted on : Monday, September 28, 2015 - 4:45:23 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Long-term archiving on : Tuesday, December 29, 2015 - 10:52:33 AM

File

CCD-csf15.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

364

Files downloads

158