Analysis of the ARINC823 protocols

This page presents the models used to verify the ARINC823 protocols in ProVerif and CryptoVerif. These models are supplemental material for the following paper:

Bruno Blanchet. Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols. In 30th IEEE Computer Security Foundations Symposium (CSF'17), Santa Barbara, CA, USA, August 2017. IEEE. To appear. Long version available at https://hal.inria.fr/hal-01527671.

The following files correspond to older versions of ProVerif and CryptoVerif; up-to-date files are included in the distributions of these tools, in directory examples/pitype/arinc823 of the ProVerif distribution and in directory examples/arinc823 of the CryptoVerif distribution.

The whole archive

1. The shared-key protocol

1.1. The ProVerif models (subdirectory sharedkey/symbolic)

arinc823-secret-key.m4.pv is the master file from which all models are generated using the m4 preprocessor. The generated files are arinc823-secret-key.$p.$e.$s.pv where

1.2 The CryptoVerif models (subdirectory sharedkey/computational)

2. The public-key protocol

2.1. The ProVerif models (subdirectory publickey/symbolic)

arinc823-public-key.m4.pv is the master file from which all models are generated using the m4 preprocessor. The generated files are arinc823-public-key.$p.$c.$e.$s.pv where

2.2. The CryptoVerif models (subdirectory publickey/computational)


Bruno Blanchet