Towards a Quantitative Analysis of Security Protocols (joint work with Paulo Mateus, Tiago Reis and Luca Viganò)
Electronic Notes in Theoretical Computer Science, 164(3):3-25, 2006. © Elsevier.

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.

Category / Keywords. Security protocols, Dolev-Yao intruder, probabilistic intruder, symbolic protocol analysis, computational protocol analysis.

Publication Info. Preliminary version presented at the 4th Workshop on Quantitative Aspects of Programming Languages (QAPL). Affiliated Workshop of ETAPS'06, Vienna, Austria, April 1-2 2006.

Date: 19 May 2006.

Get a preprint: PDF | PS | BibTeX Citation.
Get it from the publisher's website.