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
- arinc823prim.cvl contains the declarations of primitives used by CryptoVerif, in addition to its standard library of primitives.
- gen is a script that analyzes all files.
- results is a summary of the results provided by this analysis.
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
- $p is the property
- AUTHENTICATION for authentication properties
- KEY_SECRECY for secrecy of keys
- SECRECY for secrecy of messages
- UKS for no unknown key share attacks
- $e is
- ENC_SUPPORTED when the aircraft supports encryption
- ENC_NOTSUPPORTED when it does not
- $s is
- FAST when the equations encode(encode_OFF,x) = x
and compress(comp_OFF,x) = x are omitted.
- SLOW when they are included. (These scripts are so slow
that not all of them terminated within a reasonable amount of time.)
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
- $p is the property
- AUTHENTICATION for authentication properties (including
no unknown key share attacks)
- KEY_SECRECY for secrecy of keys
- SECRECY for secrecy of messages
- $c determines the compromise scenario
- PFS for forward secrecy (all long-term keys compromised after
the end of the protocol)
- COMPROMISE_U for key compromise impersonation in which U is
compromised.
- COMPROMISE_V for key compromise impersonation in which V is
compromised.
- $e is
- ENC_SUPPORTED when the aircraft supports encryption
- ENC_NOTSUPPORTED when it does not
- $s is
- FAST when the equations encode(encode_OFF,x) = x
and compress(comp_OFF,x) = x are omitted.
- SLOW when they are included. (These scripts are so slow
that not all of them terminated within a reasonable amount of time.)
2.2. The CryptoVerif models (subdirectory publickey/computational)
- lemmaEnc.ocv: file for the proof of Appendix C
- arinc823-public-key.$p.m4.cv are the master files from which all other
models of the original protocol are generated using the m4 preprocessor,
where $p is the property:
The generated files are arinc823-public-key.$p.$r.cv where
$r determines the considered replay protection
- NOREPLAY_PROT: no replay protection, original protocol
- REPLAY_PROT: Our full replay protection
-
arinc823-public-key.fixed.$p.m4.cv
are the master files from which all models of our strengthened
protocol are generated using the m4 preprocessor,
where $p is the property:
The generated files are
- arinc823-public-key.fixed.AUTHENTICATION.REPLAY_PROT.$c.cv
for authentication, where $c determines the compromise scenario
- NO_COMPROMISE: no compromise
- COMPROMISE_U for key compromise impersonation in which U is
compromised.
- COMPROMISE_V for key compromise impersonation in which V is
compromised.
- arinc823-public-key.KEY_SECRECY.REPLAY_PROT.cv
for key secrecy
- arinc823-public-key.SECRECY.REPLAY_PROT.cv
for forward secrecy of messages
Bruno Blanchet