Computationally Sound, Automated Proofs for Security Protocols

Computationally Sound, Automated Proofs for Security Protocols. V. Cortier and B. Warinschi. In Proceedings of the 14th European Symposium on Programming (ESOP'05), pp. 157–171, Lecture Notes in Computer Science 3444, Springer, Edinburgh, U.K, April 2005.

Download

[PDF] [PS] [HTML]

Abstract

Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs. However, the guarantees that it offers have been quite unclear.
In this paper, we show that it is possible to obtain the best of both worlds: fully automated proofs and strong, clear security guarantees. Specifically, for the case of protocols that use signatures and asymmetric encryption, we establish that symbolic integrity and secrecy proofs are sound with respect to the computational model. The main new challenges concern secrecy properties for which we obtain the first soundness result for the case of active adversaries. Our proofs are carried out using Casrul, a fully automated tool.

BibTeX

@INPROCEEDINGS{CortierW-ESOP05,
  AUTHOR = {Cortier, V. and Warinschi, B.},
  TITLE = {Computationally Sound, Automated Proofs for Security Protocols},
  BOOKTITLE = {Proceedings of the 14th European Symposium on Programming (ESOP'05)},
  ADDRESS = {Edinburgh, U.K},
  MONTH = {April},
  PAGES = {157-171},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {3444},
  YEAR = {2005},
  abstract = {Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs. However, the guarantees that it offers have been quite unclear.
\par
In this paper, we show that it is possible to obtain the best of both worlds: fully automated proofs and strong, clear security guarantees. Specifically, for the case of protocols that use signatures and asymmetric encryption, we establish that symbolic integrity and secrecy proofs are sound with respect to the computational model. The main new challenges concern secrecy properties for which we obtain the first soundness result for the case of active adversaries. Our proofs are carried out using Casrul, a fully automated tool.},
  doi =           {10.1007/978-3-540-31987-0_12},
}