We present an automatic, terminating method for verifying confidentiality properties, and to a lesser extent freshness properties of cryptographic protocols. It is based on a safe abstract interpretation of cryptographic protocols using a specific extension of tree automata, V-parameterized tree automata, which mix automata-theoretic techniques with deductive features. Contrary to most model-checking approaches, this method offers actual security guarantees. It owes much to D. Bolignano's ways of modeling cryptographic protocols and to D. Monniaux' seminal idea of using tree automata to verify cryptographic protocols by abstract interpretation. It extends the latter by adding new deductive abilities, and by offering the possibility of analyzing protocols in the presence of parallel multi-session principals, following some ideas by M. Debbabi, M. Mejri, N. Tawbi, and I. Yahmadi. © 2000 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Goubault-Larrecq, J. (2000). A method for automatic cryptographic protocol verification (extended abstract). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1800 LNCS, pp. 977–984). Springer Verlag. https://doi.org/10.1007/3-540-45591-4_134
Mendeley helps you to discover research relevant for your work.