Consiglio Nazionale delle Ricerche

Tipo di prodottoContributo in atti di convegno
TitoloOn the Use of Automatic Tools for the Formal Analysis of the IEEE 802.11 Key-Exchange Protocols
Anno di pubblicazione2006
Formato
  • Elettronico
  • Cartaceo
Autore/iM. Cheminod; I. Cibrario Bertolotti; L. Durante; R. Sisto; A. Valenzano
Affiliazioni autoriM. Cheminod; I. Cibrario Bertolotti; L. Durante; A. Valenzano: CNR-IEIIT, Istituto di Elettronica e di Ingegneria dell'Informazione e delle Telecomunicazioni, Torino, Italy R. Sisto: CNR-IEIIT e Dipartimento di Automatica e Informatica, Politecnico di Torino, Torino, Italy
Autori CNR e affiliazioni
  • RICCARDO SISTO
  • MANUEL CHEMINOD
  • LUCA DURANTE
  • ADRIANO VALENZANO
  • IVAN CIBRARIO BERTOLOTTI
Lingua/e
  • inglese
AbstractIt 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.
Lingua abstractinglese
Altro abstract-
Lingua altro abstract-
Pagine da273
Pagine a282
Pagine totali10
Rivista-
Numero volume della rivista-
Serie/Collana-
Titolo del volume-
Numero volume della serie/collana-
Curatore/i del volume-
ISBN1-4244-0379-0
DOI10.1109/WFCS.2006.1704167
Editore
  • IEEE-Institute Of Electrical And Electronics Engineers Inc., Piscataway (Stati Uniti d'America)
Verificato da refereeSì: Internazionale
Stato della pubblicazione-
Indicizzazione (in banche dati controllate)
  • Scopus (Codice:2-s2.0-41549138892)
  • IEEE Xplore digital library (Codice:1704167)
Parole chiaveautomatic analysis, state space exploration, IEEE 802.11, cryptographic protocols
Link (URL, URI)http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1704167
Titolo convegno/congresso6th IEEE International Workshop on Factory Communication Systems (WFCS 2006)
Luogo convegno/congressoTorino
Data/e convegno/congresso28-30 Giugno 2006
RilevanzaInternazionale
RelazioneContributo
Titolo parallelo-
Note/Altre informazioni-
Strutture CNR
  • IEIIT — Istituto di elettronica e di ingegneria dell'informazione e delle telecomunicazioni
Moduli CNR
    Progetti Europei-
    Allegati
    • On the Use of Automatic Tools for the Formal Analysis of the IEEE 802.11 Key-Exchange Protocols

    Dati storici
    I dati storici non sono modificabili, sono stati ereditati da altri sistemi (es. Gestione Istituti, PUMA, ...) e hanno solo valore storico.
    NoteIEEE Press, June 2006, pp. 273-282