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.
The structure of the AVISPA tool is presented below.
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.
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:
lμ is reduced to
a state q of the current automaton and
rμ not.
Thus, the idea is to add the transitions needed to the
reduction of rμ 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.
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.
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/.
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.
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.
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.
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.
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 | Secrecy | Time (s) |
| CHAPv2 | OK | 10.59 |
| SHARE | OK | 48.97 |
| NSPK-LOWE | OK | 15.02 |
| NSPK | NO | 7.56 |
Back to the Home Page