Véronique Cortier and Stéphanie Delaune. Deciding Knowledge in Security Protocols for Monoidal Equational Theories. In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07), pp. 196–210, Lecture Notes in Artificial Intelligence 4790, Springer, Yerevan, Armenia, October 2007.
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 \(S_E\) 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.
@inproceedings{CD-lpar07,
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~{\(S_E\)} 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.},
address = {Yerevan, Armenia},
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'07)},
OPTDOI = {10.1007/978-3-540-75560-9_16},
editor = {Dershowitz, Nachum and Voronkov, Andrei},
month = oct,
pages = {196-210},
publisher = {Springer},
series = {Lecture Notes in Artificial Intelligence},
title = {Deciding Knowledge in Security Protocols for Monoidal
Equational Theories},
volume = {4790},
year = {2007},
acronym = {{LPAR}'07},
nmonth = {10},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}