Véronique Cortier and Stéphanie Delaune. Decidability and combination results for two notions of knowledge in security protocols. Journal of Automated Reasoning, 48(4):441–487, Springer, April 2012.
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 considered: deducibility and indistinguishability. Those notions are well-studied and several decidability results already exist to deal with a variety of equational theories. Most of the existing results are dedicated to specific equational theories and only few results, especially in the case of indistinguishability, have been obtained for equational theories with associative and commutative properties (AC).
In this paper, we show that existing decidability results can be easily combined for any disjoint equational theories: if the deducibility and indistinguishability relations are decidable for two disjoint theories, they are also decidable for their union. We also propose a general setting for solving deducibility and indistinguishability for an important class (called monoidal) of equational theories involving AC operators.
As a consequence of these two results, new decidability and complexity results can be obtained for many relevant equational theories.
@article{CD-jar10,
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
considered: deducibility and indistinguishability.
Those notions are well-studied and several
decidability results already exist to deal with a
variety of equational theories. Most of the existing
results are dedicated to specific equational theories
and only few results, especially in the case of
indistinguishability, have been obtained for
equational theories with associative and commutative
properties~(AC).\par In this paper, we show that
existing decidability results can be easily combined
for any disjoint equational theories: if the
deducibility and indistinguishability relations are
decidable for two disjoint theories, they are also
decidable for their union. We also propose a general
setting for solving deducibility and
indistinguishability for an important class (called
\emph{monoidal}) of equational theories involving AC
operators.\par As a consequence of these two results,
new decidability and complexity results can be
obtained for many relevant equational theories.},
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
OPTDOI = {10.1007/s10817-010-9208-8},
journal = {Journal of Automated Reasoning},
month = apr,
number = {4},
pages = {441-487},
publisher = {Springer},
title = {Decidability and combination results for two notions
of knowledge in security protocols},
volume = {48},
year = {2012},
nmonth = {4},
lsv-category = {jour},
wwwpublic = {public and ccsb},
}