Paper 2019/1042

A Machine-Checked Proof of Security for AWS Key Management Service

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Gregoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, and Serdar Tasiran

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.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. MINOR revision.ACM CCS 2019
Keywords
Provable-SecurityMachine-Checked ProofKey Management
Contact author(s)
mbb @ fc up pt
History
2019-09-18: received
Short URL
https://ia.cr/2019/1042
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2019/1042,
      author = {José Bacelar Almeida and Manuel Barbosa and Gilles Barthe and Matthew Campagna and Ernie Cohen and Benjamin Gregoire and Vitor Pereira and Bernardo Portela and Pierre-Yves Strub and Serdar Tasiran},
      title = {A Machine-Checked Proof of Security for AWS Key Management Service},
      howpublished = {Cryptology ePrint Archive, Paper 2019/1042},
      year = {2019},
      note = {\url{https://eprint.iacr.org/2019/1042}},
      url = {https://eprint.iacr.org/2019/1042}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.