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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Kremer, S., & Mazaré, L. (2007). Adaptive soundness of static equivalence. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4734 LNCS, pp. 610–625). Springer Verlag. https://doi.org/10.1007/978-3-540-74835-9_40
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
