How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones
How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones. Hubert Comon-Lundh and Véronique Cortier. In Proceedings of the 28th Annual Symposium on Theoretical Aspects of Computer Science (STACS'11), pp. 29–44, Leibniz International Proceedings in Informatics 9, Leibniz-Zentrum für Informatik, Dortmund, Germany, March 2011.
Download
Abstract
Security protocols are short programs that aim at securing communication over a public network. Their design is known to be error-prone with flaws found years later. That is why they deserve a careful security analysis, with rigorous proofs. Two main lines of research have been (independently) developed to analyse the security of protocols. On the one hand, formal methods provide with symbolic models and often automatic proofs. On the other hand, cryptographic models propose a tighter modeling but proofs are more difficult to write and to check. An approach developed during the last decade consists in bridging the two approaches, showing that symbolic models are sound w.r.t. symbolic ones, yielding strong security guarantees using automatic tools. These results have been developed for several cryptographic primitives (e.g. symmetric and asymmetric encryption, signatures, hash) and security properties. While proving soundness of symbolic models is a very promising approach, several technical details are often not satisfactory. Focusing on symmetric encryption, we describe the difficulties and limitations of the available results.
BibTeX
@inproceedings{Stacs2011,
address = {Dortmund, Germany},
author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique},
booktitle = {{P}roceedings of the 28th {A}nnual {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'11)},
editor = {D{\"u}rr, Christoph and Schwentick, Thomas},
month = mar,
pages = {29-44},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {How to prove security of communication protocols?
A~discussion on the soundness of formal models w.r.t.
computational ones},
volume = {9},
year = {2011},
abstract = {Security protocols are short programs that aim at
securing communication over a public network. Their
design is known to be error-prone with flaws found
years later. That is why they deserve a careful
security analysis, with rigorous proofs. Two main
lines of research have been (independently) developed
to analyse the security of protocols. On the one
hand, formal methods provide with symbolic models and
often automatic proofs. On the other hand,
cryptographic models propose a tighter modeling but
proofs are more difficult to write and to check. An
approach developed during the last decade consists in
bridging the two approaches, showing that symbolic
models are sound w.r.t. symbolic ones, yielding
strong security guarantees using automatic tools.
These results have been developed for several
cryptographic primitives (e.g. symmetric and
asymmetric encryption, signatures, hash) and security
properties. While proving soundness of symbolic
models is a very promising approach, several
technical details are often not satisfactory.
Focusing on symmetric encryption, we describe the
difficulties and limitations of the available
results.},
doi = {10.4230/LIPIcs.STACS.2011.29},
}