Computational soundness of observational equivalence

Computational soundness of observational equivalence. Hubert Comon-Lundh and Véronique Cortier. Rapport de recherche RR-6508, INRIA, 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. Up to our knowledge, the only result of this kind is Adao and Fournet, in which, however, cryptographic primitives are not part of the syntax. Otherwise, previous works either considered a passive attacker, or, in case of active attackers, proved a soundness result for properties that can be defined on execution traces of the protocol. Anonymity for instance does not fall in the latter category. 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

@techreport{COMONLUNDH:2008:INRIA-00274158:2,
    hal_id = {inria-00274158},
    title = {{Computational soundness of observational equivalence}},
    author = {Comon-Lundh, Hubert and Cortier, V{\'e}ronique},
    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. Up to our knowledge, the only result of this kind is Adao and Fournet, in which, however, cryptographic primitives are not part of the syntax. Otherwise, previous works either considered a passive attacker, or, in case of active attackers, proved a soundness result for properties that can be defined on execution traces of the protocol. Anonymity for instance does not fall in the latter category. 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.}},
    keywords = {computational soundness; cryptographic protocols; verification; communicating processes},
    language = {Anglais},
    affiliation = {Laboratoire Sp{\'e}cification et V{\'e}rification [Cachan] - LSV , Research Center for Information Security - RCIS , CASSIS - INRIA Lorraine - LORIA / LIFC},
    pages = {36},
    type = {Rapport de recherche},
    institution = {INRIA},
    number = {RR-6508},
    year = {2008},
}