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
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},
}