Skip to Main content Skip to Navigation
Reports

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.
Complete list of metadatas

Cited literature [44 references]  Display  Hide  Download

https://hal.inria.fr/hal-01527671
Contributor : Bruno Blanchet <>
Submitted on : Wednesday, May 24, 2017 - 6:38:55 PM
Last modification on : Thursday, April 26, 2018 - 10:27:48 AM
Document(s) archivé(s) le : Monday, August 28, 2017 - 4:19:06 PM

File

RR-9072.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01527671, version 1

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⟩

Share

Metrics

Record views

755

Files downloads

518