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 everincreasing 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

On the use of automatic tools for the formal analysis of IEEE 802.11 key-exchange protocols / Cheminod, Manuel; CIBRARIO BERTOLOTTI, Ivan; Durante, Luca; Sisto, Riccardo; Valenzano, Adriano. - STAMPA. - (2006), pp. 273-282. (Intervento presentato al convegno Factory Communication Systems, 2006 IEEE International Workshop on tenutosi a Torino nel 28-30 June, 2006) [10.1109/WFCS.2006.1704167].

On the use of automatic tools for the formal analysis of IEEE 802.11 key-exchange protocols

CHEMINOD, MANUEL;CIBRARIO BERTOLOTTI, IVAN;DURANTE, LUCA;SISTO, Riccardo;VALENZANO, ADRIANO
2006

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 everincreasing 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
2006
9781424403790
File in questo prodotto:
File Dimensione Formato  
On_the_use_of_automatic_tools_for_the_formal_analysis_of_IEEE_802.11_key-exchange_protocols.pdf

non disponibili

Tipologia: 2a Post-print versione editoriale / Version of Record
Licenza: Non Pubblico - Accesso privato/ristretto
Dimensione 399.87 kB
Formato Adobe PDF
399.87 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/1659173