Cybersecurity is incomplete without innovation. Security researchers work on different research projects to introduce new applications and security tools. The testing of new protocols and applications in Cybersecurity domain is similar to Systems Development Life Cycle (SDLC) used in software development industry. The SDLC helps to design, develop, and test the software performance. Similarly, the security protocols introduced by Security researchers are tested through multiple techniques before embraced by the community. The Automated Validation of Internet Security Protocols and Applications (AVISPA) is one such tool that is used to analyze the internet security parameters of security-sensitive protocols and applications that are yet to be adopted by Cybersecurity world. In this tutorial, we will cover the basic working principles of AVISPA tool and its installation procedure.
What is AVISPA?
AVISPA is the short form of Automated Validation of Internet Security Protocols and Applications tool. The tool provides a suite of applications to build and analyze the formal models of security-sensitive protocols and applications. The AVISPA is recommended to analyze the security of protocols that involve messages exchange between different nodes (entities) that are part of the protocol or security scheme. Many security schemes related to privacy and authentication are tested in AVISPA. Each line of code in the schemes is interpreted individually to find the potential security flaws. The following figure presents the basic architecture of AVISPA tool.
The architecture can be classified into three layers. The top layer is the input layer marked with High Level Protocol Specification Language (HLPSL). The security protocols (codes) to be tested in AVISPA are written in HLPSL format. The middle layer in AVISPA tool is the converter section that translates the HLPSL into an Intermediate Format (IF) code with the help of an inbuilt translator. The IF code is then analyzed with the help of backend analyzers (the bottom layer). The AVISPA currently supports the following four backend analyzers (models).
- On the Fly Model Checker (OFMC)
- CL-Based Attack Searcher (CL-AtSe)
- SAT-based Model Checker (SATMC)
- Tree Automata-based Protocol Analyzer (TA4SP)
Since most of the communication in Cyberspace is carried out through open (unsecure) channels, the AVISPA provides a similar setup called Dolev-Yao (DY) model to test the protocols in an environment as if they are tested in a real world. The DY model simulates and adversarial model to find the security flaws (if any) in the protocols during the simulation process. The model enables the adversaries to intercept and modify the messages that are exchanged between the entities of the specified protocol. If an adversary manages to break the proposed security, the protocol is declared as “Unsafe” by the AVISPA tool. On the other hand, if the underlying protocol runs without any security breach, the protocol is marked as safe for the defined security goals.
High Level Protocol Specification Language (HLPSL)
The HLPSL is the crux of AVISPA tool. Any protocol or scheme to be tested by AVISPA is converted into HLPSL. It explains the working of security protocols based on the security parameters to be tested. The HLPSL transforms the under-trial protocols into roles. There are two main roles specified by the HLPSL. These are basic roles and composed roles. The basic roles describe the action of the entities (agents) that are part of the protocol. The composed roles instantiate the basic roles that design the entire scheme (protocol) run.
Constants and Variables in HLPSL: The HLPSL models the given protocols by defining the systems state. After defining the initial state, we specify the ways in which the state may change (depending on the function of each entity). State variables and constants are used for this purpose. In HLPSL, the variables start with a capital letter while constants are written in small letters for easy identification. Each variable and constant belong to a unique type. The state variables are defined in the basic roles. The state variable indicates the current value of the variables used in the scheme. The future variables (also called prime variables) are not included in the basic role definition as they are generated later in the given scheme or protocol.
HLPSL Data Types: The HLPSL is a typed programming language. Each variable and constant in HLPSL belongs to a specific type. Some of these are explained below.
- agent: The agent represents the principal names used in the test protocol or scheme. Although the intruder is also an agent, it is represented by the letter (i).
- symmetric_keys: These variable types represent the symmetric keys for encryption processes.
- asymmetric_keys: The asymmetric key variables are used for asymmetric encryption/decryption process. For instance, for any public key (pk), the decryption key shall be inv(pk).
- text: The text variable shows the nonces used in the protocol. The (fresh) attribute is added to the text variable to demonstrate the freshness of the nonces.
- nat: The nat type represents the natural numbers. The nat is useful in non-message contexts. The examples include the test of number inequality (g: A < B) and modeling of countably infinite sets.
- function: The function type represents different types of functions that are present in the protocol scheme and supported by the AVISPA tool. There are two types of functions in HLPSL. The functions that don’t change values throughout the protocol are called rigid functions. The other functions that change values (through mapping) are known as flexible functions.
AVISPA Software Installation
The AVISPA tool can be downloaded from the following official website.
There are different download options available on the home page of the website. The ideal approach is to download the AVISPA tool along with its Security Protocol Animator (SPAN) from the following link.
The download files are available in Open Virtual Appliance (OVA) format to run the tool in a virtual environment without OS installation. After downloading the OVA file, go to the Virtual Box software and click on the Import Alliance option as shown in the following screenshot.
Locate the AVISPA OVA to load in the virtual box.
After AVISPA’s OVA file uploading, a configuration screen appears to make any desired changes to the resources available to run the AVISPA image file.
After making the desired changes, click on the import option to complete the AVISPA loading process.
Now, we can run the AVISPA tool by navigating to the Start menu of the VirtualBox.
When the AVISPA program loads successfully, we see the following UBUNTU screen with SPAN application and multiple preloaded test protocols to practice the tool.
By clicking on the SPAN icon, we see the following AVISPA GUI.
Click on the file tab to see the HLPSL file load option.
Let’s upload a test HLPSL code from the available list of files to see the working of the AVISPA tool.
When the HLPSL code is loaded in the tool, we can select the desired backend model to test the protocol security. In this demonstration, we have selected the OFMC model.
If there are no attacks found in the protocol, the tool declares it Safe as shown in the following screenshot.
Apart from security analysis, the AVISPA tool also offers the protocol and intruder simulation to visualize the working or attack scenarios in the test protocols. For instance, if we click on the protocol simulation option, we can visualize the messages exchange procedure between the different entities that are part of the protocol or test scheme.
AVISPA is a reliable opensource tool to test security of different protocols and schemes that involve messages exchange between two or more entities. The simulation process makes it easier for the researchers to identify the working and intrusion points in their schemes.