Typing messages for free in security protocols: the~case of equivalence properties

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 untraceability, vote secrecy, or anonymity are typically expressed as behavioural equivalence in a process algebra that models security protocols. In this paper, we study how to decide one particular relation, namely trace equivalence, for an unbounded number of sessions. Our first main contribution is to reduce the search space for attacks. Specifically, we show that if there is an attack then there is one that is well-typed. Our result holds for a large class of typing systems and a large class of determinate security protocols. Assuming finitely many nonces and keys, we can derive from this result that trace equivalence is decidable for an unbounded number of sessions for a class of tagged protocols, yielding one of the first decidability results for the unbounded case. As an intermediate result, we also provide a novel decision procedure in the case of a bounded number of sessions.
Type de document :
Communication dans un congrès
25th International Conference on Concurrency Theory (CONCUR'14), Sep 2014, Rome, Italy. 2014
Liste complète des métadonnées

https://hal.inria.fr/hal-01080293
Contributeur : Véronique Cortier <>
Soumis le : mardi 4 novembre 2014 - 21:45:58
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

  • HAL Id : hal-01080293, version 1

Citation

Rémy Chrétien, Véronique Cortier, Stéphanie Delaune. Typing messages for free in security protocols: the~case of equivalence properties. 25th International Conference on Concurrency Theory (CONCUR'14), Sep 2014, Rome, Italy. 2014. 〈hal-01080293〉

Partager

Métriques

Consultations de la notice

358