Automated Security Protocol Analysis With the AVISPA Tool

被引:291
作者
Vigano, Luca [1 ]
机构
[1] Swiss Fed Inst Technol, Informat Secur Grp, Dept Comp Sci, Zurich, Switzerland
关键词
Security protocols; protocol models; automated protocol validation;
D O I
10.1016/j.entcs.2005.11.052
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
The AVISPA Tool is a push-button tool for the Automated Validation of Internet Security 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 automatic protocol analysis techniques. Experimental results, carried out on a large library of Internet security protocols, indicate that the AVISPA Tool is a state-of-the-art tool for Internet security protocol analysis as, to our knowledge, no other tool exhibits the same level of scope and robustness while enjoying the same performance and scalability.
引用
收藏
页码:61 / 86
页数:26
相关论文
共 71 条
[1]  
Abadi M, 2004, LECT NOTES COMPUT SC, V2986, P340
[2]   Reconstruction of attacks against cryptographic protocols [J].
Allamigeon, X ;
Blanchet, B .
18TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2005, :140-154
[3]  
[Anonymous], 1997, 97983 ISOIEC
[4]  
[Anonymous], 2005, AVISPA V1 0 USER MAN
[5]   Automatic compilation of protocol insecurity problems into logic programming [J].
Armando, A ;
Compagna, L ;
Lierler, Y .
LOGICS IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2004, 3229 :617-627
[6]  
Armando A, 2002, LECT NOTES COMPUT SC, V2529, P210
[7]  
Armando A., 2002, Computer Aided Verification. 14th International Conference, CAV 2002. Proceedings (Lecture Notes in Computer Science Vol.2404), P349
[8]  
Armando A, 2003, LECT NOTES COMPUT SC, V2805, P875
[9]  
Armando A., 2003, LNCS, V2919, P257
[10]   An Optimized Intruder Model for SAT-based Model-Checking of Security Protocols [J].
Armando, Alessandro ;
Compagna, Luca .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 125 (01) :91-108