@inproceedings{110cae5319a7459cbe9bf8f682dd0c6a,
title = "A machine-checked proof of security for AWS key management service",
abstract = "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.",
keywords = "Key Management, Machine-Checked Proof, Provable-Security",
author = "Almeida, \{Jos{\'e} Bacelar\} and Matthew Campagna and Vitor Pereira and Manuel Barbosa and Ernie Cohen and Bernardo Portela and Serdar Tasiran and Gilles Barthe and Benjamin Gregoire and Strub, \{Pierre Yves\}",
note = "Publisher Copyright: {\textcopyright} 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.; 26th ACM SIGSAC Conference on Computer and Communications Security, CCS 2019 ; Conference date: 11-11-2019 Through 15-11-2019",
year = "2019",
month = nov,
day = "6",
doi = "10.1145/3319535.3354228",
language = "English",
series = "Proceedings of the ACM Conference on Computer and Communications Security",
publisher = "Association for Computing Machinery",
pages = "63--78",
booktitle = "CCS 2019 - Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security",
}