Avispa Tool Documentation

The HLPSL Tutorial
A Beginner's Guide to Modelling and Analysing Internet Security Protocols
Download (pdf).

AVISPA v1.1 User Manual
Download (pdf).

Publicly Available Project Deliverables

(Please note that deliverables 2.1 and 2.3 refer to a version of HLPSL and IF which is not the most recent one. For the most up-to-date and stable version of HLPSL and IF please refer to the documentation included in the Avispa Package)

Deliverable 2.1:
The High Level Protocol Specification Language,
Download (pdf).

Deliverable 2.3:
The Intermediate Format,
Download (pdf).

Deliverable 6.1:
List of selected problems,
Download (ps).

Deliverable 6.2:
Specification of the Problems in the High Level Specification Language,
Download (pdf).

Scientific papers

    2006

  1. M. Abadi, V. Cortier, Deciding knowledge in security protocols under equational theories. Theoretical Computer Science. To appear.

  2. A. Armando, D. Basin, J. Cuellar, M. Rusinowitch, L. Viganò, editors, Special Issue of the Journal of Automated Reasoning on Automated Reasoning for Security Protocol Analysis, Elsevier Science. To appear.

  3. M. Backes, A. Datta, A. Derek, J.C. Mitchell, M. Turuani, Compositional Analysis of Contract Signing Protocols. Theoretical Computer Science. To appear.

  4. M. Backes, S. Mödersheim, B. Pfitzmann, L. Viganò, Symbolic and Cryptographic Analysis of the Secure WS-ReliableMessaging Scenario. Proceedings of Fossacs 2006, LNCS 3921:428--445, Springer. download

  5. Y. Boichut, Th. Genet, Feasible Trace Reconstruction for Rewriting Approximations. Proceedings of RTA'06, 2006. download

  6. Y. Boichut, P.-C. Héam, 0. Kouchnarenko, Handling Algebraic Properties in Automatic Analysis of Security Protocols. INRIA Research Report, March 2006. download

  7. M. S. Bouassisa, N. Chridi, I. Chrisment, O. Festor, L. Vigneron, Automatic Verification of a Key Management Architecture for Hierarchical Group Protocols. Proceedings of SAR'06, 2006.

  8. C. Caleiro, L. Viganò, D. Basin, On the Semantics of Alice&Bob Specifications of Security Protocols, Theoretical Computer Science. To appear.

  9. Y. Chevalier, M. Rusinowitch, Hierarchical Combination of Intruder Theories. In F. Pfenning, editor, Proceedings of the 17th International Conference on Rewriting Techniques and Applications Seattle, August 12 - 14, 2006. download

  10. V. Cortier, M. Rusinowitch, E. Zalinescu, Relating two standard notions of secrecy Computer Science Logic 2006 25-29 September, 2006, Szeged, Hungary. download

  11. P. Degano, L. Viganò, editors, Special Issue of Theoretical Computer Science on Automated Reasoning for Security Protocol Analysis, Elsevier Science. To appear.

  12. D. von Oheimb and J. Cuellar, Designing and verifying core protocols for location privacy. Proceedings of ISC'06, 2006. download

  13. J. Santiago and L. Vigneron, Automatically Analysing Non-repudiation with Authentication, Proceedings of 3rd Taiwanese-French Conference on Information Technology (TFIT), 541--554, Nancy, France, 2006.

  14. L. Viganò, Automated Security Protocol Analysis with the AVISPA Tool. Proceedings of the XXI Mathematical Foundations of Programming Semantics (MFPS'05), ENTCS 155:61--86, Elsevier. download

    2005

  15. M. Abadi, V. Cortier, Deciding knowledge in security protocols under (many more) equational theories. In Proc. 18th IEEE Computer Security Foundations Workshop (CSFW'05), Aix-en-Provence, France, June 2005, pages 62-76. IEEE Comp. Soc. Press, 2005. download

  16. A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.C. Heám, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò, L. Vigneron, The Avispa Tool for the automated validation of internet security protocols and applications, in proceedings of CAV 2005, Computer Aided Verification, LNCS 3576, Springer Verlag. download

  17. A. Armando, L. Compagna, An Optimized Intruder Model for SAT-based Model-Checking of Security Protocols, in Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2004), ENTCS 125(1):91-108, 2005. download

  18. A. Armando, L. Viganò, editors, Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2004), ENTCS 125(1), 2005. download

  19. A. Armando, L. Viganò, Preface (editorial) in Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2004), ENTCS 125(1):1, 2005. download

  20. M. Backes, A. Datta, A. Derek, J.C. Mitchell, M. Turuani, Compositional Analysis of Contract Signing Protocols. CSFW-18. June 20--22 2005. 18th IEEE Computer Security Foundations Workshop, Aix-en-Provence, France. IEEE Computer Society. download

  21. D. Basin, S. Mödersheim, Luca Viganò, Algebraic Intruder Deductions. Proceedings of LPAR 2005, LNAI 3835, pp. 549--564, Springer Verlag, 2005. download

  22. D. Basin, S. Mödersheim, L. Viganò, OFMC: A symbolic model checker for security protocols, International Journal of Information Security 4(3):181--208, 2005. download

  23. Y. Boichut, P.-C. Héam, 0. Kouchnarenko, Automatic Verification of Security Protocols Using Approximations. INRIA Research Report, October 2005. download

  24. C. Caleiro, L. Viganò, D. Basin, Relating strand spaces and distributed temporal logic for security protocol analysis, Logic Journal of the IGPL, vol. 13, no. 6, pages 637-663, 2005. download

  25. C. Caleiro, L. Viganò, D. Basin, Deconstructing Alice and Bob, in Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2005), ENTCS 135(1):3-22, 2005. download

  26. C. Caleiro, L. Viganò, D. Basin, Metareasoning about security protocols using distributed temporal logic, in Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2004), ENTCS 125(1):67-89, 2005. download

  27. Y. Chevalier, R. Küsters, M. Rusinowitch, M. Turuani, An NP decision procedure for protocol insecurity with XOR. Theoretical Computer Science, 2005. Volume 338, Number 1-3, pages 247-274. download

  28. Y. Chevalier, R. Küsters, M. Rusinowitch, M. Turuani, Deciding the Security of Protocols with Commuting Public Key Encryption. In Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2004), Electronic Notes in Theoretical Computer Sciences, 2005. Volume 125, number 1, pages 55-66. download

  29. Y. Chevalier, M. Rusinowitch, Combining Intruder Theories, In the proceedings of International Colloquium on Automata, Languages and Programming (ICALP), LNCS 3580, pages 639--651, 2005. download. (Long version available as INRIA Research Report.)

  30. Y. Chevalier, M. Rusinowitch, Combining Intruder Theories. In L. Vigneron, editor, Proceedings of the 19th International Workshop on Unification, Nara, Japan, pages 63-76, April 2005. download

  31. N. Chridi, L. Vigneron, Modélisation des propriétés de sécurité de protocoles de groupe. In Actes du 1er Colloque sur les Risques et la Sécurité d'Internet et des Systèmes, CRiSIS, Bourges, France, pages 119-132, Oct 2005. Best paper award. download

  32. L. Compagna, SAT-based Model-Checking of Security Protocols. PhD Thesis, Università degli Studi di Genova and the University of Edinburgh, September 2005. download

  33. V. Cortier, M. Rusinowitch, E. Zalinescu, A resolution Strategy for Verifying Cryptographic Protocols with CBC Encryption and Blind Signatures PPDP'05. Lisboa, Portugal, July 2005. ACM press. download

  34. P. Degano, L. Viganò, editors, Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2005), ENTCS 135(1), 2005. download

  35. P. Degano, L. Viganò, Preface (editorial) in Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2005), ENTCS 135(1):1-2, 2005. download

  36. P. Hankes Drielsma, S. Mödersheim, The ASW Protocol Revisited: A Unified View in Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2004), ENTCS 125(1):141-156, 2005. download

  37. P. Hankes Drielsma, S. Mödersheim, L. Viganò, A formalization of off-line guessing for security protocol analysis, in Proceedings of LPAR'04, LNAI 3452, pages 363--379, copyright © Springer-Verlag, 2005. download

  38. D. von Oheimb, The High-Level Protocol Specification Language HLPSL developed in the EU project AVISPA, in Proceedings of APPSEM 2005 Workshop, September 13, 2005. download

  39. J. Santiago, L. Vigneron, Study for Automatically Analysing Non-repudiation. In Actes du 1er Colloque sur les Risques et la Sécurité d'Internet et des Systèmes, CRiSIS, Bourges, France, pages 157-171, Oct 2005. download

  40. Tomasz Truderung, Regular Protocols and Attacks with Regular Knowledge, to appear in the proceedings of the International Conference on Automated Deduction (CADE), 2005, LNCS, Springer-Verlag. download

  41. L. Viganò, Automated Security Protocol Analysis with the AVISPA Tool. In the Proceedings of the XXI Mathematical Foundations of Programming Semantics (MFPS'05). To appear on the ENTCS.

    2004

  42. M. Abadi, V. Cortier, Deciding knowledge in security protocols under equational theories Icalp'04. July 2004. Turku, Finland. Lecture Notes in Computer Science. download

  43. A. Armando, L. Compagna, Abstraction-driven SAT-based Analysis of Security Protocols, in LNCS 2919 - Theory and Applications of Satisfiability Testing, Selected Paper, 2004. Copyright © Springer-Verlag. Presented at SAT 2003, May 5-8 2003, S.Margherita Ligure, Italy. download

  44. A. Armando, L. Compagna, SATMC: a SAT-based Model Checker for Security Protocols, in Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA 2004), LNCS 3229, copyright © Springer-Verlag, 2004. download

  45. A. Armando, L. Compagna, Y. Lierler, Automatic Compilation of Protocol Insecurity Problems into Logic Programming, in Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA 2004), LNCS 3229, copyright © Springer-Verlag, 2004. download

  46. Y. Boichut, P.-C. Heam, O. Kouchnarenko, F. Oehl, Improvements on the Genet and Klay Technique to Automatically Verify Security Protocols, in Automated Verification of Infinite States Systems AVIS'04 (WS ETAPS'04), 2004. download

  47. C. Caleiro, L. Viganò, D. Basin, Towards a metalogic for security protocol analysis, in Proceedings of the Workshop on the Combination of Logics: Theory and Applications (Comblog'04), pages 187--196. Center for Logic and Computation, Departamento de Matemática, Instituto Superior Técnico, Lisbon, Portugal, 2004. download

  48. Y. Chevalier, A Simple Constraint Solving Procedure for Protocols with Exclusive Or, in Proceedings of the 18th Int. Workshop on Unification, Cork (Ireland), July 2004. download. (Long version available as Technical Report.)

  49. Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drieslma, J. Mantovani, S. Mödersheim and L. Vigneron, A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols, in Proceedings of Workshop on Specification and Automated Processing of Security Requirements (SAPS 2004), 2004. download

  50. Y. Chevalier, L. Vigneron, Strategy for Verifying Security Protocols with Unbounded Message Size, Journal of Automated Software Engineering, 11(2): 141-166, April 2004. Kluwer Academic Publishers. download

  51. Y. Chevalier and L. Vigneron, Rule-based Programs describing Internet Security Protocols, Proceedings of 5th Int. Workshop on Rule-Based Programming (RULE), Aachen (Germany), June 2004. RWTH Aachen Technical Report AIB-2004-04, pages 83-97. download

  52. G. Delzanno and P. Ganty Automatic Verification of Time-sensitive Cryptographic Protocols. To appear in the Proceedings of the Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), a member conference of the European Joint Conference on Theory and Practice of Software (ETAPS 2004), 2004. download

  53. M. Rusinowitch, A Decidable Analysis of Security Protocols. In the proceedings of the 18th IFIP World Computer Congress on Theoretical Computer Science - TCS'2004, 2004.

    2003

  54. P. Ammirati and G. Delzanno, Constraint-based Automatic Verification of Time Dependent Security Properties, In Proceedings of the Workshop on Security Protocols Verification (SPV 2003), co-located with the International Conference on Concurrency Theory (CONCUR 2003), 2003. download

  55. A. Armando, L. Compagna and P. Ganty, SAT-based Model-Checking of Security Protocols using Planning Graph Analysis, in Proceedings of the 12th International FME Symposium (FME 2003), LNCS 2805, copyright © Springer-Verlag, 2003. download

  56. D. Basin, S. Mödersheim, L. Viganò, An On-The-Fly Model-Checker for Security Protocol Analysis, in Proceedings of ESORICS'03, LNCS 2808, pp. 253-270, Springer-Verlag, 2003. download

  57. D. Basin, S. Mödersheim, L. Viganò, Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols (Extended Abstract), in Proceedings of SPV'03, 2003. download

  58. D. Basin, S. Mödersheim, L. Viganò, Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols, in Proceedings of CCS'03, pp. 335-344, ACM Press, 2003. download

  59. Y. Chevalier, Resolution de problemes d'accessibilite pour la compilation et la validation de protocoles cryptographiques. These de doctorat, Universite Henri Poincare, Nancy, Decembre 2003. download

  60. Y. Chevalier and R. Kuesters and M. Rusinowitch and M. Turuani, Deciding the Security of Protocols with Diffie-Hellman Exponentiation and Products in Exponents. FST-TCS 03. December 15--17, 2003. Indian Institute of Technology, Bombay. Mumbai, INDIA. Lecture Notes in Computer Science. download

  61. Y. Chevalier, R. Kusters, M. Rusinowitch and M. Turuani, An NP Decision Procedure for Protocol Insecurity with XOR, 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003. download

  62. Y. Chevalier, R. Kuesters, M. Rusinowitch, M. Turuani and L. Vigneron, Extending the Dolev-Yao Intruder for Analyzing an Unbounded Number of Sessions, Computer Science Logic (CSL 03) and 8th Kurt Goedel Colloquium (8th KCG), 2003. download

  63. G. Delzanno and P. Ganty, Symbolic Methods for Automatically Proving Secrecy and Authentication in Infinite-state Models of Cryptographic Protocols, Proceedings of WISP, Workshop on Issues in Security and Petri Nets, 2003. download

  64. F. Oehl, G. Cécé, O. Kouchnarenko, D.Sinclair, Automatic Approximation for the Verification of Cryptographic Protocols. Proc. Int. Conference on Formal Aspects of Security (FASec), London, UK. November, 2003. Lecture Notes in Computer Science 2629, pp. 33-48. download

  65. M. Rusinowitch, Automated Analysis of Security Protocols, in G. Vidal, editor, Proceedings of the 12th International Workshop on Functional and (Constraint) Logic Programming (WFLP'03). Electronic Notes in Theoretical Computer Science 86(3), 2003. download

  66. M. Rusinowitch and M. Turuani, Protocol Insecurity with Finite Number of Sessions and Composed Keys is NP-complete, Theoretical Computer Science, 2003, download

  67. M. Turuani, Securite des Protocoles Cryptographiques: Decidabilite et Complexite. These de doctorat, Universite Henri Poincare, Nancy, Decembre 2003. download