Copyright Notice:
The publication copies distributed in this site are
provided to ensure timely dissemination of scholarly and technical
work. Copyright and all rights therein are retained by authors or by
other copyright holders (as explicitly indicated). All persons copying
this information are expected to adhere
to the terms and constraints invoked by each copyright. In
most cases, these works may not be reposted without the explicit
permission of the copyright holder
Manuel Cheminod, Ivan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano,
On the use of automatic tools for the formal analysis of IEEE 802.11 key-exchange protocols,
in WFCS 2006 - 6th IEEE Int. Workshop on Factory Communication Systems, Turin, Italy, June 2006, IEEE, pp. 273-282.
©2006 IEEE
PDF
Abstract
It is well known that the design and development of complex distributed systems, such as those used in modern factory automation
and process control environments, can obtain significant benefits from the adoption of formal methods during the specification
and verification phases. The importance of using formal techniques for verifying the design correctness is even more evident
when aspects such as security and safety are considered and a class of protocols, known as cryptographic protocols, is taken
into account. Cryptographic protocols, in fact, are becoming more and more used in industrial networks to support security-related
services such as cryptographic keys exchange/distribution and authentication, due to the ever increasing use of internet/intranet-based
connections and the introduction of wireless communications. This paper reports on some experimental investigations on the
formal verification of two cryptographic protocols, that are commonly used in industrial wireless 802.11 networks. Investigations
are carried out by means of fully automatic and publicly available tools that are based on state-exploration techniques. The
aim of our work is twofold: first we intend to offer a contribution in understanding whether or not the current prototype
tools can be considered mature enough for helping the designer with the analysis of real protocols, and second we wish to
develop some (preliminary) considerations on their characteristics and performance
Back to Riccardo Sisto's publications