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.

• Type: Conference
• Year: 2006
• Where: ASIAN
• Authors: Gergei Bana, Payman Mohassel, Till Stegers
• Keywords: Algorithms, ASIAN 2006, Equational Theories, Static Equivalence, Uses Static Equivalence