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
  15. 2005

  16. 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
  17. 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
  18. 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
  19. A. Armando, L. Viganò, editors, Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2004), ENTCS 125(1), 2005. download
  20. 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
  21. 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
  22. D. Basin, S. Mödersheim, Luca Viganò, Algebraic Intruder Deductions. Proceedings of LPAR 2005, LNAI 3835, pp. 549--564, Springer Verlag, 2005. download
  23. 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
  24. Y. Boichut, P.-C. Héam, 0. Kouchnarenko, Automatic Verification of Security Protocols Using Approximations. INRIA Research Report, October 2005. download
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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.)
  31. 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
  32. 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
  33. L. Compagna, SAT-based Model-Checking of Security Protocols. PhD Thesis, Università degli Studi di Genova and the University of Edinburgh, September 2005. download
  34. 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
  35. P. Degano, L. Viganò, editors, Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis (ARSPA 2005), ENTCS 135(1), 2005. download
  36. 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
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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.
  43. 2004

  44. M. Abadi, V. Cortier, Deciding knowledge in security protocols under equational theories Icalp'04. July 2004. Turku, Finland. Lecture Notes in Computer Science. download
  45. 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
  46. 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
  47. 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
  48. 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
  49. 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
  50. 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.)
  51. 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
  52. 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
  53. 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
  54. 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
  55. 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

  56. 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
  57. 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
  58. 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
  59. 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
  60. 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
  61. 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
  62. 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
  63. 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
  64. 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
  65. 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
  66. 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
  67. 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
  68. M. Rusinowitch and M. Turuani, Protocol Insecurity with Finite Number of Sessions and Composed Keys is NP-complete, Theoretical Computer Science, 2003, download
  69. M. Turuani, Securite des Protocoles Cryptographiques: Decidabilite et Complexite. These de doctorat, Universite Henri Poincare, Nancy, Decembre 2003. download