Please use this identifier to cite or link to this item: http://hdl.handle.net/1822/66487

TitleA machine-checked proof of security for AWS key management service
Author(s)Almeida, José Bacelar
Barbosa, Manuel
Barthe, Gilles
Campagna, Matthew
Cohen, Ernie
Gregoire, Benjamin
Pereira, Vitor
Portela, Bernardo
Strub, Pierre-Yves
Tasiran, Serdar
KeywordsProvable-Security
Machine-Checked Proof
Key Management
Issue date2019
PublisherAssociation for Computing Machinery
JournalProceedings of the ACM Conference on Computer and Communications Security
CitationJosé Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna,Ernie Cohen, Benjamin Gregoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, and Serdar Tasiran. 2019. A Machine-Checked Proof of Securityfor AWS Key Management Service. In2019 ACM SIGSAC Conference onComputer & Communications Security (CCS ’19), November 11–15, 2019,London, United Kingdom.ACM, New York, NY, USA, 16 pages. https://doi.org/10.1145/3319535.335422
Abstract(s)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.
TypeConference paper
URIhttp://hdl.handle.net/1822/66487
ISBN9781450367479
DOI10.1145/3319535.3354228
Peer-Reviewedyes
AccessOpen access
Appears in Collections:HASLab - Artigos em atas de conferências internacionais (texto completo)

Files in This Item:
File Description SizeFormat 
19CCSb.pdf1,8 MBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID