Deciding Knowledge in Security Protocols for Monoidal Equational Theories

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 ...

• Type: Conference
• Year: 2007
• Where: LPAR
• Authors: Véronique Cortier, Stéphanie Delaune
• Keywords: Artificial Intelligence, Cryptographic Functions, Equational Theories, Equational Theory, LPAR 2007