AVISPA Project

The goal of the European project AVISPA is to propose a tool for security protocols verification. This tool called avispa is composed of: a translator tool (HLPSL2IF) and four analyzers (CL-ATse, SATMC, OFMC and TA4SP). The HLPSL2IF tool translates an HLPSL (High Level Protocol Specification Language) specification of a protocol into a common language to all the tools: IF (Intermediate Format). Thus, the analyzers check various properties with their own approach. The heterogeneity of the approaches is an interesting point. Indeed, CL-ATse, SATMC and OFMC consider a bounded number of sessions making attacks research possible. The TA4SP tool proves secrecy properties on a protocol with an unbounded number of sessions.
The structure of the AVISPA tool is presented below.

Approach used by TA4SP

Thomas Genet (IRISA-Rennes, France) and Francis Klay (France-Telecom R&D) have adapted an approach based on rewriting on regular tree languages to the protocols verification.
From the language of an initial automaton A0 representing the initial configuration of the network (= the initial intruder knowledge because the intruder = network), a term rewriting R is applied until reaching a possible stabilization of the process (L(An)=L(An+1)). This term rewriting system represents, not only the intruder abilities to analyze or compose the messages, but also the protocol steps.
For example, a rule l → r, where l is the message received and r the message sent, represents a protocol step.
Thus, terms obtained by rewriting are added to the language of the current automaton. A new automaton is then obtained and so on.

The process, presented above, consists in searching a substitution μ which associates a variable a ground term such that:
is reduced to a state q of the current automaton and not.
Thus, the idea is to add the transitions needed to the reduction of into q.
For example, to add the term f(g(a),b) on the state q, the transitions below are added to the transitions set of the current automaton.
a → qnew1, g(qnew1) → qnew2, b → qnew3 and f(qnew2,qnew3) → q
Notice that the process concerns substitutions from variables to states. It is then possible to rewrite a set of terms into another set of terms.

However this process may goes on forever due to the new states introduced at each rewriting step. The use of approximations functions can make the process seen above to terminate. However, the counterpart of the approximation functions use is that the result obtained is an over-approximation of the intruder knowledge. Thus, if a secrecy property is safe on this over-approximation, then it is also true for the real intruder knowledge.

The figure below summarizes the main idea of this approach.

A tool named Timbuk and developed by Thomas Genet implements the approach seen previously. The Timbuk tool is available at the following address: http://www.irisa.fr/lande/genet/timbuk/.

Characteristics of TA4SP

From a theoretical point of view, the main difference remains in the fact that the states allotted by the approximation function are not fixed initially, contrary to some approximation functions previously used by Thomas Genet and Frederic Oehl (F. Oehl carried out a work on the automatic generation of approximation functions from an Isabelle specification). Unfortunately, for some industrial protocols, Oehl's improvement has not been sufficient to verify them. Our strategy is initially to check if we can use transitions of the current automaton. When it is not possible anymore, the approximations use default states (or new states). This approximation function contains symbolic transitions (where the right hand side or the left hand side of a transition may contain variables). It is then possible to compute under-approximations, over-approximations and to switch automatically from the first to the second during the process.

From a practical point of view, this tool is completely automatic and is composed of 2 tools:
  • A translator of the intermediate format to an input format (we have defined) supported by Timbuk and
  • an extension of Timbuk to make our approximation function supported by Timbuk.
The following picture summarizes the structure of the TA4SP tool.

Online Demonstration

You can try TA4SP either from the command line version of the AVISPA tool available at http://www.avispa-project.org or from the web interface freely reachable at http://www.avispa-project.org/web-interface/.

A new version is now available here! This version handles algebraic properties of operators like exponentiation or exclusive or. Download it here! Mac version and Unix version.

Some results

The table below is resulted from several experimentations of a previous version of the tool.
The answer OK means that the property is checked by using over-approximations whereas the answer NO means that the property is violated (by using under-approximations). The list below is not exhaustive.

Protocol SecrecyTime (s)
CHAPv2 OK10.59

Back to the Home Page