research-article

Open access

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

Authors:

José Bacelar Almeida,

Manuel Barbosa,

Matthew Campagna,

Benjamin Gregoire,

Bernardo Portela,

Pierre-Yves Strub,

Serdar TasiranAuthors Info & Claims

CCS '19: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security

Pages 63 - 78

https://doi.org/10.1145/3319535.3354228

Published: 06 November 2019 Publication History

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.

Supplementary Material

WEBM File (p63-portela.webm)

Download
133.75 MB

References

[1]

Michel Abdalla, Mihir Bellare, and Phillip Rogaway. 1998. DHIES: An Encryption Scheme Based On The Diffie-Hellman Problem. Contributions to IEEE P1363a.(Sept. 1998).

[2]

Michel Abdalla, Mihir Bellare, and Phillip Rogaway. 2001. The Oracle Diffie-Hellman Assumptions and an Analysis of DHIES. In CT-RSA 2001 (LNCS), David Naccache (Ed.), Vol. 2020. Springer, Heidelberg, 143--158. https://doi.org/10.1007/3--540--45353--9_12

[3]

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and François Dupressoir. 2016. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. InFSE 2016 (LNCS), Thomas Peyrin (Ed.), Vol. 9783. Springer, Heidelberg, 163--184. https://doi.org/10.1007/978--3--662--52993--5_9

[4]

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, and Vitor Pereira. 2017. A Fast and Verified Software Stack for Secure Function Evaluation. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM, 1989--2006. https://doi.org/10.1145/3133956.3134017

Digital Library

[5]

Amazon Web Services (AWS). 2018. AWS Key Management Service Crypto-graphic Details. (August 2018). https://d1.awsstatic.com/whitepapers/KMS-Cryptographic-Details.pdf.

[6]

Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2013. EasyCrypt: A Tutorial. In Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures (Lecture Notes in Computer Science), Alessandro Aldini, Javier López, and Fabio Martinelli(Eds.), Vol. 8604. Springer, 146--166. https://doi.org/10.1007/978--3--319--10082--1_6

[7]

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO 2011 (LNCS), Phillip Rogaway (Ed.), Vol. 6841. Springer, Heidelberg, 71--90. https://doi.org/10.1007/978--3--642--22792--9_5

[8]

Mihir Bellare, Alexandra Boldyreva, and Jessica Staddon. 2003. Randomness Reuse in Multi-recipient Encryption Schemeas. In PKC 2003 (LNCS), Yvo Desmedt(Ed.), Vol. 2567. Springer, Heidelberg, 85--99. https://doi.org/10.1007/3--540--36288--6_7

[9]

Bruno Blanchet. 2006. A Computationally Sound Mechanized Prover for Security Protocols. In 2006 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, 140--154. https://doi.org/10.1109/SP.2006.1

Digital Library

[10]

Bruno Blanchet. 2018. Composition Theorems for CryptoVerif and Application to TLS 1.3. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9--12, 2018. IEEE Computer Society, 16--30. https://doi.org/10.1109/CSF.2018.00009

[11]

Bruno Blanchet and Avik Chaudhuri. 2008. Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage. In 2008 IEEE Symposiumon Security and Privacy (S&P 2008), 18--21 May 2008, Oakland, California, USA. IEEE Computer Society, 417--431. https://doi.org/10.1109/SP.2008.12

Digital Library

[12]

Matteo Bortolozzo, Matteo Centenaro, Riccardo Focardi, and Graham Steel. 2010. Attacking and fixing PKCS#11 security tokens. In ACM CCS 10, Ehab Al-Shaer,Angelos D. Keromytis, and Vitaly Shmatikov (Eds.). ACM Press, 260--269. https://doi.org/10.1145/1866307.1866337

[13]

Christian Cachin and Nishanth Chandran. 2009. A Secure Cryptographic Token Interface. In Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, July 8--10, 2009. IEEE Computer Society, 141--153.

Digital Library

[14]

Ran Canetti. 2001. Universally Composable Security: A New Paradigm for Cryptographic Protocols. In 42nd FOCS. IEEE Computer Society Press, 136--145.https://doi.org/10.1109/SFCS.2001.959888

[15]

Ran Canetti, Yevgeniy Dodis, Rafael Pass, and Shabsi Walfish. 2007. Universally Composable Security with Global Setup. In TCC 2007 (LNCS), Salil P. Vadhan(Ed.), Vol. 4392. Springer, Heidelberg, 61--85. https://doi.org/10.1007/978--3--540--70936--7_4

[16]

Stéphanie Delaune, Steve Kremer, and Graham Steel. 2008. Formal Analysis of PKCS#11. In Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, USA, 23--25 June 2008. IEEE Computer Society, 331--344.

Digital Library

[17]

Steve Kremer, Robert Künnemann, and Graham Steel. 2013. Universally Composable Key-Management. In ESORICS 2013 (LNCS), Jason Crampton, Sushil Jajodia, and Keith Mayes (Eds.), Vol. 8134. Springer, Heidelberg, 327--344. https://doi.org/10.1007/978--3--642--40203--6_19

[18]

Steve Kremer, Graham Steel, and Bogdan Warinschi. 2011. Security for Key Management Interfaces. In Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27--29 June, 2011. IEEE Computer Society, 266--280. https://doi.org/10.1109/CSF.2011.25

Digital Library

[19]

Matthew M. Papi, Mahmood Ali, Telmo Luis Correa, Jr., Jeff H. Perkins, and Michael D. Ernst. 2008. Practical Pluggable Types for Java. In Proceedings of the 2008 International Symposium on Software Testing and Analysis (ISSTA '08). ACM,New York, NY, USA, 201--212. https://doi.org/10.1145/1390630.1390656

[20]

Phillip Rogaway. 2006. Formalizing Human Ignorance. In Progress in Cryptology- VIETCRYPT 06 (LNCS), Phong Q. Nguyen (Ed.), Vol. 4341. Springer, Heidelberg,211--228.

[21]

Victor Shoup. 2001. A Proposal for an ISO Standard for Public Key Encryption(version 2.1). (2001). https://www.shoup.net/papers/iso-2_1.pdf.

[22]

Victor Shoup. 2001. A Proposal for an ISO Standard for Public Key Encryption. Cryptology ePrint Archive, Report 2001/112. (2001). http://eprint.iacr.org/2001/112.

[23]

Thomas Shrimpton, Martijn Stam, and Bogdan Warinschi. 2016. A Modular Treatment of Cryptographic APIs: The Symmetric-Key Case. In CRYPTO 2016, Part I (LNCS), Matthew Robshaw and Jonathan Katz (Eds.), Vol. 9814. Springer, Heidelberg, 277--307. https://doi.org/10.1007/978--3--662--53018--4_11

Digital Library

Cited By

Koh WKoh JDai B(2024)Robust image classification system via cloud computing, aligned multimodal embeddings, centroids and neighboursMachine Learning with Applications10.1016/j.mlwa.2024.100583(100583)Online publication date: Aug-2024
https://doi.org/10.1016/j.mlwa.2024.100583
Linvill KKaki GWustrow E(2023)Verifying Indistinguishability of Privacy-Preserving ProtocolsProceedings of the ACM on Programming Languages10.1145/36228497:OOPSLA2(1442-1469)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622849
Haselwarter PRivas EVan Muylder AWinterhalter TAbate CSidorenco NHriţcu CMaillard KSpitters B(2023)SSProve: A Foundational Framework for Modular Cryptographic Proofs in CoqACM Transactions on Programming Languages and Systems10.1145/359473545:3(1-61)Online publication date: 20-Jul-2023
https://dl.acm.org/doi/10.1145/3594735
Show More Cited By

Index Terms

A Machine-Checked Proof of Security for AWS Key Management Service
1. Security and privacy
  1. Cryptography
    1. Key management
  2. Formal methods and theory of security
    1. Formal security models

Recommendations

Secure key management in cloud computing
InfoSec '14: Proceedings of the 2014 Information Security Curriculum Development Conference

In this paper, we will discuss Secure Key Management in Cloud Computing. We discuss the basics of what a key is to how it is used in cloud computing. This paper looks at the types and states of a key. It is then followed by the cloud computing model and ...
Database security management for healthcare SaaS in the Amazon AWS Cloud
ISCC '12: Proceedings of the 2012 IEEE Symposium on Computers and Communications (ISCC)

Software as a Service (SaaS) applications fully-exploiting the potential of elastic Cloud computing infrastructures naturally are enabling new ubiquitous access scenarios for nomadic users, such as market salesmen and home healthcare medical assistants. ...
A non-interactive deniable authentication scheme based on designated verifier proofs

A deniable authentication protocol enables a receiver to identify the source of the given messages but unable to prove to a third party the identity of the sender. In recent years, several non-interactive deniable authentication schemes have been ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '19: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security

November 2019

2755 pages

ISBN:9781450367479

DOI:10.1145/3319535

General Chairs:
Lorenzo Cavallaro
King's College London, UK
,
Johannes Kinder
Bundeswehr University Munich, Germany
,
Program Chairs:
XiaoFeng Wang
Indiana University, USA
,
Jonathan Katz
George Mason University, USA

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 November 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Portuguese Foundation for Science and Technology (FCT)

Conference

CCS '19

Sponsor:

SIGSAC

CCS '19: 2019 ACM SIGSAC Conference on Computer and Communications Security

November 11 - 15, 2019

London, United Kingdom

Acceptance Rates

CCS '19 Paper Acceptance Rate 149 of 934 submissions, 16%;

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
2,290
Total Downloads

Downloads (Last 12 months)274
Downloads (Last 6 weeks)24

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Koh WKoh JDai B(2024)Robust image classification system via cloud computing, aligned multimodal embeddings, centroids and neighboursMachine Learning with Applications10.1016/j.mlwa.2024.100583(100583)Online publication date: Aug-2024
https://doi.org/10.1016/j.mlwa.2024.100583
Linvill KKaki GWustrow E(2023)Verifying Indistinguishability of Privacy-Preserving ProtocolsProceedings of the ACM on Programming Languages10.1145/36228497:OOPSLA2(1442-1469)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622849
Haselwarter PRivas EVan Muylder AWinterhalter TAbate CSidorenco NHriţcu CMaillard KSpitters B(2023)SSProve: A Foundational Framework for Modular Cryptographic Proofs in CoqACM Transactions on Programming Languages and Systems10.1145/359473545:3(1-61)Online publication date: 20-Jul-2023
https://dl.acm.org/doi/10.1145/3594735
Barbosa MBarthe GGrégoire BKoutsos AStrub P(2023)Mechanized Proofs of Adversarial Complexity and Application to Universal ComposabilityACM Transactions on Privacy and Security10.1145/358996226:3(1-34)Online publication date: 19-Jul-2023
https://dl.acm.org/doi/10.1145/3589962
Jeziorski KMcFadden DLennon R(2023)Verification of Certificate Authorities (CAs) and integration with cloud providers for enhanced security2023 Cyber Research Conference - Ireland (Cyber-RCI)10.1109/Cyber-RCI59474.2023.10671564(1-8)Online publication date: 24-Nov-2023
https://doi.org/10.1109/Cyber-RCI59474.2023.10671564
Cremers CFontaine CJacomme C(2022)A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols2022 IEEE Symposium on Security and Privacy (SP)10.1109/SP46214.2022.9833800(125-141)Online publication date: May-2022
https://doi.org/10.1109/SP46214.2022.9833800
Zou RLiu YZang QWei BLiu CHou JZhou YChe J(2022)Research and Development of Cyber Cyberspace Resilience Technology2022 International Conference on Information Technology, Communication Ecosystem and Management (ITCEM)10.1109/ITCEM57303.2022.00014(23-28)Online publication date: Dec-2022
https://doi.org/10.1109/ITCEM57303.2022.00014
Dupressoir FKohbrok KOechsner S(2022)Bringing State-Separating Proofs to EasyCrypt A Security Proof for Cryptobox2022 IEEE 35th Computer Security Foundations Symposium (CSF)10.1109/CSF54842.2022.9919671(227-242)Online publication date: Aug-2022
https://doi.org/10.1109/CSF54842.2022.9919671
Rungta N(2022)A Billion SMT Queries a Day (Invited Paper)Computer Aided Verification10.1007/978-3-031-13185-1_1(3-18)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13185-1_1
Barbosa MBarthe GGrégoire BKoutsos AStrub PKim YKim JVigna GShi E(2021)Mechanized Proofs of Adversarial Complexity and Application to Universal ComposabilityProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security10.1145/3460120.3484548(2541-2563)Online publication date: 12-Nov-2021
https://dl.acm.org/doi/10.1145/3460120.3484548
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents