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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00181606
Contributor : Véronique Cortier <>
Submitted on : Wednesday, October 24, 2007 - 10:34:39 AM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM

Identifiers

  • 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. ⟨inria-00181606⟩

Share

Metrics

Record views

270