A machine-checked proof of security for AWS key management service
| Autor: | Vitor Pereira, José B. Almeida, Benjamin Grégoire, Pierre-Yves Strub, Serdar Tasiran, Ernie Cohen, Manuel Barbosa, Gilles Barthe, Bernardo Portela, Matthew J. Campagna |
|---|---|
| Přispěvatelé: | Universidade do Minho, Universidade do Porto, Institute IMDEA Software [Madrid], Amazon Web Services [Seattle] (AWS), Mathematical, Reasoning and Software (MARELLE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP), Département d'informatique de l'École polytechnique (X-DEP-INFO), École polytechnique (X), Universidade do Porto = University of Porto |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Provable security
050101 languages & linguistics Computer science Provable-Security Cryptography 02 engineering and technology Machine-Checked Proof Encryption Computer security computer.software_genre [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] 0202 electrical engineering electronic engineering information engineering 0501 psychology and cognitive sciences Key management Protocol (object-oriented programming) Service (business) Science & Technology business.industry 05 social sciences Proof assistant Security service 020201 artificial intelligence & image processing business computer Key Management Engenharia e Tecnologia::Engenharia Eletrotécnica Eletrónica e Informática |
| Zdroj: | CCS ACM CCS 2019-26th ACM Conference on Computer and Communications Security ACM CCS 2019-26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom. pp.63-78, ⟨10.1145/3319535.3354228⟩ |
| Popis: | We present a machine-checked proof of security for the domain management protocol of Amazon Web Services' KMS (Key Management Service) a critical security service used throughout AWS and by AWS customers. Domain management is at the core of AWS KMS; it governs the top-level keys that anchor the security of encryption services at AWS. We show that the protocol securely implements an ideal distributed encryption mechanism under standard cryptographic assumptions. The proof is machine-checked in the EasyCrypt proof assistant and is the largest EasyCrypt development to date. Manuel Barbosa was supported by grant SFRH/BSAB/143018/2018 awarded by the Portuguese Foundation for Science and Technology (FCT). Vitor Pereira was supported by grant FCT-PD/BD/113967/201 awarded by FCT. This work was partially funded by national funds via FCT in the context of project PTDC/CCI-INF/31698/2017. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|