[Resource Topic] 2019/1042: A Machine-Checked Proof of Security for AWS Key Management Service

Welcome to the resource topic for 2019/1042

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

Authors: José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Gregoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, 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.

ePrint: https://eprint.iacr.org/2019/1042

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .