A machine-checked proof of security for AWS key management service

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

doi:10.1145/3319535.3354228

A machine-checked proof of security for AWS key management service

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

École Polytechnique

Universidade de Minho
Amazon Machine Learning Solutions Lab
University of Porto
IMDEA Software Institute
INRIA

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	CCS 2019 - Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security
Publisher	Association for Computing Machinery
Pages	63-78
Number of pages	16
ISBN (Electronic)	9781450367479
DOIs	https://doi.org/10.1145/3319535.3354228
Publication status	Published - 6 Nov 2019
Event	26th ACM SIGSAC Conference on Computer and Communications Security, CCS 2019 - London, United Kingdom Duration: 11 Nov 2019 → 15 Nov 2019

Publication series

Name	Proceedings of the ACM Conference on Computer and Communications Security
ISSN (Print)	1543-7221

Conference

Conference	26th ACM SIGSAC Conference on Computer and Communications Security, CCS 2019
Country/Territory	United Kingdom
City	London
Period	11/11/19 → 15/11/19

Keywords

Key Management
Machine-Checked Proof
Provable-Security

Access to Document

10.1145/3319535.3354228

Cite this

Almeida, J. B., Campagna, M., Pereira, V., Barbosa, M., Cohen, E., Portela, B., Tasiran, S., Barthe, G., Gregoire, B., & Strub, P. Y. (2019). A machine-checked proof of security for AWS key management service. In CCS 2019 - Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (pp. 63-78). (Proceedings of the ACM Conference on Computer and Communications Security). Association for Computing Machinery. https://doi.org/10.1145/3319535.3354228

@inproceedings{110cae5319a7459cbe9bf8f682dd0c6a,

title = "A machine-checked proof of security for AWS key management service",

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.",

keywords = "Key Management, Machine-Checked Proof, Provable-Security",

author = "Almeida, \{Jos{\'e} Bacelar\} and Matthew Campagna and Vitor Pereira and Manuel Barbosa and Ernie Cohen and Bernardo Portela and Serdar Tasiran and Gilles Barthe and Benjamin Gregoire and Strub, \{Pierre Yves\}",

note = "Publisher Copyright: {\textcopyright} 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.; 26th ACM SIGSAC Conference on Computer and Communications Security, CCS 2019 ; Conference date: 11-11-2019 Through 15-11-2019",

year = "2019",

month = nov,

day = "6",

doi = "10.1145/3319535.3354228",

language = "English",

series = "Proceedings of the ACM Conference on Computer and Communications Security",

publisher = "Association for Computing Machinery",

pages = "63--78",

booktitle = "CCS 2019 - Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security",

}

Almeida, JB, Campagna, M, Pereira, V, Barbosa, M, Cohen, E, Portela, B, Tasiran, S, Barthe, G, Gregoire, B & Strub, PY 2019, A machine-checked proof of security for AWS key management service. in CCS 2019 - Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. Proceedings of the ACM Conference on Computer and Communications Security, Association for Computing Machinery, pp. 63-78, 26th ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, United Kingdom, 11/11/19. https://doi.org/10.1145/3319535.3354228

A machine-checked proof of security for AWS key management service. / Almeida, José Bacelar; Campagna, Matthew; Pereira, Vitor et al.
CCS 2019 - Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, 2019. p. 63-78 (Proceedings of the ACM Conference on Computer and Communications Security).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A machine-checked proof of security for AWS key management service

AU - Almeida, José Bacelar

AU - Campagna, Matthew

AU - Pereira, Vitor

AU - Barbosa, Manuel

AU - Cohen, Ernie

AU - Portela, Bernardo

AU - Tasiran, Serdar

AU - Barthe, Gilles

AU - Gregoire, Benjamin

AU - Strub, Pierre Yves

PY - 2019/11/6

Y1 - 2019/11/6

N2 - 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.

AB - 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.

KW - Key Management

KW - Machine-Checked Proof

KW - Provable-Security

U2 - 10.1145/3319535.3354228

DO - 10.1145/3319535.3354228

M3 - Conference contribution

AN - SCOPUS:85075915733

T3 - Proceedings of the ACM Conference on Computer and Communications Security

SP - 63

EP - 78

BT - CCS 2019 - Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security

PB - Association for Computing Machinery

T2 - 26th ACM SIGSAC Conference on Computer and Communications Security, CCS 2019

Y2 - 11 November 2019 through 15 November 2019

ER -

Almeida JB, Campagna M, Pereira V, Barbosa M, Cohen E, Portela B et al. A machine-checked proof of security for AWS key management service. In CCS 2019 - Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery. 2019. p. 63-78. (Proceedings of the ACM Conference on Computer and Communications Security). doi: 10.1145/3319535.3354228

A machine-checked proof of security for AWS key management service

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this