Problem statement: what kind of problem is presented by the authors and why this problem is important?
- Approach & Design: briefly describe the approach designed by the authors
- Strengths and Weaknesses: list the strengths and weaknesses, in your opinion
- Evaluation: how did the authors evaluate the performance of the proposed scheme? What kind of workload was designed and used?
- Conclusion: by your own judgement.
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.
ing 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 permissions@acm.org.
CCS ’19, November 11–15, 2019, London, United Kingdom
© 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.
ACM ISBN 9
78
-1-4503-
67
47-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
https://doi.org/10.1145/3319535.3354228
https://doi.org/10.1145/3319535.3354228
https://doi.org/10.1145/3319535.3354228
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. This
provides defense in depth, and potentially allows the proof of additional security
properties not described here.
6
In AWS KMS, these statements are actually commands to perform particular actions,
such as a command requesting an HSM to add or remove HSMs or operators from a
domain; such a command implicitly carries with it the certification from the command
signers that the added entities are genuine. Note also that operators represent human
operators, which play many additional security roles in the system; we describe only
as much as is needed to justify the presented
security proof.
7
Note that it is always safe to add domain-local secrets that appear only encrypted
by keys of the domain. This can be done by allowing such secrets to only be created
by an HSM of the domain (that immediately encrypts the new secret under a domain
key), and to be re-encrypted from one domain key to another domain key of the same
domain. For example, in AWS KMS, customer master keys are treated in this way, and
hosts are also responsible for issuing the commands that manage the creation and
usage of such keys.
Session 1C: Cloud Security I CCS ’19, November 11–15, 2019, London, United Kingdom
66
Domain States, Tokens and Key Usage. A domain state logically
consists of two parts: 1) a domain trust describing the administrative
state of the domain—its entities and rules of operation—and 2) the
actual domain keys. The trust components include a unique name
of the domain, the set of entities of each type treated as genuine for
the domain and the agreement keys for each HSM in the domain.
The trust also includes a set of quorum rules defining what sets
of operators (quorums) are considered trustworthy. Domain state
modifications must be authorized by one of these quorums. Since
the trust state of a domain can evolve over time (as operators, HSMs,
and hosts are added and removed from the domain), the trust also
includes the cryptographic fingerprint (hash) of the previous trust
from which it was derived (by means of a trust update). Domain
keys are kept secret from all entities other than the HSMs of the
domain, whereas the domain trust only has to be authenticated.
The concrete trust representation is signed by an HSM of the trust.
To provide the encryption functionality of a domain, its HSMs
need access to the domain keys, which should not be exposed to
other entities. To allow this, the domain state is concretely repre-
sented by a domain token signed by an HSM of the trust, which
includes an encryption of the domain keys. This representation
authenticates the state and binds the encrypted data to the trust;
domain keys are decryptable only by the HSMs of the trust.
To allow encryptions between HSMs of a domain, each HSM
has a long-term Diffie-Hellman agreement key pair. It certifies its
(public) agreement key as its own by signing it with its identity
key. To encrypt the domain keys for the other HSMs in a domain,
an HSM first encrypts them under an ephemeral symmetric key.
It then generates an ephemeral Diffie-Hellman key pair, uses DH
agreement with this key pair and each of the agreement keys of
the domain HSMs to compute a shared secret with each HSM,
uses a key derivation function (KDF) on each shared secret to pro-
duce a set of symmetric keys, each of which is used to encrypt the
ephemeral symmetric key. The result is a multi-recipient encryp-
tion of the domain keys to all the other HSMs in the domain based
on DHIES [1]. This scheme has performance advantages: cipher-
texts to all the HSMs in the domain take less bandwidth and can
be batch-generated faster. The final domain token includes all of
these encryptions, the public ephemeral Diffie-Hellman key, and
the domain trust, all signed by the HSM creating the token. When
an HSM receives a command (other than to create a new domain),
it also gets a domain token on which to operate
8
(see Figure 2); it
decrypts the domain token, and uses it to process the request.
Domain State Transitions. The security of a domain depends criti-
cally on all of the HSMs of a domain being genuine. For example, if
an adversary could somehow introduce an identity into a domain
for which he holds the private signing key, he could use this identity
to sign an agreement key for which he holds the private key, have
another member update the domain, and use his fake agreement
key to decrypt the new domain token, breaking security. How-
ever, the HSMs performing the domain update operations (adding
and removing entities) do not carry with them a state that allows
them to recognize the identity keys of genuine entities. Domain
8
In AWS KMS, these domain states are typically cached within the HSMs, rather
than being explicitly provided as part of a command. This provides slightly stronger
security guarantees, e.g. wrt state rollback.
updates where HSMs modify trusts therefore rely on authorizations
(attestations) of identity keys produced by operators, as follows.
An HSMwill sign a new trust with any set of entities and quorum
rules, if that trust is initial (i.e., has no predecessor fingerprint).9 To
modify an existing trust to create a new trust, an HSM checks that 1)
it is an HSM of the existing trust, and 2) every entity in the new trust
is either in the old trust or is certified (for the domain) by a quorum
of operators of the existing trust. If these checks are successful, it
creates and signs a new trust with the updated information, with
the fingerprint of the existing trust as predecessor of the new one.
A host processing requests for a domain maintains in his state a
trust for the domain; his commands can only be processed by HSMs
in the trust.
10
As the trust of a domain evolves, hosts update their
version of the trust. A host of a domain is initially given the initial
trust of the domain. A host updates to a new trust only if 1) the
predecessor fingerprint of new trust is the fingerprint of its current
trust, and 2) the new trust is signed by an HSM of its current trust.
Invariant: an honest trust stays honest. A trust is honest if and only
if its HSMs, hosts, and operators are all genuine, every quorum
of operators (as defined by its quorum rules) contains an honest
operator, and its predecessor trust (if any) is honest. A crucial
property of the DMP is that, if a domain is initially created with
an honest trust, then the domain will remain honest as updates
are performed by HSMs. Note that this guarantee is enforced even
though the HSM performing the updates keeps no state other than
its own signing and agreement keys:
11
such an HSM has no way
of distinguishing genuine operators from non-genuine ones, and it
depends on attestation by operators to identify genuine HSMs.
Intuitively, the trust honesty property is preserved by the fol-
lowing inductive reasoning, which we formalize in our machine-
checked proof. The base case is trivial. In the inductive step, an HSM
is asked to update an honest existing trust to a new trust, and it
performs checks (1-2) described above. By the quorum requirement
on honest trusts, any entity certified by a quorum in the existing
trust is guaranteed to be genuine. By check 2) above, the HSM will
therefore guarantee that all entities in the new trust are genuine. To
show that honesty is preserved it remains to prove that the quorum
requirement is satisfied by the new trust. This is guaranteed by
the global assumption on the security parameter n: since we just
proved all operators in the new trust must be genuine, it must be
the case that any subset of operators of size at least n contains at
least one honest operator. Thus, if the current trust is honest, the
successor trust (once signed by an HSM of the predecessor trust) is
also honest. By the observation of the last paragraph, the actions
of a host guarantee that if the host starts out with an honest trust,
the host trust will remain honest.
Allowing Dishonest Domains. The DMP presented here allows dis-
honest domains to share entities with honest domains. In AWS
KMS, this is prevented by having HSMs cache domain states, and
9
This corresponds to a domain creation request in AWS KMS.
10
Commands are in fact issued by first obtaining an ephemeral symmetric key token
generated by an HSM of the trust, with the plaintext key decryptable only using
either a domain key or by the host requesting the token. We do not describe this
communication mechanism in this paper.
11
Again, AWS KMS caches domain tokens, rather than them being explicitly provided
for updates; the DMP proof shows that this caching is not needed for the current
security proof.
Session 1C: Cloud Security I CCS ’19, November 11–15, 2019, London, United Kingdom
67
type HId. (∗ Identities of HSMs ∗)
type OpId. (∗ Identities of Operators ∗)
type HstId. (∗ Identities of Hosts ∗)
type DomId. (∗ Identities of Domains ∗)
(∗ Trust data (genuine HSMs) and metadata ∗)
type Fpr.
typeQuorum = OpId fset ∗ int.
typeMetadata =Quorum ∗ Fpr option ∗ HstId fset ∗ DomId.
type Trust = (HId fset) ∗Metadata.
(∗ Domain keys in plaintext and encrypted form ∗)
type Keys = (Handle,Key) fmap.
type EKeys = MCTxt.
(∗ Unwrapped domain token ∗)
type TkData = { td_inst: bool; td_trust: Trust; td_skeys: Keys;
}.
(∗Wrapped domain token and trust ∗)
type TkWrapped = { tkw_ekeys: EKeys; tkw_signer: HId; tkw_sig: signature; }.
type Token = { tk_inst: bool; tk_trust: Trust; tk_wdata: TkWrapped; }.
Figure 3: EasyCrypt Definitions for Domain Tokens
using additional commands by which an HSM attests to its current
domains. This allows operators to check that an HSM is loaded
up with honest domain tokens, and so will never process requests
using dishonest domain tokens. The current proof shows that lock-
ing down the HSMs in this way is not needed to achieve domain
security. Note that the current proof nevertheless still applies to
the security of AWS KMS, since the latter’s stricter rules simply
restrict adversarial action.
3.2 Formalization in EasyCrypt
Background on EasyCrypt. EasyCrypt is an interactive proof assis-
tant for verifying the security of cryptographic constructions in the
computational model. EasyCrypt adopts the code-based approach,
in which primitives, security goals and hardness assumptions are
expressed as probabilistic programs. EasyCrypt uses formal tools
from program verification and programming languages to justify
cryptographic reasoning, providing several program logics. We now
describe the formalization of the DMP in EasyCrypt.
12
Trusts and Domain Tokens. Figure 3 shows the EasyCrypt declara-
tions for domain tokens. The HId type is a pair holding the signing
key of the HSM and its public agreement key. The OpId type is simply
the signing key for the human operator. Type TkWrapped corresponds
to signed data structures, which we reuse both for signed trusts and
signed domain tokens. Technically, this simplifies the writing of
invariants, as we only need to deal with one encoding function into
the domain of signature schemes. We then syntactically distinguish
(using bit tk_inst) installable signed trusts—only these can be installed
in hosts—from signed domain tokens that also carry domain keys.
Wrapping and Unwrapping. Figure 4 shows how we formalize in
EasyCrypt the operations carried out by HSMs to wrap (i.e., creat-
ing a data structure that is digitally signed and contains encrypted
domain keys) and unwrap (verifying authenticity and recover clear-
text domain keys) domain tokens. Operator checkToken performs con-
sistency checks on tokens and performs signature verification; in
particular, it also checks that the encrypted keys cph are encrypted
12
Notation: In EasyCrypt tup.1 denotes the first element of a tuple; notation is over-
loaded for fields in records, as in rec.field.
op proj_pks (hids: HId fset) : MPk = image snd hids.
(∗ Operator used for both unwrap and trust updates ∗)
op checkToken(inst : Installable, old new : Trust, tkw : TkWrapped)
=
let (cphs, sid, sig) = (tkw.tkw_ekeys, tkw.tkw_signer, tkw.tkw_sig) in
let msg = encode_msg (new,cphs,sid,inst) in
verify(sid.1, msg, sig) ∧ proj_pks (tr_mems old) = fdom cphs ∧
sid ∈ tr_mems old.
proc wrap(hid : HId,td : TkData) : Token = {
(inst, trust, keys)← (td.td_inst, td.td_trust, td.td_skeys);
mem← tr_mems trust;
tag← encode_tag trust;
ptxt← encode_ptxt keys;
ekeys←$ mencrypt (proj_pks mem) tag ptxt;
msg← encode_msg (trust, ekeys, hid, inst);
sig← SigSch.sign(hid.1, msg);
tkw← { tkw_ekeys = ekeys; tkw_signer = hid; tkw_sig = sig };
return { tk_inst = inst; tk_trust = trust; tk_wdata = tkw; };
}
proc unwrap(hid : HId, tk : Token) : TkData option = {
rtd← None;
(inst, trust, data)← (tk.tk_inst, tk.tk_trust, tk.tk_wdata);
(∗ Signer must be in trust: so we call check with trust as old ∗)
if (checkToken inst trust tk.tk_wdata ∧
hid ∈ tr_mems trust ∧ hid_in hid benc_keys) {
(ekey, dkey)← benc_keys[hid.1];
(tag, cphs)← (encode_tag trust, data.tkw_ekeys);
cph← cphs[ekey];
optxt← decrypt dkey tag cph;
if (optxt,None)
skeys← decode_ptxt optxt;
rtd← Some { td_inst = inst; td_trust = trust; td_skeys = skeys; };
}
return rtd;
}
Figure 4: HSM Operations for Domain Token (un)wrapping.
to all HSM members of the trust (proj_pks(tr_mems old)=fdom cphs), and that
the signer is a member of the trust (sid ∈ tr_mems old).13
Encryption is formalized as tag-based multi-recipient public-
key encryption [8, 22]. Intuitively, this is a variant of public-key
encryption where one can provide multiple agreement keys to
the encryption algorithm, so that the resulting ciphertext can be
decrypted independently by multiple recipients using only their
individual private agreement keys. Encryption therefore takes a set
of public keys (type MPk), and we model ciphertexts as a map from
public keys to sub-ciphertexts that contain only the parts of the full
ciphertext that each recipient needs to decrypt. This abstraction
permits capturing the specific flavor of public-key encryption used
in the DMP: the multi-recipient syntax permits modeling schemes
that minimize bandwidth and encryption time via the reuse of
randomness across multiple ciphertexts. The construction is tag-
based, because it binds the ciphertext to the meta-data of the token
(parameter tag) thereby preventing an adversary from porting such
a ciphertext from a domain token associated to an honest trust
to a domain token that is under its control. We describe how we
formalized the proof of security for the encryption scheme used
in AWS KMS in Section 5, and how we showed that the security
model it satisfies is sufficient for the purposes of the DMP.
Trust management operations. Figure 5 shows the modeling of host
operations. This consists of checking a signed trust (token) for
consistency and its relation to its predecessor. The latter means
checking that the signer is in the predecessor trust, and that the
13
When this operator is used in unwrap we have old=trust. The same operator is used
for checking updates by both hosts and HSMs; in that case, the signer must be an HSM
of the predecessor trust as well.
Session 1C: Cloud Security I CCS ’19, November 11–15, 2019, London, United Kingdom
68
op tr_initial(trust : Trust) = tfpr trust = None.
op checkTrustProgress(old new : Trust) = old = tfpr new.
proc installUpdatedTrust(hstid : HstId, tk : Token) : bool = {
b← false;
if (hstid ∈ HstPolSrv.hosts_tr) {
old← hosts_tr[hstid];
(∗ Signer must be in old trust and trust must be installable ∗)
b← tk.tk_inst ∧ checkToken tk.tk_inst old tk.tk_trust tk.tk_wdata ∧
hstid ∈ hosts_tr ∧ ¬tr_initial (tr_data tk.tk_trust) ∧
checkTrustProgress hosts_tr[hstid] tk.tk_trust;
if (b) hosts_tr[hstid]← tk.tk_trust;
}
return b;
}
Figure 5: Host Trust Update Operation
op checkTrustUpdate(old : Trust, new : Trust, auth : Authorizations) : bool =
(∗ Check threshold n preserved ∗)
tthr old = tthr new ∧
(∗ Signers are a quorum ∗)
fdom auth \subset tops old ∧
(∗ Signers are a quorum of correct size ∗)
(tthr old) ≤ card (fdom auth) ∧
(∗ Check hash consistency ∗)
tfpr new = hash old ∧
(∗ Check all new members signed ∗)
let newmems = tmems new \ tmems old in
let newops = tops new \ tops old in
(∗ Verify all signatures ∗)
let msg = encode (newmems,newops) in
all (fun o⇒ o ∈ auth ∧ verify (o, msg, oget auth[o])) (fdom auth).
Figure 6: HSM Trust Update Validation
predecessor fingerprint contained in the new trust is the finger-
print of the predecessor trust (so the new trust can also not be an
initial/root trust, and must actually have a fingerprint). Note that,
for each host, we keep track of which trust is installed using a map
hosts_tr.
Finally, Figure 6 shows the behavior of an HSM when checking a
request for a trust update after successful unwrapping of the domain
token containing the old trust. This ensures that an HSM member
of the old trust has signed it. The update request is formalized by
providing the new trust and a set of authorizations, which are just
signatures by operators on the members of the new trust, who are
not in the old trust. The check enforces that the minimum quorum
size (tthr old) is preserved, and that a quorum of at least this size of
operators in the old trust have signed the request. This is computed
by a fold over the list of operators auth that signed the request.
4 REAL-VS-IDEAL SECURITY FOR KMS DMP
In this section we describe and justify the security definition we
adopted for the DMP, corresponding to the AEAD-service layer
as shown in Figure 1. We begin by defining a general syntax for
(possibly distributed) cryptographic keymanagement APIs, inspired
by the work of Shrimpton, Stam andWarinschi [23]. This formalism
abstracts away all the details of the protocol that are not directly
related to key operations, and we believe it to be of independent
interest to analyse the security of other key management APIs.
This allows us to reason about different security models using
simpler definitions, and later refine the results for the concrete
case of the DMP. With this refinement in mind, we clarify how
the introduced abstract notions map to DMP features in various
remarks throughout the text.
type KMS_Oracles = {
proc newOp(badOp : bool) : OpId option ∗ OpSk option
proc requestAuthorization(request : Request, opid : OpId)
: Authorization option
proc newHst() : HstId
proc installInitialTrust(hstid : HstId, tk : Token) : bool
proc installUpdatedTrust(hstid : HstId, tk : Token) : bool
proc newHSM() : HId
proc newToken(hid : HId, new : Trust) : Token option
proc updateTokenTrust(hid : HId, new_trust : Trust, auth : Authorizations,
tk : Token) : Token option
proc addTokenKey(hid : HId, hdl : Handle, tk : Token) : Token option · · · }.
Figure 7: KMS TkManage and TkNewKey Operations
4.1 Key Management APIs
Key management APIs store keys in tokens. In the real world, a
token can be implemented by using trusted hardware (e.g., an HSM
or a SIM card) to store and perform computations with the keys,
in which case keys may never leave the trusted boundaries of the
hardware device. In other settings, for example in the cases where
the underlying hardware cannot store the key material in its inter-
nal state, tokens are implemented as cryptographically hardened
data structures, which guarantee that only trusted devices can (tem-
porarily) access the key material. Our formalization abstracts these
details and applies to both cases.
A token tk is a data structure mapping handles (key identifiers)
to keys key, together with some meta-data that is used by the API
for management operations. The basic operations on tokens are:
• TkManage(tk, cmd): a generic interface that captures all man-
agement operations that can be carried out on tokens, including
creating a new empty token, changing meta-data, and all other
operations that do not affect the keys stored in the token.
14
On
input a token tk and a command description, it returns a (possibly
updated) token.
• TkNewKey(tk, hdl, cmd): samples a new key from the appro-
priate distribution and adds it to the token under the relation
hdl→ key and following the API-specific instructions described
in cmd. The success of this operation may depend on the consis-
tency of the input token itself and on the command cmd, e.g. the
command might violate a check on permissions for generating
keys in a particular token.
15
• TkReveal(tk, hdl, cmd): exposes the key associatedwith hdlwithin
tk, following the API-specific instructions described in cmd. As
before, the success of this operation may depend on the command
details cmd.
The TkReveal operation is a modeling artifact. It is used to make
explicit that any cryptographic API will contain as part of its in-
ternal mechanisms a procedure to recover keys contained within
tokens, so that they can be used to provide cryptographic services.
This serves two purposes: i. to define what correctness of an API
means, and ii. to obtain keys managed by the API in the security
games that define API security—in some cases these keys are simply
given to the adversary in order to model security breaches and, in
other cases, they are used to construct challenges for the adversary.
Relation to the DMP.We show in Figure 7 the EasyCrypt declarations
matching the notions of TkNewKey (addTokenKey) and TkManage (the
14
I.e., these commands may change the state of the API and even the meta-data
associated with keys, but the handle-to-key map will not change.
15
We do not model key deletion operations; including them in the model does not
affect the proof rationale, but it adds complexity to invariants.
Session 1C: Cloud Security I CCS ’19, November 11–15, 2019, London, United Kingdom
69
remaining proc declarations) for the DMP. addTokenKey simply takes
the identity of the HSM that shall carry out the operation of adding
a key to the token.
In token management (TkManage), we include procedures to
create new genuine operators (the model allows both honest and
dishonest ones, in which case the adversary gets the signing key)
and genuine hosts and HSMs. The requestAuthorization procedure models
the actions of honest operators signing attestation requests for
genuine entity identities, in which case this management operation
is really not operating on tokens, but only on the global state of the
API. The body of this procedure just checks that all entities in the
request are indeed genuine and signs the request with the key for
honest operator OpId.
Two procedures model the operations on hosts: installing an
initial trust in host hstid, and updating the installed trust. In the first
case, the body of the procedure ensures that the installed trust is
honest and initial. This captures the global assumption that we
are focusing our analysis on hosts that were initially configured
with honest trusts (there is nothing one can guarantee otherwise).
In the latter case, the procedure executes the operations for hosts
shown in Figure 5. Finally, the newToken and updateTokenTrust procedures
model the actions of HSMs when they are called upon to create
empty tokens, or to update a trust based on authorizations issued
by operators.
Crucially our model enforces that, as in the DMP, the states of
genuine HSMs, operators and hosts are totally disjoint, and that the
only communication between the different entities in the model
must be explicitly performed using calls to this API.
It remains to explain the semantics of the TkReveal operation
within AWS KMS. Recall that the purpose of the operation in the
syntax of key management APIs is to allow defining security exper-
iments that explicitly have access to API-protected keys in order
to express the goal of an adversary (e.g., to formalize that a key
is indistinguishable from random, the experiment needs to have
access to the key in order to construct a real-or-random oracle). In
our model of the DMP, TkReveal is simply the operation that asks
a genuine HSM to unwrap a domain token and return the key for a
particular handle
16
.
Correctness. A natural requirement for key management APIs is
that, subject to an API-specific set of restrictions over calls, they
reliably store secret keys. To define correctness we introduce a pred-
icate valid over traces of calls to TkManage and TkNewKey, which
for a given token-handle-command input (tk, hdl, cmd) indicates
whether a reveal operation should successfully return a key. In the
AWS KMS model, valid simply requires that the command is placed
on a genuine HSM, and the trust of the domain token is installed in
a genuine host. Correctness requires that, if the HSM validates the
domain token and a key with to hdl is stored within, then TkReveal
must successfully recover it.
4.2 Defining Security of Encryption Services
Cryptographic key management APIs such as the DMP are used to
build cryptographic services. In this section we follow the approach
adopted in Universal Composability to formalizing this notion, by
16 TkReveal is of course not an actual operation of the DMP; it is only used as part of
the proof.
Z
77
+gsTLXTzQrMMr4WMtUCk7O6oyaraAdLMW2IVxDC9YaNb+GSS7KDDUJxa0dhEFBUcUNSaFw7g9LiwUXUz7GgUPNM7RRtRxzzi6dk7A0N+5oYkv394uKZ9bOstjdzDhN7Ga2MP/LBiWlt1EldVESarH6KC0Vo5wtdmaJNChIzRxwYaSblYkJN1yQa8Z3HYSbG29D77odOn4MoA7ncAFXEMIN3MEDdKALAhJ4hXdv4r15H6uuat66tDP4I+/zBzjGijg=
73
97la3tnd296n7toH54dNw4qXetzg3jHaalNv2YWi6F4h0UKHk/M5ymseS9eHpX+r1nbqzQ6hFnGY9SOlYiEYyik8JBSnHCqCye5sNG02/5iyGbEKygCatpDxtfg5FmecoVMkmtDQM/w6igBgWTfF4b5JZnlE3pmIcOFU25jYpF5Dm5cMqIJNq4o5As1N8vCppaO0tjd7OMaNe9UvzPC3NMbqJCqCxHrtjyoySXBDUp9ycjYThDOXNAmREuK2ETaihD11LNlRCsr7wJ3atW4PjBhyqcwTlcQgDXcAv30IYOMNDwAm/w7qH36n0s66p4q95O4c94nz9Sd5AT
Order an Essay Now & Get These Features For Free:
Turnitin Report
Formatting
Title Page
Citation
Outline
