Adaptive Soundness of Static Equivalence
Steve Kremer and Laurent Mazaré. Adaptive Soundness of Static Equivalence. In Proceedings of the 12th European Symposium on Research in Computer Security (ESORICS'07), pp. 610–625, Lecture Notes in Computer Science 4734, Springer, Dresden, Germany, September 2007.
doi:10.1007/978-3-540-74835-9_40
Download
[PDF] [PDF (long version)] [HTML]
Abstract
We define a framework to reason about implementations of equational theories in the presence of an adaptive adversary. We particularly focus on soundess of static equivalence. We illustrate our framework on several equational theories: symmetric encryption, XOR, modular exponentiation and also joint theories of encryption and modular exponentiation. This last example relies on a combination result for reusing proofs for the separate theories. Finally, we define a model for symbolic analysis of dynamic group key exchange protocols, and show its computational soundness.
BibTeX
@inproceedings{KM-esorics07,
abstract = {We define a framework to reason about implementations
of equational theories in the presence of an adaptive
adversary. We particularly focus on soundess of
static equivalence. We illustrate our framework on
several equational theories: symmetric encryption,
XOR, modular exponentiation and also joint theories
of encryption and modular exponentiation. This last
example relies on a combination result for reusing
proofs for the separate theories. Finally, we~define
a model for symbolic analysis of dynamic group key
exchange protocols, and show its computational
soundness.},
address = {Dresden, Germany},
author = {Kremer, Steve and Mazar{\'e}, Laurent},
booktitle = {{P}roceedings of the 12th {E}uropean {S}ymposium on
{R}esearch in {C}omputer {S}ecurity ({ESORICS}'07)},
DOI = {10.1007/978-3-540-74835-9_40},
editor = {Biskup, Joachim and Lopez, Javier},
month = sep,
pages = {610-625},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Adaptive Soundness of Static Equivalence},
volume = {4734},
year = {2007},
acronym = {{ESORICS}'07},
nmonth = {9},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KM-esorics07.pdf},
}