License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2011.29
URN: urn:nbn:de:0030-drops-29993
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/2999/
Go to the corresponding LIPIcs Volume Portal

Comon-Lundh, Hubert ; Cortier, Véronique

How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones.

pdf-format:
7.pdf (0.6 MB)

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 - Entry

@InProceedings{comonlundh_et_al:LIPIcs:2011:2999,
  author =	{Hubert Comon-Lundh and V{\'e}ronique Cortier},
  title =	{{How to prove security of communication protocolsl A discussion on the soundness of formal models w.r.t. computational ones.}},
  booktitle =	{28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011) },
  pages =	{29--44},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-25-5},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{9},
  editor =	{Thomas Schwentick and Christoph D{\"u}rr},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/2999},
  URN =		{urn:nbn:de:0030-drops-29993},
  doi =		{10.4230/LIPIcs.STACS.2011.29},
  annote =	{Keywords: verification, security, cryptography}
}

Keywords: verification, security, cryptography
Collection: 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)
Issue Date: 2011
Date of publication: 11.03.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI