@article{Adão20063,
title = "Towards a Quantitative Analysis of Security Protocols",
journal = "Electronic Notes in Theoretical Computer Science",
volume = "164",
number = "3",
pages = "3 - 25",
year = "2006",
note = "<ce:title>Proceedings of the 4th International Workshop on Quantitative Aspects of Programming Languages (QAPL 2006)</ce:title> <xocs:full-name>Quantitative Aspects of Programming Languages 2006</xocs:full-name>",
issn = "1571-0661",
doi = "10.1016/j.entcs.2006.07.009",
url = "http://www.sciencedirect.com/science/article/pii/S1571066106004889",
author = "Pedro Adão and Paulo Mateus and Tiago Reis and Luca Viganò",
keywords = "Security protocols",
keywords = "Dolev-Yao intruder",
keywords = "probabilistic intruder",
keywords = "symbolic protocol analysis",
keywords = "computational protocol analysis",
abstract = "This paper contributes to further closing the gap between formal analysis and concrete implementations of security protocols by introducing a quantitative extension of the usual Dolev-Yao intruder model. This extended model provides a basis for considering protocol attacks that are possible when the intruder has a reasonable amount of computational power, in particular when he is able, with a certain probability, to guess encryption keys or other particular kind of data such as the body of a hashed message. We also show that these extensions do not augment the computational complexity of the protocol insecurity problem in the case of a finite number of interleaved protocol sessions."
}