Sciweavers

IANDC
2008

Symbolic protocol analysis for monoidal equational theories

13 years 3 months ago
Symbolic protocol analysis for monoidal equational theories
We are interested in the design of automated procedures for analyzing the (in)security of cryptographic protocols in the Dolev-Yao model for a bounded number of sessions when we take into account some algebraic properties satisfied by the operators involved in the protocol. This leads to a more realistic model than what we get under the perfect cryptography assumption, but it implies that protocol analysis deals with terms modulo some equational theory instead of terms in a free algebra. The main goal of this paper is to set up a general approach that works for a whole class of monoidal theories which contains many of the specific cases that have been considered so far in an ad-hoc way (e.g. exclusive or, Abelian groups, exclusive or in combination with the homomorphism axiom). We follow a classical schema for cryptographic protocol analysis which proves first a locality result and then reduces the insecurity problem to a symbolic constraint solving problem. This approach strongly rel...
Stéphanie Delaune, Pascal Lafourcade, Denis
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where IANDC
Authors Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez, Ralf Treinen
Comments (0)