Computational soundness of observational equivalence

Many security properties are naturally expressed as indistinguishability between two versions of a protocol. In this paper, we show that computational proofs of indistinguishability can be considerably simplified, for a class of processes that covers most existing protocols. More precisely, we show a soundness theorem, following the line of research launched by Abadi and Rogaway in 2000: computational indistinguishability in presence of an active attacker is implied by the observational equivalence of the corresponding symbolic processes. We prove our result for symmetric encryption, but the same techniques can be applied to other security primitives such as signatures and public-key encryption. The proof requires

• Type: Conference
• Year: 2008
• Where: CCS
• Authors: Hubert Comon-Lundh, Véronique Cortier
• Keywords: CCS 2008, Computational Proofs, Corresponding Symbolic Processes, Many Security Properties, Security Privacy