Sciweavers

ASIAN
2006
Springer

Computational Soundness of Formal Indistinguishability and Static Equivalence

13 years 9 months ago
Computational Soundness of Formal Indistinguishability and Static Equivalence
In the investigation of the relationship between the formal and the computational view of cryptography, a recent approach, first proposed in [10], uses static equivalence from cryptographic pi calculi as a notion of formal indistinguishability. Previous work [10, 1] has shown that this yields the soundness of natural interpretations of some interesting equational theories, such as certain cryptographic operations and a theory of XOR. In this paper however, we argue that static equivalence is too coarse to allow sound interpretations of many natural and useful equational theories. We illustrate this with several explicit examples in which static equivalence fails to work. To fix the problem, we propose a notion of formal indistinguishability that is more flexible than static equivalence. We provide a general framework along with general theorems, and then discuss how this new notion works for the explicit examples where static equivalence fails to ensure soundness.
Gergei Bana, Payman Mohassel, Till Stegers
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ASIAN
Authors Gergei Bana, Payman Mohassel, Till Stegers
Comments (0)