Vérification mécanisée, symbolique et calculatoire, des protocoles avioniques ARINC823
| Autor: | Bruno Blanchet |
|---|---|
| Přispěvatelé: | Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), ANR-14-CE28-0014,AnaStaSec,Analyse Statique pour la Sécurité(2014), Inria Paris, Programming securely with cryptography (PROSECCO ) |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
security protocols
Theoretical computer science Computer science modèle symbolique 0211 other engineering and technologies Cryptography 0102 computer and information sciences 02 engineering and technology Encryption Computer security computer.software_genre 01 natural sciences Public-key cryptography [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] protocoles cryptographiques [INFO]Computer Science [cs] 021110 strategic defence & security studies Cryptographic primitive business.industry Cryptographic protocol Avionics vérification computational model 010201 computation theory & mathematics Complementarity (molecular biology) The Symbolic modèle calculatoire business computer symbolic model |
| Zdroj: | 30th IEEE Computer Security Foundations Symposium 30th IEEE Computer Security Foundations Symposium, Aug 2017, Santa Barbara, United States. pp.68-82, ⟨10.1109/CSF.2017.7⟩ CSF [Research Report] RR-9072, Inria Paris. 2017, pp.40 |
| Popis: | 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.; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|