Cryptology ePrint Archive: Report 2019/1042

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

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

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.

Category / Keywords: cryptographic protocols / Provable-Security; Machine-Checked Proof; Key Management

Original Publication (with minor differences): ACM CCS 2019

Date: received 13 Sep 2019

Contact author: mbb at fc up pt

Available format(s): PDF | BibTeX Citation

Version: 20190918:123121 (All versions of this report)

Short URL: ia.cr/2019/1042


[ Cryptology ePrint archive ]