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.
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
Long-term archiving on : 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

661

Files downloads

397