Deciding knowledge in security protocols for monoidal equational theories.

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 (UMR 6174), 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 used: deducibility and indistinguishability. Only few results have been obtained (in an ad-hoc way) for equational theories with associative and commutative properties, especially in the case of static equivalence. The main contribution of this paper is to propose a general setting for solving deducibility and indistinguishability for an important class (called monoidal ) of these theories. Our setting relies on the correspondence between a monoidal theory E and a semiring SE which allows us to give an algebraic characterization of the deducibility and indistinguishability problems. As a consequence we recover easily existing decidability results and obtain several new ones.
Type de document :
Communication dans un congrès
14th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR'07, Oct 2007, Yerevan, Armenia. 2007
Liste complète des métadonnées

https://hal.inria.fr/inria-00181606
Contributeur : Véronique Cortier <>
Soumis le : mercredi 24 octobre 2007 - 10:34:39
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

  • HAL Id : inria-00181606, version 1

Citation

Véronique Cortier, Stéphanie Delaune. Deciding knowledge in security protocols for monoidal equational theories.. 14th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning - LPAR'07, Oct 2007, Yerevan, Armenia. 2007. 〈inria-00181606〉

Partager

Métriques

Consultations de la notice

192