Abstract
AVISPA is a push-button tool for the automated validation of Internet security-sensitive protocols and applications. It provides a modular and expressive formal language for specifying protocols and their security properties, and integrates different back-ends that implement a variety of state-of-the-art automatic analysis techniques. To the best of our knowledge, no other tool exhibits the same level of scope and robustness while enjoying the same performance and scalability.
This work was supported by the FET Open Project IST-2001-39252 and the BBW Project 02.0431, “AVISPA: Automated Validation of Internet Security Protocols and Applications” (www.avispa-project.org).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Armando, A., Basin, D., Bouallagui, M., Chevalier, Y., Compagna, L., Mödersheim, S., Rusinowitch, M., Turuani, M., Viganò, L., Vigneron, L.: The AVISS Security Protocol Analysis Tool. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 349. Springer, Heidelberg (2002)
Armando, A., Compagna, L.: SATMC: a SAT-based Model Checker for Security Protocols. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 730–733. Springer, Heidelberg (2004)
Basin, D., Mödersheim, S., Viganò, L.: OFMC: A Symbolic Model-Checker for Security Protocols. International Journal of Information Security (2004)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proc. CSFW 2001. IEEE Computer Society Press, Los Alamitos (2001)
Boichut, Y., Heam, P.-C., Kouchnarenko, O., Oehl, F.: Improvements on the Genet and Klay Technique to Automatically Verify Security Protocols. In: Proc. AVIS 2004, ENTCS (2004) (to appear)
Bozga, L., Lakhnech, Y., Perin, M.: Hermes: An Automatic Tool for the Verification of Secrecy in Security Protocols. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 219–222. Springer, Heidelberg (2003)
The CAPSL Integrated Protocol Environment, http://www.csl.sri.com/~millen/
Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., Mantovani, J., Mödersheim, S., Vigneron, L.: A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols. In: Proc. SAPS 2004. Austrian Computer Society (2004)
Chevalier, Y., Vigneron, L.: Automated Unbounded Verification of Security Protocols. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 324. Springer, Heidelberg (2002)
Clark, J., Jacob, J.: A Survey of Authentication Protocol Literature: Version 1.0, 17. November (1997), http://www.cs.york.ac.uk/~jac/papers/drareview.ps.gz
Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. In: Proc. CSFW 2000. IEEE Computer Society Press, Los Alamitos (2000)
Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)
Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security 6(1), 85–128 (1998)
Song, D.: Athena: A new efficient automatic checker for security protocol analysis. In: Proc. CSFW 1999. IEEE Computer Society Press, Los Alamitos (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armando, A. et al. (2005). The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_27
Download citation
DOI: https://doi.org/10.1007/11513988_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)