Combining algorithms for deciding knowledge in security protocols

Mathilde Arnaud 1 Véronique Cortier 1 Stéphanie Delaune 1
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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In formal approaches, messages sent over a network are usu- ally modeled by terms together with an equational theory, axiomatiz- ing the properties of the cryptographic functions (encryption, exclusive or, . . . ). The analysis of cryptographic protocols requires a precise un- derstanding of the attacker knowledge. Two standard notions are usu- ally considered: deducibility and indistinguishability. Those notions are well-studied and several decidability results already exist to deal with a variety of equational theories. However most of the results are dedicated to specific equational theories. We show that 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. As an application, new decidability results can be obtained using this combination theorem.
Type de document :
Communication dans un congrès
6th International Symposium on Frontiers of Combining Systems - FroCoS'07, Sep 2007, Liverpool, United Kingdom. 2007
Liste complète des métadonnées

https://hal.inria.fr/inria-00181609
Contributeur : Véronique Cortier <>
Soumis le : mercredi 24 octobre 2007 - 10:37:04
Dernière modification le : jeudi 15 février 2018 - 08:48:09

Identifiants

  • HAL Id : inria-00181609, version 1

Citation

Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune. Combining algorithms for deciding knowledge in security protocols. 6th International Symposium on Frontiers of Combining Systems - FroCoS'07, Sep 2007, Liverpool, United Kingdom. 2007. 〈inria-00181609〉

Partager

Métriques

Consultations de la notice

141