DROPS

Document

DOI: 10.4230/LIPIcs.STACS.2011.29

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

Authors: Hubert Comon-Lundh and Véronique Cortier

Published in: LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 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.

Cite as

Hubert Comon-Lundh and Véronique Cortier. How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones.. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 29-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{comonlundh_et_al:LIPIcs.STACS.2011.29,
  author =	{Comon-Lundh, Hubert and Cortier, V\'{e}ronique},
  title =	{{How to prove security of communication protocols? 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 =	{Schwentick, Thomas and D\"{u}rr, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.29},
  URN =		{urn:nbn:de:0030-drops-29993},
  doi =		{10.4230/LIPIcs.STACS.2011.29},
  annote =	{Keywords: verification, security, cryptography}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2008.1766

About models of security protocols

Authors: Hubert Comon-Lundh

Published in: LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008)

Abstract

In this paper, mostly consisting of definitions, we revisit the models of security protocols: we show that the symbolic and the computational models (as well as others) are instances of a same generic model. Our definitions are also parametrized by the security primitives, the notion of attacker and, to some extent, the process calculus.

Cite as

Hubert Comon-Lundh. About models of security protocols. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 352-356, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{comonlundh:LIPIcs.FSTTCS.2008.1766,
  author =	{Comon-Lundh, Hubert},
  title =	{{About  models of security protocols}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{352--356},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1766},
  URN =		{urn:nbn:de:0030-drops-17662},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1766},
  annote =	{Keywords: Protocols, security, concurrency, formal methods}
}

Search Results

Documents authored by Comon-Lundh, Hubert

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

Abstract

Cite as

About models of security protocols

Abstract

Cite as

Thanks for your feedback!

Could not send message