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

[PDF] [HTML] 

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