About V@PSI

VA@PSI is a three-years project funded by the Italian Ministry of Education, University and Research (MIUR) under the FIRB (Fondo per gli Investimenti della Ricerca di Base) Programme, as RBAU01P5SS.

Principal Investigator: Alessandro Armando, University of Genova
Managing Organization: DIST, University of Genova
Duration: 36 months (from January 2004)
Overall budget: 300.000 Euro

Research Groups
University of Genova (Alessandro Armando)
University of Trento (Fabio Massacci)
University of Napoli (Massimo Benerecetti)

Our economic, political, and social life today depends vitally on communication and IT infrastructures, in particular the Internet. The acceptance and continued expansion of these infrastructures depends on trust: all participants must have confidence in their security, which is integrated into the infrastructure either by means of specific security protocols or protocol families (cf. protocols like IPSec, IKE, TLS, and SSH). In open networks protocols should work even under worstcase assumptions, e.g. messages may be eavesdropped or tampered with by an "intruder" or careless principals. Severe attacks can be conducted even without breaking cryptography, but by exploiting weaknesses in the protocols themselves. These attacks oftem stems from subtle misconceptions in the design of the protocols which are very difficult for humans to determine, due to the complex ways different protocol sessions could be interleaved, and the possible interferences of malicious intruders.

V@PSI aims to develop a platform based on a variety of techniques that will allow industry and standardization experts to automatically validate or detect errors on a large collection of practically relevant, Internet protocols.

The overall goals of the project are:

  1. to develop a rich specification language for formalizing protocols, security goals, and threat models for protocols of industrial complexity, building upon existing standards for protocol specification (e.g. SDL, ASN.1, UML-CD, etc.),
  2. to advance the state-of-the-art model-checking techniques to scale up to this complexity,
  3. to build a platform based on these techniques that will allow industry and standardization experts to automatically validate or detect errors, and
  4. to tune the tool composing this platform and demonstrate proof-of-concept on a large collection of practically relevant, Internet protocols.
The partners have previously carried out extensive work that lays the foundations of the proposed technology. They have developed independently a number of different verification and validation techniques based on
  1. finite-state analysis by reduction to propositional satisfiability checking,
  2. infinite-state verification based on interactive theorem-proving,
  3. model checking interactive distributed systems based on process algebras, and
  4. model-checking of multi-agent finite state machines.
The techniques developed by the partners exhibit a strong form of complementarity. On the one hand, (i) and (iv) cope with the infinity of the search space by building and analyzing approximations of the problem which are then iteratively improved. These techniques are thus most suited for error detection: while (i) has proved very effective in finding attacks carried out by an active intruder, (iv) can identify flaws by showing that protocols do not ensure the expected security goals. On the other hand, (iii) aims at establishing the equivalence between a model known to enjoy the desired security property and the actual model and therefore, together with (ii), is suited for verification.

The effectiveness of the approaches on small and medium size protocols has been demonstrated in previous work. However, whether the approaches scale up to the new generation of largescale, security protocols remains a challenge. This will leads us to
This will be done by developing an integrated verification platform based on them, by selecting a set of security sensitive Internet protocols, and by using the tools to automatically analyze the selected protocols.