The AVISPA Tool provides a suite of applications for building and analyzing formal models of
security protocols. Protocol models are written in the High Level Protocol Specification Language,
or HLPSL. It aims at developing a push-button, industrial-strength technology for the analysis of large-scale Internet security-sensitive protocols and applications. Also 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. Experimental results, carried out on a large library of Internet security protocols, indicate that the AVISPA tool is the state of the art for automatic security protocols. No other tool combines the same scope and robustness with such performance and scalability.
With the spread of the Internet and network-based services and the development of new technological possibilities, the number and scale of new security protocols under development is outpacing the human ability to rigorously analyse and validate them. This is an increasingly serious problem for standardization organizations like the Internet Engineering Task Force (IETF), the International Telecommunication Union (ITU) and the World Wide Web Consortium (W3C). It also affects companies whose products and services depend on the rapid standardization and correct functioning of these protocols, and users whose rights and freedoms (eg the right to privacy of personal data) depend on a secure infrastructure.
Designing secure protocols is a hard problem. In open networks such as the Internet, protocols should work even under worst-case assumptions, eg that messages may be seen or tampered with by an intruder (also called the attacker or spy). Severe attacks can be conducted without breaking cryptography, by exploiting weaknesses in the protocols themselves. Examples of this are 'masquerading attacks', in which an attacker impersonates an honest agent, or 'replay attacks', in which messages from one protocol session (ie execution of the protocol) are used in another session. The possibility of these attacks sometimes stems from subtle mistakes in protocol design. Typically these attacks go unnoticed, as it is difficult for humans, despite careful protocol inspection, to determine all the complex ways in which protocol sessions can be interleaved, with the possible interference of a malicious intruder.
Tools that support a rigorous analysis of security protocols are thus of great importance in accelerating and improving the development of the next generation of security protocols. Ideally, these tools should be completely automated, robust, expressive and easily usable, so that they can be integrated into protocol development and standardization processes.
Although in the last decade many new techniques that can automatically analyse small and medium-scale protocols have been developed, moving up to large-scale Internet security protocols remains a challenge. The AVISPA tool is a push-button tool for the Automated Validation of Internet Security-sensitive Protocols and Applications, which rises to this challenge in a systematic way. First, it provides a modular and expressive formal language for specifying security protocols and properties. Second, it integrates different back-ends that implement a variety of automatic analysis techniques ranging from protocol falsification (by finding an attack on the input protocol) to abstraction-based verification methods for both finite and infinite numbers of sessions. To the best of our knowledge, no other tool exhibits the same scope and robustness while enjoying the same performance and scalability.
AVISPA Web-based graphical user interface.
As shown in the figure, AVISPA is equipped with a Web-based graphical user interface that supports the editing of protocol specifications and allows the user to select and configure the back-ends integrated into the tool. If an attack on a protocol is found, the tool displays it as a message-sequence chart. The interface features specialized menus for both novice and expert users. A protocol designer interacts with the tool by specifying a security problem (ie a protocol paired with a security property that the protocol is expected to achieve) in the High-Level Protocol Specification Language (HLPSL). The HLPSL is an expressive, modular, role-based, formal language that is used to specify control-flow patterns, data-structures, alternative intruder models and complex security properties, as well as different cryptographic primitives and their algebraic properties. These features make HLPSL well suited for specifying modern, industrial-scale protocols.
In order to demonstrate the effectiveness of AVISPA, we selected a substantial set of security problems associated with protocols that have recently been, or are currently being standardized by organizations like the Internet Engineering Task Force IETF. We then formalized a large subset of these protocols in HLPSL. The result of this specification effort is the AVISPA Library (publicly available on the AVISPA Web site), which at present comprises 215 security problems derived from 48 protocols. Most of the problems in the library can be solved by the AVISPA tool in a few seconds. Moreover, AVISPA detected a number of previously unknown attacks on some of the protocols analysed, eg on some protocols of the ISO-PK family, on the IKEv2-DS protocol, and on the H.530 protocol.
The AVISPA tool can be freely accessed either through its Web-based interface or by downloading and installing the software distribution. For more details, please refer to the AVISPA Web site.
AVISPA has been developed in the context of the FET Open Project IST-2001-39252 'AVISPA: Automated Validation of Internet Security Protocols and Applications', in collaboration with the University of Genova, INRIA Lorraine, ETH Zurich and Siemens Munich.
