Mathilde Arnaud, Véronique Cortier, and Stéphanie Delaune. Combining algorithms for deciding knowledge in security protocols. In Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS'07), pp. 103–117, Lecture Notes in Artificial Intelligence 4720, Springer, Liverpool, UK, September 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. Those notions are well-studied and a lot of decidability results already exist to deal with a variety of equational theories.
We show that 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. As an application, new decidability results can be obtained using this combination theorem.
@inproceedings{ACD-frocos07,
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. Those notions
are well-studied and a lot of decidability results
already exist to deal with a variety of equational
theories.\par We~show that 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. As~an application, new decidability results
can be obtained using this combination theorem.},
address = {Liverpool, UK},
author = {Arnaud, Mathilde and Cortier, V{\'e}ronique and
Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {F}rontiers of {C}ombining {S}ystems
({FroCoS}'07)},
OPTDOI = {10.1007/978-3-540-74621-8_7},
editor = {Wolter, Franck},
month = sep,
pages = {103-117},
publisher = {Springer},
series = {Lecture Notes in Artificial Intelligence},
title = {Combining algorithms for deciding knowledge in
security protocols},
volume = {4720},
year = {2007},
acceptrate = {14/31},
acronym = {{FroCoS}'07},
nmonth = {9},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}