On the Use of Automatic Tools for the Formal Analysis of the IEEE 802.11 Key-Exchange Protocols

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.