Computational Soundness of Observational Equivalence

Computational Soundness of Observational Equivalence. Hubert Comon-Lundh and Véronique Cortier. In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS'08), pp. 109–118, ACM Press, Alexandria, Virginia, USA, October 2008.

Download

[PDF] [HTML]

Abstract

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 the introduction of new concepts, which are general and can be reused in other settings.

BibTeX

@inproceedings{CLC-CCS2008,
  address =       {Alexandria, Virginia, USA},
  author =        {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique},
  booktitle =     {{P}roceedings of the 15th {ACM} {C}onference on
                   {C}omputer and {C}ommunications {S}ecurity
                   ({CCS}'08)},
  month =         oct,
  pages =         {109-118},
  publisher =     {ACM Press},
  title =         {Computational Soundness of Observational Equivalence},
  year =          {2008},
  abstract =      {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 the introduction of
                   new concepts, which are general and can be reused in
                   other settings.},
  doi =           {10.1145/1455770.1455786},
}