Verification of Security Protocols

Verification of Security Protocols. Véronique Cortier. In 10th Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09), pp. 5–13, Lecture Notes in Computer Science 5403, Springer, Savanah, USA, January 2009. (Invited Tutorial).

Download

[PDF] [HTML]

Abstract

Security protocols are short programs aiming at securing communications over a network. They are widely used in our everyday life. Their verification using symbolic models has shown its interest for detecting attacks and proving security properties. In particular, several automatic tools have been developed. However, the guarantees that the symbolic approach offers have been quite unclear compared to the computational approach that considers issues of complexity and probability. This later approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks.
In this tutorial, we will first overview several techniques used for symbolically verifying security protocols. In a second part of the presentation, we will present recent results that aim at obtaining the best of both worlds: fully automated proofs and strong, clear security guarantees. The approach consists in proving that symbolic models are sound with respect to computational ones, that is, that any potential attack is indeed captured at the symbolic level.

BibTeX

@InProceedings{VMCAI09,
  author = 	 {V{\'e}ronique Cortier},
  title = 	 {Verification of Security Protocols},
  booktitle = {10th Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09)},
  pages = 	 {5-13},
  year = 	 {2009},
  volume = 	 {5403},
  series = 	 {Lecture Notes in Computer Science},
  address = 	 {Savanah, USA},
  month = 	 {January},
  publisher = {Springer},
  abstract = {Security protocols are short programs aiming at securing
communications over a network. They are widely used in our everyday
life. Their verification using symbolic models has shown its interest
for detecting attacks and proving security properties. In particular,
several automatic tools have been developed. However, the guarantees
that the symbolic approach offers have been quite unclear compared to
the computational approach that considers issues of complexity and
probability. This later approach captures a strong notion of security,
guaranteed against all probabilistic polynomial-time attacks. 
\par
In this tutorial, we will first overview several techniques used for
symbolically verifying security protocols. In a second part of the
presentation, we will present recent results that aim at obtaining
the best of both worlds: fully automated proofs and strong, clear security
guarantees. The approach consists in proving that symbolic models are
sound with respect to computational ones, that is, that any
potential attack is indeed captured at the symbolic level.
},
  doi =           {10.1007/978-3-540-93900-9_5},
  note = {(Invited Tutorial)},
}