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


https://hal.inria.fr/hal-01527671
Contributeur : Bruno Blanchet <>
Soumis le : mercredi 24 mai 2017 - 18:38:55
Dernière modification le : jeudi 15 juin 2017 - 09:09:32

Fichier

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

Identifiants

  • HAL Id : hal-01527671, version 1

Collections

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

207

Téléchargements du document

59