Skip to Main content Skip to Navigation
Conference papers

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
Contributor : Véronique Cortier <>
Submitted on : Wednesday, October 24, 2007 - 10:34:39 AM
Last modification on : Wednesday, October 14, 2020 - 4:02:57 AM


  • HAL Id : inria-00181606, version 1


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⟩



Record views