Decidability and combination results for two notions of knowledge in security protocols.

Véronique Cortier 1, 2 Stéphanie Delaune 3
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic functions (encryption, exclusive or, . . . ). The analysis of cryptographic protocols requires a precise understanding of the attacker knowledge. Two standard notions are usually considered: deducibility and indistinguishability. Those notions are well-studied and several decidability results already exist to deal with a variety of equational theories. Most of the existing results are dedicated to specific equational theories and only few results, especially in the case of indistinguishability, have been obtained for equational theories with associative and commutative properties (AC). In this paper, we show that existing decidability results can be easily combined for any disjoint equational theories: if the deducibility and indistinguishability relations are decidable for two disjoint theories, they are also decidable for their union. We also propose a general setting for solving deducibility and indistinguishability for an important class (called monoidal ) of equational theories involving AC operators. As a consequence of these two results, new decidability and complexity results can be obtained for many relevant equational theories.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2012, 48 (October), pp.441-487. 〈10.1007/s10817-010-9208-8〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00525778
Contributeur : Véronique Cortier <>
Soumis le : mardi 12 octobre 2010 - 16:48:11
Dernière modification le : jeudi 11 janvier 2018 - 06:24:26

Identifiants

Citation

Véronique Cortier, Stéphanie Delaune. Decidability and combination results for two notions of knowledge in security protocols.. Journal of Automated Reasoning, Springer Verlag, 2012, 48 (October), pp.441-487. 〈10.1007/s10817-010-9208-8〉. 〈inria-00525778〉

Partager

Métriques

Consultations de la notice

223