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

José Bacelar Almeida

University of Minho and INESC TEC

Manuel Barbosa

University of Porto (FCUP) and

INESC TEC

Gilles Barthe

IMDEA Software Institute

MPI for Security and Privacy

Matthew Campagna

Amazon Web Services

Ernie Cohen

Amazon Web Services

Benjamin Gregoire

INRIA Sophia Antipolis

Vitor Pereira

University of Porto (FCUP) and

INESC TEC

Bernardo Portela

University of Porto (FCUP) and

INESC TEC

Pierre-Yves Strub

École Polytechnique

Serdar Tasiran

Amazon Web Services

ABSTRACT We present a machine-checked proof of security for the domain

management protocol of Amazon Web Services’ KMS (Key Man-

agement 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 stan-

dard cryptographic assumptions. The proof is machine-checked in

the EasyCrypt proof assistant and is the largest EasyCrypt devel-

opment to date.

CCS CONCEPTS • Security and privacy → Key management; Logic and veri- fication.

KEYWORDS Provable-Security; Machine-Checked Proof; Key Management

ACM Reference Format: José 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 Security

for AWS Key Management Service. In 2019 ACM SIGSAC Conference on Computer & Communications Security (CCS ’19), November 11–15, 2019, London, United Kingdom. ACM, New York, NY, USA, 16 pages. https://doi.

org/10.1145/3319535.3354228

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]

CCS ’19, November 11–15, 2019, London, United Kingdom © 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.

ACM ISBN 978-1-4503-6747-9/19/11. . . $15.00

https://doi.org/10.1145/3319535.3354228

1 INTRODUCTION Today’s cloud services use sophisticated distributed architectures

and algorithms to make data highly available and durable. To im-

prove security, data at rest is typically encrypted, and decrypted

only when/where necessary. The encryption keys themselves must

be similarly durable and available; however, directly providing all keys towhichever service needs to use them unnecessarily increases

the attack surface. For the most sensitive keys, it is more prudent to

encapsulate them within a separate distributed encryption service.

Such a service allows the creation of new keys, and uses these

keys to encrypt and decrypt data, but does not expose the keys

themselves to clients.

The subject of this paper is the AWS domain management proto-

col (henceforth abbreviated DMP), a distributed encryption service

underlying the Amazon Web Services (AWS) Key Management Ser-

vice (KMS [5]). AWS KMS, a core component of the AWS cloud, lets

AWS customers create and manage encryption keys, providing a

consistent view of encryption/decryption operations across AWS

services, and controlling their use through AWS Identity and Access

Management (IAM). 1 The widespread usage of AWS KMS and the

central role of the DMP justifies a high-assurance security proof,

leveraging recent developments in computer-aided cryptography

such as [3, 4, 7].

In this paper, we present a fully mechanized, concrete proof of

security of the DMP. Informally, the proof shows that the DMP

provides an idealized encryption service.

Security goal. The DMP is designed to protect the confidentiality

of data encrypted under domain keys and guarantee the correct

operation of the interface it provides, even in the presence of a

malicious individual interfering with the inner workings of the sys-

tem. In particular, we consider an adversary that can commission

and decommission hosts and HSMs (Hardware Security Modules),

assumed to be under adversarial control, and manipulate (insert,

delete, modify) messages exchanged between system entities. Our

1 Within AWS KMS, the DMP is used only to encrypt and decrypt customer master

keys, the roots of the customer key hierarchies. The use of these master keys, and the

design of KMS (outside of the DMP itself) is described in [5].

Session 1C: Cloud Security I CCS ’19, November 11–15, 2019, London, United Kingdom

63

goal is to show that such an adversary cannot gain further advan-

tage than possibly causing the system to go unresponsive.

Formally, this security goal is defined using an ideal functionality

and the real-vs-ideal world paradigm, similarly to the Universal

Composability [14] framework. We prove that the DMP is indis-

tinguishable from an idealized encryption service to an arbitrary

external environment that can collude with a malicious insider

adversary. This formalization captures precisely the security that

the rest of AWS KMS needs from the DMP.

Main Theorem. Our main theorem states that the DMP behaves

like an ideal authenticated encryption service. The theorem rules

out attacks from arbitrary computationally bounded adversaries,

under standard cryptographic assumptions for digital signatures,

hash-functions and encryption schemes. Formally, we prove that

the probability of breaking the protocol is smaller than

2 · ( (qops + qhid) · ϵsig + qdom · ϵaead + ϵcr + ϵmrpke + ϵcoll

) ,

where qops and qhid are upper bounds on the number of human op-

erators and HSMs in the system, respectively; qdom upper-bounds

the number of domain keys; ϵsig, ϵaead and ϵcr denote the maxi-

mum probabilities of breaking a standard signature, authenticated

encryption and cryptographic hash function, respectively; ϵmrpke denotes the maximum probability of breaking a multi-recipient

variant of public-key encryption; and ϵcoll is a small statistical term

related to collisions of signature verification keys. The security of

cryptographic signatures, hashes, and authenticated encryption im-

plies that all of the epsilons above (and hence the total probability

of breaking the protocol) are negligible. A more precise statement

of the concrete cryptographic setting and bound can be found in

Sections 4 and 5.

Formalization. The proof is fully machine-checked in EasyCrypt [6],

a proof assistant for cryptographic proofs. The development is

15K lines of code (loc), of which 500 loc comprise the protocol

specification. Besides being the largest EasyCrypt development

to date, the proof combines game-hopping techniques that are

standard in cryptographic proofs, and rich inductive reasoning that

is standard in program verification. The machine-checked proof is

novel for the following reasons:

• We formalize a notion of key secrecy for KMS DMP in the style of

cryptographic APIs [23] and extend prior work in this area by i.

addressing a substantially more complex (distributed) API; and ii.

making explicit which assumptions on the behaviour of human

operators are necessary (as otherwise trivial breaks would be

possible), whilst excluding all non-trivial breaks as in prior work

by reducing to standard cryptographic assumptions.

• We relate the above definition of security with a real-vs-ideal

world security definition for encryption services, by proving

a (reusable) general composition result for combining crypto-

graphic key management APIs with AEAD schemes. Our result-

ing top-level security theorem establishes that KMS DMP is as

good as an ideal authenticated encryption service in the specified

trust model.

• The machine-checked proof follows best proof engineering prac-

tices and favors reusable components, breaking down the verifi-

cation effort in three types of steps:

i. reusable results that lift standard cryptographic assumptions

on signatures and hash functions to idealized versions that

permit reasoning symbolically about complex invariants on

authenticated data structures;

ii. use rich inductive reasoning to prove that intricate authentica-

tion invariants hold in the security experiments, and rewrite

(slice) the code of the security games to make explicit the split

between data which is under adversarial control (due to trivial

strategies that do not contradict the security claim) and data

which is outside of the adversary’s reach; and

iii. build on the previous results to conduct a game hopping proof

that, first, idealizes digital signatures and hash functions, accou-

ting for concrete (negligible) security losses; then modularly

uses the authentication invariants to perform security experi-

ment slicing; and finally reduces the key-secrecy property to

the security of multi-recipient encryption.

Paper Structure. In Section 2 we give a bird’s eye view of our ap-

proach and provide a road-map for the paper, before moving on to

more technical sections. In Section 3 we give a detailed description

of the DMP and of its formalization in EasyCrypt. Then, in Section 4

we formalize the security model that we have adopted and in which

we have proved security of the DMP. In Section 5 we describe the

machine-checked security proof. Section 6 gives an overview of the

improvements to EasyCrypt that were developed during the project.

Section 8 contains a summary of related work, and Section 9 the

concluding remarks.

2 OVERVIEW In this section we present an overview of the DMP goals and inter-

face, and then outline the structure and contents of the EasyCrypt

model and proof (shown in Figure 1).

DMP Concepts. The fundamental unit of security in the DMP is

a domain. Each domain provides an independent distributed en-

cryption functionality using a combination of machines and people

(collectively referred to as entities) which may change over time.

Each entity can participate in multiple domains.

Concretely, a domain is given by its entities, the rules governing

the domain, and a set of (symmetric) domain keys. The entities

are of three types: HSMs, human operators, and front-end hosts. HSMs are the inner security boundary of the DMP, and have a

limited web-based API and no other active physical interfaces to

their operational state. Sensitive cryptographic materials of an HSM

are stored only in volatile memory, and are erased when the HSM

exits operational state, including shutdowns and resets. Domain

keys likewise appear in the clear only in the volatile memory of

HSMs in the domain.

The goal of the DMP is to govern the operations on domain keys

and to manage membership of HSMs in a domain, as well as au-

thorizing operators to act on a domain. HSMs do not communicate

directly with each other. Thus, a central function of the DMP is to

synchronize the domain state between domain participants. For this

purpose, all information about a domain state, including its domain

keys, is transferred and stored in a domain token. A domain token

contains encryptions of the domain keys, and is authenticated in

order to bind these encryptions to the domain state.

Session 1C: Cloud Security I CCS ’19, November 11–15, 2019, London, United Kingdom

64

Domain state is modified through quorum-authenticated com-

mands issued by authorized operators for that domain. Changes

to domain state include modifying the list of trusted participants

in the domain, modifying the set of quorum rules, and periodi-

cally rotating domain keys. Rules on quorum-signed commands

are designed to mitigate attacks by colluding dishonest operators,

namely attacks that might allow such operators to bypass the secu-

rity protections provided by the HSMs. By requiring authorization

from n operators from the domain, the security of operations that

add new entities to a domain is anchored on the assumption that

a quorum of n operators from the domain will always contain at

least one honest operator that follows the protocol, where n is a

security parameter for the domain. A more detailed description of

the domain management operations is included in Section 3, along

with their formalization in EasyCrypt.

DMP Implementation. Not counting the crypto libraries, the imple-

mentation of the DMP protocol is spread across some 16.5K lines

of Java code. The conformance of this code to the protocol level

design is checked via integration tests. Additionally, a formal code

validation mechanism has been built using an extension to a taint

tracking type system (the Checker Framework, [19]). The checked

property is a necessary condition for conformance to the protocol:

a domain key must not be returned as part of the return value of an

API call without first being encrypted by another key. This check

is performed continuously, every time the KMS codebase changes,

and it required only 323 manual annotations to the codebase.

DMP Functional Interface. The DMP provides an encryption func-

tionality for each of its domains. Different domains can vary in the

entities that they trust, their tolerance for dishonesty, and other

security-related parameters. For each domain, the provided en-

cryption functionality has the following interface 2 (formalized in

Section 4):

• New(hdl) creates a new domain key within the domain and as-

sociates it to a key identifier hdl. The result indicates whether the operation was successful.

• Enc(hdl,msg, ad) uses the domain key associated with identifier

hdl to encrypt the payloadmsgwith associated data ad, returning the ciphertext.

• Dec(hdl, cph, ad) uses the domain key associated with identifier

hdl to decrypt ciphertext cph with associated data ad and, if

successful, returns the recovered plaintext.

The goal of the DMP security proof is to show that the DMP pro-

vides an idealized version of this interface (with a small probability

of error). This ideal interface is close to that of standard Authen-

ticated Encryption with Associated Data (AEAD), as detailed in

Section 4, except that operations might fail (with no effect), as one

might expect in a distributed system.

The EasyCrypt security proof consists of three layers. 3 The top

layer gives a real-vs-ideal world security definition for the DMP

and shows that security of a DMP domain in this model follows

2 This interface mentions only domain keys, so the functionality gives a simple way

to separate the security provided by the DMP from its use in the rest of AWS KMS.

3 Note that the scale of the proof does not increase the trusted base, as it is fully

machine-checked by EasyCrypt – indeed, this is the main motivation for machine-

checked provable security; the guarantee that the proof justifies the formalized security

theorem requires only trust in EasyCrypt itself.

Sig (UF)

SigService (Real-Ideal)

Hash (CR)

Hash Chain (Real-Ideal)

Policy (Real-Ideal)

Policy (Bad Event)

AEADTag-Based MR-PKE

ODH Group/KDF

Crypto API (Ind-based)

AEAD Service (Real-Ideal)

Figure 1: Structure of the machine-checked proof

from the secrecy of its domain keys. The next layer shows that the

DMP does indeed preserve the secrecy of domain keys of so-called

“honest" domains (described in Section 3), assuming the secure

implementation of the low-level cryptographic constructions used

to create domain tokens. The bottom layer shows the security of

these low-level constructions.

Proof: Real-vs-ideal World Security.At the top layer of the EasyCrypt proof lies a formal definition of security for encryption services

supported by key management protocols such as the DMP (detailed

in Section 5.1). The definition follows the real-vs-ideal paradigm of

the UC framework (in fact, our proof can be seen as being carried out

in a specific hybrid model in the UC framework, which we discuss

in detail in Appendix A). Intuitively, the ideal functionality leaks

nothing to the (adversarial) environment except the length of the

data being encrypted, and implements decryption by maintaining a

table mapping pairs (cph, ad) to messages. Ideal encryption always

returns encryptions of 0 ℓ , where ℓ is the encrypted data length,

and adds a new entry to this table; decryption simply does a lookup

from the table (rather than calling the decryption function).

At this level we reduce the real-vs-ideal world security of the

DMP to an indistinguishability-based security property that cap-

tures the secrecy of domain keys. This means that in the lower

levels of the proof we do not need to reason about how domain

keys are used; it suffices to prove that the DMP keeps domain keys

hidden from the attacker’s view.

Proof: Indistinguishability-based security. The second layer of results proves that the protocol hides all information about domain keys

from the adversary’ view. This is formalized as a cryptographic

API [23] that guarantees domain key secrecy. The model captures

the actions of a malicious insider adversary by allowing the do-

main management operations to consist of multiple adversarially

orchestrated steps. The main challenge in this proof, formalized

using the game-hopping technique, is to establish the invariants

that govern the state of security experiments in each hop. These in-

variants combine properties that arise from standard cryptographic

Session 1C: Cloud Security I CCS ’19, November 11–15, 2019, London, United Kingdom

65

Figure 2: High-level view of the DMP. assumptions (e.g., absence of collisions and signature forgeries)

with the inductive argument that justifies the soundness of the do-

main update operations carried out by honest operators, HSMs and

hosts. It is by the joint action of these two types of guarantees that

the domain management policy excludes dishonest entities from

explicitly obtaining information on domain keys. The proof at this

layer reduces the security of the API to the security of lower-level

abstractions, all of which are formalized in the indistinguishability

style, in order to facilitate the game-hopping technique. The details

are discussed in Section 5.3.

Proof: Low-level abstractions. The lower layer of security results de-

fines idealized versions of digital signature services, hash maps and

certification of identity keys by human operators. It also contains

proofs that these abstractions are indistinguishable from real-world

instantiations down to standard cryptographic assumptions, which

can then be used to make concrete the bounds in the theorems

established at the higher layers in the development. At this level,

we also formalize the specific flavor of (multi-recipient) public-key

encryption that is used by the DMP.

This lower layer in the proof is meant to modularize various

components, for three purposes: 1) lifting assumptions formalized

as bad events, such as unforgeability and collision resistance, to

indistinguishability definitions, allowing the higher-level parts of

the proof to be solely based on indistinguishability game hops; 2) al-

lowing for reuse of the abstractions across the project (e.g., we reuse

the signature abstraction for both operator signatures and HSM

signatures); and 3) allow for multiple instantiations of the same

underlying primitive (e.g., an encryption scheme with different

constructions). This part of the proof is presented in Section 5.2.

3 KMS DOMAIN MANAGEMENT PROTOCOL 3.1 Detailed Description A high-level operational view of the DMP is presented in Figure 2

(reproduced from [5]). Operators issue commands, HSMs manipu-

late the contents of domain tokens, and coordinator servers propa-

gate updated domain tokens to each HSM in a domain to keep their

domain states approximately synchronized (the latter are not shown

and assumed for the purpose of the proof to be under adversarial

control).

We now describe the core concepts and mechanisms involved

in the DMP at the level of the mathematical model of the protocol

that forms the basis of the formal proof of security. We begin by

introducing the notion of a domain state, the different entities in the

system and what assumptions we make about their behavior; we

then explain the roles of these entities in domain state transitions,

and conclude with an intuitive explanation of the security rationale

underlying the design.

Protocol entities and assumed behavior. The DMP is implemented

using three types of entities: HSMs, hosts, and operators. Each entity

is identified with its identity (signature verification) key. A genuine entity is (the identity key of) anHSM/Host/Operator that behaves as

specified by the DMP. A domain might include non genuine identity

keys of any entity type, e.g. keys created by amalicious entity. HSMs

perform the actual encryption and decryption operations, 45

and are

the only entities allowed to manipulate domain keys in cleartext.

Operators are responsible for certifying identity keys: they sign

statements claiming that a given identity key represents a genuine

HSM, host or operator. 6 Honest operators only sign statements

that are true, i.e. if an honest operator claims a key is that of a

genuine HSM, the key is in fact genuine. Conversely, dishonest

operators, while themselves genuine, might sign statements that

are false. Note that we assume only that an honest operator can

tell whether another operator is genuine, not whether he is honest.

Genuine but dishonest operators model insider threats, possibly

colluding with external adversaries. Non-genuine operators model

arbitrary rogue identity keys that the adversary may also create in

its attack. For the purpose of this paper, the quorum rule is defined

by a security parameter n, which describes the minimum number

of operators of the domain that must authorize an update over

the domain state. Our security analysis is anchored on a global

assumption that any set of n genuine operators contains at least

one honest operator that follows the protocol. For example, a rule

imposing that a quorum consists of a set of at least n = 2 operators

from the domain guarantees that it requires at least two dishonest

operators of the domain to break security.

Finally, hosts are the service endpoints. Although the actions of

hosts in AWS KMS are more complex, our analysis focuses on the

crucial role of honest hosts in directing cryptographic operations

to honest domains: 7 as entry points in the system, hosts keep track

of domain states and check that they are updated consistently with

the domain management rules by HSMs. (Although we have not

formalized this, in Appendix B we discuss how our proof implies

security in a model where corrupt hosts are considered.)

4 What we call HSMs are, in AWS KMS, running instances of FIPS 140-2 certified

hardware security modules. They generate fresh identity and agreement key pairs

when they boot, and store them only in volatile memory; the instance is effectively

destroyed when power is lost. This simplifies physical protection — it suffices to

guarantee that the machine cannot be physically attacked without losing power.

5 In our protocol model, HSMs are conceptually stateless beyond their identity and

agreement key pairs. In AWS KMS, HSMs maintain the current domain state for each

domain they operate on, allowing their behavior to be more tightly controlled.