Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols

Abstract : We present the first formal analysis of two avionic protocols that aim to secure air-ground communications, the ARINC823 public-key and shared-key protocols. We verify these protocols both in the symbolic model of cryptography, using ProVerif, and in the computational model, using CryptoVerif. While we confirm many security properties of these protocols, we also find several weaknesses, attacks, and imprecisions in the standard. We propose fixes for these problems. This case study required the specification of new cryptographic primitives in CryptoVerif. It also illustrates the complementarity between symbolic and computational verification.
Type de document :
Communication dans un congrès
30th IEEE Computer Security Foundations Symposium, Aug 2017, Santa Barbara, United States. pp.68-82, 2017, 〈10.1109/CSF.2017.7〉
Liste complète des métadonnées

Littérature citée [35 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01575861
Contributeur : Bruno Blanchet <>
Soumis le : lundi 21 août 2017 - 18:47:35
Dernière modification le : jeudi 26 avril 2018 - 10:28:18

Fichier

BlanchetCSF17.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Relations

  • est une partie de hal-01527671 - Companion technical report

Citation

Bruno Blanchet. Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols. 30th IEEE Computer Security Foundations Symposium, Aug 2017, Santa Barbara, United States. pp.68-82, 2017, 〈10.1109/CSF.2017.7〉. 〈hal-01575861〉

Partager

Métriques

Consultations de la notice

82

Téléchargements de fichiers

36