A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems

A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems. Véronique Cortier, Steve Kremer, and Bogdan Warinschi. Journal of Automated Reasoning, 46(3-4):225–259, Springer, April 2010.

Download

[PDF] [HTML] 

Abstract

Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs. However, the guarantees that it offers with respect to the more detailed computational models have been quite unclear.
For more than twenty years the two approaches have coexisted but evolved mostly independently. Recently, significant research efforts attempt to develop paradigms for cryptographic systems analysis that combines the best of both worlds. There are two broad directions that have been followed. Computational soundness aims to establish sufficient conditions under which results obtained using symbolic models imply security under computational models. The direct approach aims to apply the principles and the techniques developed in the context of symbolic models directly to computational ones.
In this paper we survey existing results along both of these directions. Our goal is to provide a rather complete summary that could act as a quick reference for researchers who want to contribute to the field, want to make use of existing results, or just want to get a better picture of what results already exist.

BibTeX

@article{SurveySoundnessJAR,
  author =        {Cortier, V{\'e}ronique and Kremer, Steve and
                   Warinschi, Bogdan},
  journal =       {Journal of Automated Reasoning},
  month =         apr,
  number =        {3-4},
  pages =         {225-259},
  publisher =     {Springer},
  title =         {A~Survey of Symbolic Methods in Computational
                   Analysis of Cryptographic Systems},
  volume =        {46},
  year =          {2010},
  abstract =      {Since the 1980s, two approaches have been developed
                   for analyzing security protocols. One of the
                   approaches relies on a computational model that
                   considers issues of complexity and probability. This
                   approach captures a strong notion of security,
                   guaranteed against all probabilistic polynomial-time
                   attacks. The other approach relies on a symbolic
                   model of protocol executions in which cryptographic
                   primitives are treated as black boxes. Since the
                   seminal work of Dolev and Yao, it has been realized
                   that this latter approach enables significantly
                   simpler and often automated proofs. However, the
                   guarantees that it offers with respect to the more
                   detailed computational models have been quite
                   unclear.\par For more than twenty years the two
                   approaches have coexisted but evolved mostly
                   independently. Recently, significant research efforts
                   attempt to develop paradigms for cryptographic
                   systems analysis that combines the best of both
                   worlds. There are two broad directions that have been
                   followed. Computational soundness aims to establish
                   sufficient conditions under which results obtained
                   using symbolic models imply security under
                   computational models. The direct approach aims to
                   apply the principles and the techniques developed in
                   the context of symbolic models directly to
                   computational ones.\par In this paper we survey
                   existing results along both of these directions. Our
                   goal is to provide a rather complete summary that
                   could act as a quick reference for researchers who
                   want to contribute to the field, want to make use of
                   existing results, or just want to get a better
                   picture of what results already exist.},
  doi =           {10.1007/s10817-010-9187-9},
}