4. Protocol verification: the AVISPA platform

In practice, Internet protocols can run in parallel (known as protocol sessions). They are therefore highly susceptible to man-in-the-middle attacks. The question then arises, when a protocol is developed, as to whether it is secure against these vulnerabilities.

The general technique is as follows:

• we model the system in a mathematical language;

• the properties to be verified by the system are modeled in a compatible language;

• we compare the two models to determine whether the system is correct in terms of its properties.

When it comes to the computerized verification of systems (the term system is used here in a generic sense, to designate a program as well as a protocol or cruise control), the general approach...