Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols

Résumé : Nous présentons la première analyse formelle de deux protocoles avioniques qui visent à sécuriser les communications air-sol, les protocoles ARINC823 à clé publique et à clé partagée. Nous vérifions ces protocoles, à la fois dans le modèle symbolique de la cryptographie, en utilisant ProVerif, et dans le modèle calculatoire, en utilisant CryptoVerif. Si nous confirmons beaucoup de propriétés de sécurité de ces protocoles, nous trouvons aussi plusieurs faiblesses, attaques, et imprécisions dans le standard. Nous proposons des corrections pour ces problèmes. Cette étude de cas a nécessité la spécification de nouvelles primitives cryptographiques dans CryptoVerif. Elle illustre aussi la complémentarité entre la vérification symbolique et la vérification calculatoire.
Type de document :
Rapport
[Research Report] RR-9072, Inria Paris. 2017, pp.40
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01527671
Contributeur : <>
Soumis le : mercredi 24 mai 2017 - 18:38:55
Dernière modification le : jeudi 15 juin 2017 - 09:09:32
Document(s) archivé(s) le : lundi 28 août 2017 - 16:19:06

Fichier

RR-9072.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01527671, version 1
  • Mot de passe : x#khj#

Collections

Relations

Citation

Bruno Blanchet. Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols. [Research Report] RR-9072, Inria Paris. 2017, pp.40. 〈hal-01527671〉

Partager

Métriques

Consultations de la notice

286

Téléchargements de fichiers

96