BACHELOR THESIS

C OMPUTING S CIENCE

R ADBOUD U NIVERSITY

The X3DH Protocol: A Proof of Security

Author: First supervisor/assessor:

Ferran van der Have Dr. B.J.M. Mennink
s4104145 b.mennink@cs.ru.nl

Second supervisor:
Prof. Dr. J.J.C. Daemen
j.daemen@cs.ru.nl

Second assessor:
Dr. S. Samardjiska
simonas@cs.ru.nl

January 22, 2022

 Abstract

The X3DH protocols is a key agreement protocol that is used in the Signal protocol
to establish a shared secret key between two parties. While there is a rigorous
security analysis for the Signal protocol, the X3DH protocol does not have the
same level of analysis. In this paper we will provide such an analysis and provide
explanations for most of the theory that is used. We will define the security this
protocol gives and give a proof of security of the X3DH protocol by using game
hops and introducing an adversary with power over the network and proving a
bound on the advantage of the adversary. The conclusion is that the X3DH protocol
provides secrecy of the shared secret and the message.
Contents

1 Introduction 3
1.1 Signal Protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.1.1 Double Ratchet . . . . . . . . . . . . . . . . . . . . . . . 3
1.1.2 Properties . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.2 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.3 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.4 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2 Preliminaries 7
2.1 Mathematical structures . . . . . . . . . . . . . . . . . . . . . . . 7
2.1.1 Groups . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.1.2 Cyclic Groups . . . . . . . . . . . . . . . . . . . . . . . 7
2.1.3 Multiplicative Groups . . . . . . . . . . . . . . . . . . . 8
2.1.4 Fields . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.1.5 Elliptic Curves . . . . . . . . . . . . . . . . . . . . . . . 8
2.2 Key Derivation Functions . . . . . . . . . . . . . . . . . . . . . . 11
2.3 Computational Problems . . . . . . . . . . . . . . . . . . . . . . 11
2.3.1 Discrete Logarithm . . . . . . . . . . . . . . . . . . . . . 11
2.4 Random Oracles . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.5 Distinguishability . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.5.1 Advantages . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.5.2 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.5.3 Security Strength . . . . . . . . . . . . . . . . . . . . . . 14
2.6 Diffie-Hellman . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.6.1 Security . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.6.2 Static and Ephemeral . . . . . . . . . . . . . . . . . . . . 16
2.6.3 Public Key Authentication . . . . . . . . . . . . . . . . . 16
2.6.4 Diffie-Hellman Problems . . . . . . . . . . . . . . . . . . 17
2.7 Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.7.1 Threat Models . . . . . . . . . . . . . . . . . . . . . . . 18
2.7.2 Security Models . . . . . . . . . . . . . . . . . . . . . . 18
2.8 Game Hopping . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.8.1 Large Failure Events . . . . . . . . . . . . . . . . . . . . 19

1
 2.8.2 Small Failure Events . . . . . . . . . . . . . . . . . . . . 19

3 Research 20
3.1 The X3DH Protocol . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.1.1 Trusted Server . . . . . . . . . . . . . . . . . . . . . . . 20
3.1.2 Prekeys . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.1.3 Initiating the Protocol . . . . . . . . . . . . . . . . . . . 22
3.1.4 Deciphering . . . . . . . . . . . . . . . . . . . . . . . . . 24
3.2 Defining the X3DH Protocol . . . . . . . . . . . . . . . . . . . . 24
3.2.1 Threat Model . . . . . . . . . . . . . . . . . . . . . . . . 24
3.2.2 Security Model . . . . . . . . . . . . . . . . . . . . . . . 25
3.2.3 Modelling X3DH . . . . . . . . . . . . . . . . . . . . . . 27
3.2.4 Session Identifier . . . . . . . . . . . . . . . . . . . . . . 28
3.2.5 Predicates . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3.3 Proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.3.1 Scope of the Proof . . . . . . . . . . . . . . . . . . . . . 32
3.3.2 Proof of Security . . . . . . . . . . . . . . . . . . . . . . 33

4 Conclusions 41
4.1 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41

2
Chapter 1

Introduction

Messaging services are very popular and are used globally. However, privacy is be-
coming a bigger topic for the consumers of these services. In return, the providers
of these services use cryptographic protocols to secure the messages and make it
very difficult for adversaries to read these messages. This was not always the case,
as the first messaging services were hardly encrypted at all.
One of the cryptographic protocols that is used nowadays is the Signal protocol.
The Signal protocol is a secure messaging protocol that is included in many known
messaging applications, such as Signal, Skype [27], WhatsApp [37] and Facebook
Messenger [18]. This protocol is used to provide end-to-end encryption of commu-
nication, meaning that it aims to prevent third parties to read the messages while it
is in transit from one party to another.
Initially, there was no proof of security, only a scheme when the protocol was
implemented. Later, Cohn-Gordon et al. [11] were the first to provide a formal
security analysis of the Signal protocol. While the protocol has been out for a
number of years, there has only been a small amount of research done about the
Signal protocol.

1.1 Signal Protocol

Signal consists of two protocols: an initial key agreement protocol Extended Triple
Diffie-Hellman (X3DH) [29] and a double ratcheting algorithm [28].

1.1.1 Double Ratchet

The double ratcheting algorithm is used to encrypt messages based on a shared
secret key, and consists of two stages: asymmetric and symmetric ratcheting. For
every new message, a new key will be derived from the previous keys in such a
way that previous keys cannot be calculated with the help of later keys.
In the asymmetric stage each party generates a secret value using the Diffie-
Hellman protocol which is used to generate the key for the next message. The two

3
parties take turns in generating new secrets and sending them to the other party to
use in deriving the shared secret keys.
In the case that a party wants to send multiple messages at once, the method
used in the asymmetric stage cannot be used. For this case there is the symmetric
stage. In this stage, every message will have a new key derived from the same
secret.
The shared secret key which is used to start the double ratcheting algorithm is
commonly received from the X3DH protocol. The X3DH protocol is used to agree
on a shared secret key between two parties. Like other key agreement protocols,
such as Diffie-Hellman or RSA-KEM, it is done in such a way that other parties
that are listening in on the conversation will not be able to calculate this secret
key. The focus of this paper is the X3DH protocol and this protocol will be further
explained in Section 3.1.

1.1.2 Properties
Signal claims to have the following properties:

• Post-compromise security [12]: If at some point an adversary compromises

a secret and is able to calculate the shared secret key that is used, then future
communication is still secure. However this comes with a condition. If at
some point an adversary compromises a secret key, but the adversary missed
at least one message that was sent after the secret key has been compromised,
then the adversary can no longer read the communication as a new secret has
been introduced of which the adversary has no knowledge.

• Forward secrecy [9]: If at some point an adversary compromises a secret key,

then past communication is still secure as the adversary would be unable to
decode these past messages.

• Resilience (definition is taken from [4]): This means that the output of this
protocol is computationally indistinguishable from random. In the case of
a key exchange protocol, the output of this protocol is a shared secret key
between two parties.

• Plausible deniability [10]: This means that there is no proof that a party has
sent a message to another party, in other words two parties can deny that they
have had communication.

Signal claims that the double ratchet algorithm provides post-compromise security,
forward secrecy and resilience, and X3DH provides forward secrecy and plausible
deniability.

4
1.2 Motivation
In the security analysis of Cohn-Gordon et al. [11], they use the Triple Diffie-
Hellman protocol as key agreement protocol. It is also possible to use X3DH as
key agreement protocol. The difference between the two protocols is that X3DH
has an additional Diffie-Hellman value that is used to calculate the shared secret
key.
In Triple Diffie-Hellman, the responder does not provide an ephemeral key or
one-time prekeys. This makes replaying messages possible [29].
If the initiator sends an initial message without the use of a one-time prekey,
then an adversary can replay this message multiple times. The responder will then
think that the initiator send multiple messages, whereas the initiator only sent one.
While Cohn-Gordon et al. used the Triple Diffie-Hellman protocol as key agree-
ment, they also proved secrecy for the X3DH protocol. The goal of this paper will
be to focus on only on the X3DH protocol and prove the secrecy of this protocol.

1.3 Contributions
The aim of this thesis is to define the security that X3DH provides. It is unclear
what security X3DH actually provides, so defining this makes the protocol itself
better to understand.
Another goal is to provide a clear and accessible proof of secrecy of the X3DH
protocol, while also providing a clear definition of secrecy in this protocol. The
proof is based on the security analysis of Cohn-Gordon et al. [11]. This analysis
is very extensive, but does not fully explain the underlying theory. The goal of the
current project is to first provide all the necessary knowledge that is needed and
then provide the proof of secrecy for the X3DH protocol.
By making this proof more accessible, other cryptographers or researchers that
use the X3DH protocol or research it will know what X3DH is and can verify the
security it provides.

1.4 Related Work

This paper heavily relies on the research done by Cohn-Gordon et al. [11]. They
provide a formal security analysis of the Signal protocol, and in this analysis they
prove the security of the Triple Diffie-Hellman protocol, which is a protocol which
is almost the same as X3DH, but misses one combination of secret values that
X3DH has. They have given a proof for the security in the case that X3DH is used.
Our goal is to provide a similar proof of security for the actual X3DH protocol and
provide all the necessary preliminary knowledge for this proof.
In another work, Kobeissi et al. [23] use CryptoVerif and ProVerif to provide
a framework to automate verification of cryptographic protocols. They used this

5
framework and applied it to a simplified version of the Signal protocol in order to
find weaknesses in this protocol.
Almuzaini et al. [2] provided another formal analysis of the Signal protocol
using a model checking tool called Scyther. Whereas Cohn-Gordon et al. assumed
that the secrets that are used are verified using another channel of communication,
in this research it is not assumed so. Without this assumption Almuzaini et al. did
find an attack on the Signal protocol that exposes a secret key.
Our paper focuses on one-to-one chats using the Signal protocol, however it
is possible to implement group chats, which Rösler et al. [34] focused on. They
analyzed the group chat implementations of Signal and other messaging services
which implement the Signal protocol.
Cremers et al. [13] have researched a clone attack on messaging services that
implement the Signal protocol. A clone attack is an attack that clones the identity
of a party after the full state of a party is compromised. The conclusion of this
research is that many messaging services cannot recover from a clone attack, and
as such will violate the post-compromise security claim.
The specifications of the X3DH protocol by Marlinspike et al. [29] from Signal
is used to define our model of X3DH and explain the X3DH protocol.

6
Chapter 2

Preliminaries

2.1 Mathematical structures

Cryptographic schemes are based on certain mathematical structures. In this sec-
tion we will briefly explain the structures that we will use.

2.1.1 Groups
In this work, a group is a tuple (A, ./), where A is a set and ./ a binary operation,
with the following properties:

• Closed: ∀x, y ∈ A : a ./ b ∈ A,

• Associative: ∀x, y, z ∈ A : (a ./ b) ./ c = a ./ (b ./ c),

• Neutral element: ∃e ∈ A, ∀a ∈ A : a ./ e = e ./ a = a,

• Inverse element: ∀a ∈ A, ∃a0 ∈ A : a ./ a0 = a0 ./ a = e,

• Commutative: ∀a, b ∈ A : a ./ b = b ./ a.

The commutative property is optional, however groups that satisfy this property are
called abelian. A group can be infinite depending on A. The number of elements
in A is called the order of the group. The order of an element a ∈ A, denoted as
ord(a), is the smallest positive integer n such that an = e, or [n]a = e in the case
of addition. Modular addition is a group with the operation + which is denoted as
(Z/nZ, +).

2.1.2 Cyclic Groups

Let (A, +) be a group and g ∈ (A, +). Consider the set {[0]g, [1]g, . . . ord(g)−1}.
This set is a group, denoted as hgi:

• Closed: We can see that ∀i, j ∈ {0 . . . ord(g) − 1} it holds that

[i]g + [j]g = [i + j mod ord(g)]g ∈ hgi.

7
 • Associative: Is trivial, since + is associative.

• Neutral Element: [0]g is the neutral element.

• Inverse Element: We can see that ∀i ∈ {0 . . . ord(g) − 1} the inverse of

[i]g is [ord(g) − i]g.

This group is called a cyclic group and g is called the generator of this group. For
example, in a group (Z/nZ, +), the generator g = 1. Cyclic groups are abelian,
and a cyclic group of order q is isomorphic with (Z/qZ, +). Isomorphic means that
the groups have the same structure and properties. Having an isomorphism means
that there is a mapping function from one group to the other which is a bijection.
A subset H ⊂ G of a group (G, +) is called a subgroup of G, if (H, +) is also
a group.

2.1.3 Multiplicative Groups

To have a group that is based on modular multiplication (Z/nZ, ∗) one has to re-
move some elements from [0, . . . , n − 1], as some elements do not have an inverse.
The neutral element of a multiplicative group is 1. For example, 0 has no inverse.
This means that if we have an element i ∈ (Z/nZ, ∗), i 6= 0 and for some j ∈ N
we have that i ∗ j = n = 0 mod n, then i does not have an inverse either. The
only numbers that have an inverse in (Z/nZ, ∗) are numbers that are coprime to n.
A number x is coprime to n if the greatest common divisor is 1. In the case that n
is a prime, then all elements i ∈ {1 . . . n − 1} are coprime to n, so we only have
to remove 0. We will define such modular multiplication groups with the elements
that violate the group properties removed as (Z/nZ)∗ .

2.1.4 Fields
In this work, a field is a triple (F , +, ∗), where (F , +) is a group and (F \{0 })∗
is a group and distributivity holds. Distributivity means that for all a, b, c ∈ F it
holds that a ∗ (b + c) = a ∗ b + a ∗ c. The field (Z/pZ, +, ∗), where p is a prime,
is called a prime field and is denoted as GF (p). There is a unique prime field for
each prime number.

2.1.5 Elliptic Curves

In public-key cryptography, parties have a public key and a private key. The first is
publicly known and the latter is a secret. Some public-key cryptography is based
on the fact that solving discrete logarithm, explained in Section 2.3.1, is compu-
tationally difficult in certain cyclic groups. When public-key cryptography was
introduced, multiplicative groups based on prime numbers were used.
Another form of public-key cryptography is Elliptic Curve Cryptography (ECC) [14],
which is based on subgroups of elliptic curves. Elliptic curves [22] make it possi-
ble to use smaller keys compared to non-EC cryptography, while still being equally

8
hard to break. Breaking a cryptographic protocol means that an adversary can cal-
culate or deduce the shared secret, without having access to the secret components
that make up this shared secret.
Let GF (q) be a finite field with q elements, where q = pm , p is prime and
p 6= 2, 3. An elliptic curve over GF (q) is the set of pairs (x, y) that satisfies the
following equation, called the Weierstrass equation:

y 2 = x3 + ax + b. (2.1)

Figure 2.1: Addition in elliptic curves: Figure 2.2: Doubling in elliptic curves:
P +Q=R 2P = R

Elliptic Curve Group

We can now define two operations. First we have addition of two points on an
elliptic curve, which results in a third point on the curve. It is best explained by
a geometric example instead of formulas shown in Figure 2.1. We have points P
and Q. To add these points together we draw a straight line through both points.
This line will intersect on a third point on the curve, on point R0 . Now we take the
reflection of R0 on the x-axis to get R. This R is the result of the addition of P and
Q.

9
 The second operation is doubling, which is also better explained by a geometric
example, shown in Figure 2.2. We have a point P which we are going to double.
First we draw the tangent line of the elliptic curve at point P , which intersects at
point R0 . Next we take the reflection of R0 on the x-axis to get R, which is the
result of the doubling of P .
Now we can define an abelian group (E, +) of an elliptic curve defined over a
field, with a neutral element that is a called point at infinity, ∞. This point is the
sum of P and −P (which is the reflection of point P on the x-axis) and is a point
on every vertical line. We must show that the group properties hold:
• Closed: By construction adding two points results in
another point on the curve E .

• Associative: This is not easy to prove. One of the proofs is given by

Friedl [21].

• Neutral Element: ∀P ∈ E it holds that P + ∞ = ∞ + P = P .

• Inverse Element: ∀P ∈ E it holds that P + (−P ) = ∞.

• Commutative: This is trivial. For example, in Figure 2.1 it does

not matter if we draw the line through P first or Q.
An elliptic curve over a field can be defined by so-called domain parameters.
These domain parameters are a sextuple T = (p, a, b, G, n, h), where the elements
are as follows:
• p specifies the finite field GF (p).

• a and b specify the curve E.

• G ∈ E GF (p) , which is a point on the curve over GF (p), is a base point.
This can be any point, but must be agreed upon by both parties.

• n = ord(G).


• h = #E GF (p) /n. This is called the cofactor of the elliptic curve E.
X3DH is implemented with either the Elliptic Curve Diffie-Hellman X25519
or X448 [1]. These curves use the Montgomery form representation of elliptic
curves.
By 2 = x3 + Ax2 + x. (2.2)
Both use a function “X25519” and “X448”, respectively, in order to do scalar
multiplications on the curve. They take as an input a coordinate of a point P and
a scalar n and outputs nP . In order for Alice to generate a public key in X25519,
first she generates a private key a and converts it into a byte string of 32 bytes.
Then her public key is A = aG, where G is the base point, which is the point with
the minimal, positive x value in the case of these functions.

10
 Then her public key is A = X25519(a, 9) where 9 is the x-coordinate of the
base point. Bob does the same with a private key b and computes B. Now both can
compute the shared secret key K = X25519(a, B) = X25519(b, A).

2.2 Key Derivation Functions

In order to get a shared secret key, a Key Derivation Function (KDF) is often used
to derive multiple shared secret keys from a shared secret. A KDF can stretch
shared secrets into longer strings and can create multiple different secret keys from
the same shared secrets with the help of a salt.
This function uses as input a secret value and possibly known parameters. In
this work, a KDF accepts an input of four arguments: a value from keying mate-
rial, a length value `, an optional salt value and an optional context variable. The
last two optional arguments can be set to a constant if they are not needed. The salt
value is a non-secret random value that provides additional randomness to the func-
tion. Adding a salt value makes the KDF stronger, by making it less predictable, as
using a salt makes different uses of the KDF independent of each other, provided
that the KDF is strong enough. With a salt we can even derive two different outputs
from the same secret value input, which is called domain seperation. The context
value can provide information about the context the KDF is used in. For example,
it could contain identities of the user, which algorithm is used or even a timestamp.
The output of a KDF is a string of bits with length ` which can be used in
further protocols as a key. A KDF is a one-way function, meaning that if we know
the output of a KDF, it is infeasible to calculate the input values that were used.
X3DH also makes use of a Key Derivation Function (KDF), namely the HKDF
algorithm [25, 26].

2.3 Computational Problems

Most cryptographic schemes are based on computationally hard problems. These
computationally hard problems cannot be solved efficiently, which means that if a
cryptographic scheme is based on such a problem in a successful way, then break-
ing such a scheme could not be done efficiently either. This is done by design,
because having a cryptographic scheme that takes a long time to break is desirable.

2.3.1 Discrete Logarithm

Let G be a cyclic group with generator g and order q. Then we know that for every
y ∈ G, there is a unique x ∈ (Z/qZ)∗ such that g x = y. This value x is called
the discrete logarithm of y with respect to g: x = logg y. Note that x is unique in
0
(Z/qZ)∗ , which means that if there is a x0 where g x = y, then x0 ≡ x mod q.
The discrete logarithm problem [30] in a cyclic group G with generator g and
order q is as follows: given a randomly chosen y ∈ G, compute logg y. In other

11
words, find x ∈ (Z/qZ)∗ such that g x = y.
In the case of Elliptic Curves [36] it is as follows: consider an elliptic curve E
over a finite field GF (p) with p a prime and P = (x, y) a point of prime order n,
meaning that n is the smallest number such that nP = ∞, on the elliptic curve.
Let k be an integer. Let E be the cyclic group generated by P . Given a point
Q = kP ∈ E, it will be hard to compute k.

2.4 Random Oracles

In order to analyse the security of cryptographic protocols, a random oracle is
often used. Random oracles were introduced and first used in proofs by Bellare
and Rogaway [6]. These oracles are a black box, which means we know nothing of
their inner workings. In the definition of Bellare and Rogaway, the random oracles
produce a bit-string of infinite length: RO : {0, 1}∗ → {0, 1}∞ , of which we
then take the first n bits. In our work however, we focus on random oracles with
fixed-length output: RO : {0, 1}∗ → {0, 1}n .
Interacting with this oracle is done by queries. A party can query a string x to
the random oracle and the oracle will see if x has been queried before. If it has
not been queried before, the oracle will reply with a random string y of length n,
where n ∈ N. If x has been queried before, then the oracle will reply the same
string that was returned when x was queried for the first time.

2.5 Distinguishability
With the help of random oracles we can conduct an experiment to help us prove
the security of protocols. Formally in these experiments, the adversary Eve is an
algorithm A. To measure the capability of the adversary, we use the following
experiment.
Secretly we will select either our cryptographic protocol CP with a secret key
or a random oracle RO. We choose so by generating a random bit b which will
either be 0 or 1. We select CP if b = 1 and select RO if b = 0 . It is up to the
adversary A to find what the value of the bit is.
The experiment is shown in Figure 2.3. Now A will be in one of two worlds:
the “real world” or the “ideal world”. In the real world, A interacts with CP and
A interacts with RO in the ideal world. A does not know in which world it is in,
but can query the entity it is interacting with, noted as “oracle”. When A queries
input X, CP will process the input paired with the secret key which is unknown to
the adversary and provide output Y of length n bits. RO will take input X and see
if it has already received X before. If that is the case, output Y will be the same
as when X was queried before. If X was not queried before, output Y will be a
random bit string of length n. Eventually A returns a bit b0 ∈ {0, 1}. b0 = 1 if A
thinks it is in the real world, and b0 = 0 if it thinks it is in the ideal world.

12
 Secret Key

Figure 2.3: Distinguishability experiment with input X, output Y and adversary

A.

In the case of public key cryptography, we can use a random oracle to prove
the security of our protocol. If we give this random oracle a proper interface so
that it accepts the same values as our protocol and provides similar looking output,
we can query the random oracle for a session key. We can then use the experiment
defined above to get a session key from either the protocol or the oracle and ask an
adversary to tell us in which world he is in. Using this distinguishability experiment
we then prove the security of the “ideal” version where we use the oracle. Then we
will prove our “real” version secure, where we use our protocol, as otherwise we
will have a efficient solution to a computational hard problem.

2.5.1 Advantages
If the adversary would just guess, then he has a success probability of 1/2. So
in order to have a successful attack, he needs to guess b with a probability that is
significantly larger than 1/2.
One can define the advantage of the adversary with this equation:

AdvCP (A) = 2Pr(b = b0 ) − 1. (2.3)

However, in order to better work with the advantage, another formula is derived as
follows. In this derivation we use the logical “and” symbol ∧. This means that in
order for the statement a ∧ b to be true, both a and b must be true. We can derive

13
the following formula:

AdvCP (A) = 2Pr(b = b0 ) − 1

= 2 Pr b0 = 1 ∧ b = 1 + Pr b0 = 0 ∧ b = 0 − 1

Pr(b0 = 1 ∧ b = 1) Pr(b0 = 0 ∧ b = 0)
= + −1
Pr(b = 1) Pr(b = 0) (2.4)
= Pr(b0 = 1|b = 1) + Pr(b0 = 0|b = 0) − 1
= Pr(b0 = 1|b = 1) − 1 − Pr b0 = 0|b = 0

= Pr(b0 = 1|b = 1) − Pr(b0 = 1|b = 0).

This formula is most used in practice in order to calculate the advantage of an

adversary. In case of just guessing, AdvCP = 0. So if there is an attack where
AdvCP is significantly larger than 0, then this would count as a successful attack.

2.5.2 Complexity
The advantage of A of distinguishing between CP and RO increases when A
makes queries to its oracle, called online queries. All these queries are stored in
a query history, noted QHd . To express the advantage we use the total number of
bits sent to and received from the oracle for all queries, |QHd |. This is called the
data complexity.
It is also possible for A to implement CP itself with an arbitrarily chosen secret
key. A does not have to be connected to its oracle for this, so these are called offline
evaluations. These evaluations are stored in another query history, noted QHc . The
advantage in this case depends on the length of the key, so |QHc |. This is called
the computational complexity.
Implementing and running the individual evaluations often involves more com-
putations related to the scheme that is used. However the time these take is often
neglected.

2.5.3 Security Strength

Proving an upper bound for the advantage of an adversary against the protocol is
not possible. We can never know if a protocol is secure, we can only disprove
the security of a protocol by providing an attack. The best we can do is claiming
an upper bound that corresponds to an exhaustive key search. An exhaustive key
search is where an adversary tries all possible keys until the right key is found.
This is by no means efficient, but it will always succeed given enough time.
In the case we have a protocol P with a key length of k the upper bound we
can claim the following:
|QHc |
AdvP (A) ≤ . (2.5)
2k
The adversary that matches this bound, is the adversary that performs an exhaustive
key search.

14
2.6 Diffie-Hellman
In order to understand the Extended Triple Diffie-Hellman protocol, or X3DH,
we need to understand the Diffie-Hellman protocol. Diffie-Hellman [19] is a key-
exchange protocol, created by Whitfield Diffie and Martin Hellman dating back to
1976 [17]. The protocol ensures that two parties can calculate a shared secret, from
their own personal secrets. A third party with no access to these personal secrets is
unable to calculate the shared secret. Traditionally the two parties are named Alice
and Bob and the malicious third party is named Eve.
Diffie-Hellman makes use of public key cryptography in order to create a
shared secret that only Alice and Bob know. In order for Alice to send a mes-
sage to Bob, she calculates the shared secret and uses this as an input for a Key
Derivation Function (KDF). This is a function that creates a secret key based on
the shared secret that can be used for secure communication. KDF is explained in
Section 2.2. Bob can also compute the shared secret and uses the KDF to calculate
the same secret key.
The protocol makes use of either a multiplicative group G of order q and a
generator g or an elliptic curve group of order q and base point g. The protocol
goes as follows:

• Key generation: Alice chooses a number a and calculates A ≡ g a mod q.

Bob chooses a number b and calculates B ≡ g b mod q.

• Alice sends A to Bob.

• Bob sends B to Alice.

• Now both parties can calculate the shared secret K ≡ Ab ≡ g ab ≡ g ba ≡

B a mod q.

The domain parameters of the Diffie-Hellman protocol are (q, g). These parame-
ters define the group that is used in the protocol. The public keys are (A, B ) and
the private keys are (a, b).
We will use the notation DH (A, B ) for the the shared secret of both parties
with the public keys A and B. It is important for each party to know the corre-
sponding private key for one of the public keys.

2.6.1 Security
The Diffie-Hellman protocol is based on the computationally hard Diffie-Hellman
assumption. This means that an attacker needs to solve this computationally hard
problem if it wants to break the protocol. However this is dependent on the choice
of the group and the generator. If the group is too small, solving the computational
problem is not difficult.
In order for Eve to find out what the shared secret is, she has to either compro-
mise one of the private keys, or find a way to calculate the shared secret with only

15
the public keys. For example, in order for Eve to compromise the shared secret key
g ab , she has to either calculate a from g a with a discrete logarithm, or Eve can have
another method to calculate g ab from g a and g b .
This means that breaking the Diffie-Hellman protocol by trying to compute the
shared secret key is not efficient and as such Diffie-Hellman is secure against these
kinds of attacks.

2.6.2 Static and Ephemeral

There are multiple versions of the Diffie-Hellman protocol used in different scenar-
ios. There are two static versions, namely static-static and ephemeral-static [32].
Static means that the private and public key are unchanged by the party for all com-
munications. In the static-static case that means that the key generation is not part
of the protocol, but must be done beforehand. In ephemeral-static, one party has a
static key pair, while the other party creates new key pairs for every time a DH step
is done in the protocol that is used.
There is also a ephemeral-ephemeral version, where each party generates a
new key pair for each DH step done in the protocol. In the ephemeral versions
the key generation is part of the protocol. These ephemeral keys can still be used
for a longer time. For example in TLS [33], the ephemeral keys are used in the
handshake protocol and then the keys that are derived from the handshake are used
for longer sessions.

2.6.3 Public Key Authentication

It is possible, however, for Eve to impersonate Alice, by just sending Bob a public
key and saying she is Alice. Therefore, it is important for Bob to authenticate the
public key that was sent to him. One way of doing this, is by using an out-of-band
authentication. This is a verification method that is on a different communication
channel, for example Bob can physically meet Alice and compare the public key
he received with the public key of Alice herself. This is difficult to do on a large
scale, especially if keys are replaced often or the parties that communicate with
each other live very far away. Meeting thousands of people physically to check the
public keys is very difficult to do, especially in times of the Corona virus.

Signatures
A signature scheme [20] is a way to cryptographically sign a message in such a
way that the receiver can authenticate that the message came from the sender and
that the message is not changed. The use of signatures provide authentication of
the party that is sending the message. It also provides integrity of the message,
meaning that it is visible if the message is altered during transmission. It also
provides non-repudiation of origin, meaning that the sender cannot deny having
sent the message.

16
 The problem with using signatures for authentication is that the public key that
is used has to be authenticated itself before it can be used.
Signature schemes make use of the public and private keys of public key cryp-
tography. If Alice sends a message to Bob, but wants to sign it, she signs the
message with Alice her private key and sends both the signature and the original
message to Bob. Bob can verify the signature using Alice her public key. Only
Alice has access to her private key, so Bob can be almost sure that the message
came from her.

Certificates
Another way of authenticating is by introducing a trusted third party (TTP), for
example a company, also called a Certificate Authority (CA), and certificates. A
certificate is a signature that binds an identity to a public key. For example, Alice
and Bob have generated key pairs (a, A) and (b, B). If Alice is sure that Bob his
public key is B, she can sign a message containing the public key of Bob and Bob
his identity. For example, the message could be “Bob’s public key is B”. Bob can
then use the signature from Alice to show other parties that he is communicating
with that B is indeed his public key. However, for this to work Alice needs to be
trusted by the other parties that Bob is communicating with.
A CA can be such a party that is trusted by every other party. Any party that
wants to use a CA to obtain and verify certificates must obtain the public key of
the CA. This has to be done in a secure way, else it is not possible to authenticate
the public keys of other parties using this CA. This can be done by physical means
and is better to scale compared to the previous method, since every party only has
to visit the CA once and they do not have to physically meet the other parties.
With the help of a CA, two parties Alice and Bob can authenticate the public
keys of each other with the help of the certificates. Since Alice trusts the CA, she
trusts the certificate that says that the public key of Bob is B.
The way the Signal protocol handles certificates is dependent on the implemen-
tation. However, the common way for mobile applications, and as such messaging
services implementing the Signal protocol, is to implement a CA inside the appli-
cation.

2.6.4 Diffie-Hellman Problems

In the case of Diffie-Hellman an attacker wants to calculate the shared secret
K = g ab , where a and b are the private keys of the communicating parties. There
are several variants of computational problems [3] that arise for the attacker. We
will discuss three of these problems.
First there is the Computational Diffie-Hellman Problem (CDH): given a triple
of elements (g, g a , g b ) where a and b are randomly chosen, find K = g ab . This
is based on the discrete logarithm problem. If an adversary could easily solve the
discrete logarithm problem, then the adversary can also solve CDH easily. First the

17
adversary uses the discrete logarithm to calculate a from g a . Then the adversary
can compute (g b )a = g ab . However, there is no proof as of yet that this is the
only way to solve CDH. In some special cases it can be shown that the discrete
logarithm assumption is the same as the CDH assumption [15].
Second there is the Decisional Diffie-Hellman Problem (DDH) [8]: given a
quadruple of elements (g, g a , g b , g c ) where a and b are randomly chosen, decide
whether c ≡ ab mod p. In other words, if we have (g a , g b , x ) it is difficult to
decide if x = g ab or x is a random element in the group generated by g. It is the
case that if CDH is easy to solve, then so is DDH, however the opposite is not true.
There are some groups where solving DDH is easy, but CDH is not. These groups
are called Gap Diffie-Hellman groups.
There is also a computational problem related to these Gap Diffie-Hellman
groups, namely the Gap Diffie-Hellman Problem (GDH) [31]: given a triple of
elements (g, g a , g b ) where a and b are randomly chosen, find K = g ab with help
of a DDH Oracle. Having access to a DDH Oracle means that we can query the
oracle with a quadruple of elements (g, g a , g b , g c ). The oracle will return 1 if
g c = g ab and 0 otherwise. This can be used to verify potential solutions to the
GDH problem and query them to the DDH oracle to see if they are correct. The
proof of security of X3DH makes use of the GDH hardness assumption.

2.7 Models
2.7.1 Threat Models
A threat model is a model which contains the capabilities of the adversary. We
define the capabilities and we will prove in the end that an adversary with these
capabilities cannot break the protocol which you are trying to prove to be secure.
For example, an adversary can be a passive attacker, meaning that the adversary
can only eavesdrop. An adversary can also be an active attacker, meaning that
the adversary can delete, modify, replay messages and has full control over the
network.

2.7.2 Security Models

A security model is a model that can be used to model the protocol you are trying
to prove secure. This contains variables and definitions of the protocol in such a
way that you can prove security of the model.

2.8 Game Hopping

In this proof we will calculate the advantage of the adversary using game hopping.
Game hopping is a technique used in security proofs of protocols [7, 35]. We will
construct a series of games in order to prove the security. Each game differs slightly
from the preceding game. These changes have to be small in order to analyze them

18
better. The advantage that the adversary has in each game is bounded in some
way by the preceding game. The first game will be the original experiment. The
following games will lead to a game for which we can prove a bound. Because
each game is bounded in some way by their preceding games, we can then prove a
bound for the original experiment.

2.8.1 Large Failure Events

Some of the game hops used in the proof are based on large failure events [16]. In
this case we assume that two games will appear identical until a certain error event
occurs, but the probability that this event occurs is very large. We also assume that
this error event and winning the game are independent of each other. We can then
calculate the advantage as follows: Let E be the error event that can occur in Game
1, and Si be the event that you succeed in game i. Let Game 1 and 2 be identical
until E occurs, and if E occurs then the adversary loses. If E does not occur, then
the adversary wins in Game 2 if and only if it would win in Game 1. We can then
see:
Pr(S2 ) = Pr(S1 ∧ ¬E)
(2.6)
= Pr(S1 ) · Pr(¬E).
This can be rewritten as:
1
Pr(S2 ) · = Pr(S1 ). (2.7)
Pr(¬E)

However, this means that by rewriting the formula we must have Pr(¬E) 6= 0. It
is the case that if Pr(¬E) = 0, then we see that Pr(S2 ) = 0 in equation 2.6.
For example, in Game 1 the attacker must calculate the shared secret key with
a public key. In Game 2 the challenger guesses a public key i ∈ {1 . . . q} and the
attacker can only win if that public key is used. Then we can define the event E as
the event that that certain public key is not used. As the probability that ¬E occurs
is 1q , we obtain that:
Pr(S1 ) = Pr(S2 ) · q. (2.8)

2.8.2 Small Failure Events

Other game hops are based on small failure events. As in large failure events, two
games will be identical until a certain error event occurs. However, in this case the
probability that this event occurs is small. In the case of small failure events we
can use the following lemma, provided by Shoup [35]:

Lemma 1. Let A, B, F be events defined in some probability distribution, and

suppose that A ∧ ¬F ⇐⇒ B ∧ ¬F . Then |Pr(A) − Pr(B)| ≤ Pr(F ).

19
Chapter 3

Research

3.1 The X3DH Protocol

Extended Triple Diffie-Hellman or X3DH is a key agreement protocol. This means
that through this protocol two parties can agree on a shared secret key through an
unprotected channel of communication. In order to make the explanations easier
to read, we will give names to the parties that are involved in the protocol. In cryp-
tography it is common to name these parties Alice and Bob. X3DH is designed
for asynchronous messaging. It is possible to use Diffie-Hellman for asynchronous
messaging, however it is not designed specifically for this. Asynchronous mes-
saging makes it possible for Bob to have published some information on a server
and be offline, while Alice can establish a shared secret key and send encrypted
messages using the information on the server. Figure 3.1 provides a visual repre-
sentation of the X3DH protocol.
The server needs to be a trusted server in order to ensure secrecy and a secure
connection. If that is not the case, then the server could provide a key to Alice of
which the server knows the private key. In that case, the server would be able to
read the messages.

3.1.1 Trusted Server

When we speak of trust in cryptography, we assume that the entity that is trusted
will behave according to a set of rules. This set of rules is dependent on the context
in which the entity acts. So in our case a trusted server will distribute the keys in
the way that we expect and will not provide keys so that the server can read the
messages.
If the server is not a trusted server, then the messages that are sent between
Alice and Bob could be read by the server, or the messages can be deleted by the
server.
In order to establish trust between a party and a server, it is possible to use the
Trust On First Use (TOFU) principle. In short, a party connects to a server which
the party does not trust yet and hopes nothing goes wrong. If nothing goes wrong

20
 Step 1)
IKP, SPKP, Certificate, multiple OPKP
Party Server

Step 2) B

Alice Server

IKB, SPKB, Certificate, OPKB

Step 3)

Alice Bob
IKA, EKA, Identifier for OPKB, Ciphertext

Figure 3.1: A visual representation of the X3DH protocol. The steps shown in the
figure do not have to be done at once. In step 1 the parties publish their information
to the server. In step 2 Alice requests Bob his information. In this step Bob can be
offline. In step 3 Alice sends Bob the secrets needed to compute the shared secret.
In this step Bob can also be offline and will receive this message from Alice when
he comes online.

at first, then the server can be trusted. This principle is not the best principle to use,
but it is the easiest one to use.
In this paper we do not assume that the server is trusted. However we do
assume that Alice and Bob have authenticated the public keys of each other, so that
an impersonification of either party by the server would be noticed.

3.1.2 Prekeys
We assume that Alice is the party that initiates the X3DH protocol and wants to
send a message to Bob. In order for Bob to be able to receive a message, he
needs to generate and store some keys on the server. The generation of these keys
is implementation specific, but as specified in the documentation of Signal [29],
they must either all be in X25519 form or in X448 form. These forms have been
discussed in Section 2.1.5. Bob has a private key for every key that is uploaded to
the server. First, Bob needs to generate and store his public identity key IKB to
the server. The private key corresponding to the identity key is ikB and Bob should
keep this key a secret. The identity key is a long-term key that Bob generates when
he connects to the server for the first time. This key is tied to his identity so this
key will not be replaced over time.

21
 The second key that needs to be generated and stored is a medium-term public
key SPKB , called a signed prekey. This is called a signed prekey, because Bob also
needs to store a public key certificate of SPKB using IKB . This signed prekey and
the certificate have to be replaced regularly, by generating a new signed prekey.
The server will be updated to use the new signed prekey. After replacing the key,
Bob keeps the old private key of SPKB for a short time, in order to be able to
decrypt delayed messages. It is important that he deletes the old keys after that
short period of time, in order to provide forward secrecy as these keys are needed
to recalculate the shared secret that is used to decrypt past messages. The amount
of time that the old keys are stored are dependent on the implementation. Since
one-time prekeys are used, replaying older signed prekeys are not harmful, since
they have to be accompanied with a one-time prekey. If Bob notices a one-time
prekeys has been reused, Bob does not accept the message.
These one-time prekeys OPKB are the last keys that have to be uploaded by
Bob. These keys are used a single time, after which the server deletes the key.
When the server notices that the amount of one-time prekeys is getting low, or
whenever Bob wants, he can upload more of these keys to the server. These keys
and SPKB are called ”prekeys” because the keys are uploaded prior to the begin-
ning of the protocol. So in short, the values Bob needs to store are:

• IKB ,

• SPKB ,

• a certificate of SPKB using ikB , the private key corresponding to IKB ,

• multiple OPKB ’s.

The first two keys and the certificate combined with a single OPKB is called a
prekey bundle.

3.1.3 Initiating the Protocol

In order for Alice to initiate the protocol and send a message to Bob, she first has
to request a prekey bundle. Alice needs to verify the certificate before she will
use this bundle. Since she has access to IKB , she can check the contents of the
certificate. If the contents are equal to SPKB , then the certificate is correct. If the
certificate is incorrect, then Alice will not accept the message.
After checking the certificate, Alice creates an ephemeral Diffie-Hellman key
pair with public key EKA . Ephemeral keys are newly generated keys for each
new instance of the protocol and are only used for that instance. Identity keys
and medium-term keys can be used for multiple instances of the protocol, but
ephemeral keys are only used for a single instance. Alice also has her own identity
key IKA of which she has the private key. Alice has access to the following private
keys: ika and eka . Now she can compute the Diffie-Hellman secret keys that are
needed to calculate the shared secret key KAB .

22
 • K1 = DH (IKA , SPKB ),

• K2 = DH (EKA , IKB ),

• K3 = DH (EKA , SPKB ),

• K4 = DH (EKA , OPKB ).

See Figure 3.2 for a visual representation.

Long-term Medium-term Ephemeral

keys keys keys

Keys of Alice IKA EKA

Diffie-Hellman K1 K2 K3 K4
Shared Secrets

Keys of Bob IKB SPKB OPKB

Figure 3.2: The first and last row are public keys that are from Bob and Alice
respectively. The lines from the Diffie-Hellman keys indicate what keys are used
in the calculation.

Using a KDF Alice and Bob can subsequently calculate the shared secret key:
KAB = KDF (K1 ||K2 ||K3 ||K4 , `, salt, context), where || means concatenation
of the keys. Without loss of generality we assume that injective padding is used on
the input. The `, salt and context variables are all dependent on how this protocol
is implemented. After Alice has calculated KAB she deletes her ephemeral key,
ekA , and all the Ki .
Now that Alice has the shared secret key KAB , she can send a message to Bob
so that Bob can calculate KAB as well. Alice will send the following to Bob:

• IKA ,

• EKA ,

23
 • an identifier of which one-time prekey is used,

• an initial ciphertext that is encrypted with KAB .

After the initial message, KAB is used in the ratcheting algorithm to derive the
future keys. Alice can append optional information, such as Bob his username or
certificates. This is however dependent on the implementation.

3.1.4 Deciphering
In order for Bob to decipher the message, he needs to calculate KAB . After receiv-
ing the initial message, Bob knows IKA , EKA and which one-time prekey Alice
used. He also has access to the following private keys: spkB , ikB and opkB . Now
Bob can do the same Diffie-Hellman calculations that Alice did, because the public
keys that are used are either already known by Bob or sent by Alice. It is impor-
tant that Bob also deletes the intermediary Ki values and opkB after calculating
KAB . Now Bob can decrypt the initial ciphertext sent by Alice and checks if it is
correct. It is important that if it is incorrect, for example if the message decrypts
to a random string, Bob stops all communication and deletes all associated values.
If it is correct, both parties can use shared secret key KAB for the rest of their
communication.

3.2 Defining the X3DH Protocol

Before we can consider the proof, we have to understand the context and what
it is exactly we want to prove. We do so by providing a threat model in Section
3.2.1 which analyses possible adversaries and what it is we want to prove. Then
we provide a security model in Section 3.2.2 which we will apply to model the
X3DH protocol. A brief overview of the X3DH protocol can be seen in Figure 3.1.
The models we provide are based on the models Cohn-Gordon et al. [11], however
they analysed the entire Signal protocol, whereas we will only analyse the X3DH
protocol.

3.2.1 Threat Model

We first need to define our threat model. We assume an active adversary Eve that
has control over the network on which the messages will be sent. This means that
Eve can delete messages, but also alter them. Eve can set up a session between two
parties and can choose ephemeral keys. This way, if Eve cannot break the protocol,
then attackers with less control over the network cannot either. We do not consider
the use of side-channel attacks, for example a timing attack [24]. These attacks
are focused not on the protocol itself, but on the devices that run the protocol. Our
threat model is the same model that is used in the proof by Cohn-Gordon et al.

24
 We assume that the KDF function is working as it should and that there is
no other way to calculate the shared secret key than by using the Diffie-Hellman
values.
We do assume that Alice and Bob have both verified the public keys of each
other.
The property we want to prove is secrecy of the shared secret key. Authenti-
cation will be proven alongside secrecy by showing that only the intended parties
could compute the key KAB . Secrecy of the shared secret key will be proven by
showing that the shared key will stay a secret even if some secret values from either
Alice or Bob would be compromised.

3.2.2 Security Model

In our proof we will use a key indistinguishability model [5]. Key indistinguisha-
bility means that it should be very hard for an adversary to distinguish between a
real key and a random string of the same length. In our model we do not consider
the certificate that is used for authentication, as this certificate is used for authenti-
cation and we assume that both parties have verified the public keys. Our security
model is based on the model that is used in the proof by Cohn-Gordon et al. The
difference is that Cohn-Gorden et al. modelled the entirety of the Signal protocol,
whereas we only model the X3DH protocol. As such the definitions are similar to
the ones used in the paper of Cohn-Gordon et al. but are not entirely the same. One
big difference is that we only have to model one stage, where in order to model the
Signal protocol you have to model multiple stages.
There are three stages in the protocol. First the parties upload their prekey
bundles, containing their identity key, signed prekey, a public key certificate of the
signed prekey and multiple one-time prekeys. The second stage is Alice requesting
Bob’s prekey bundle from the server. The third stage is Alice sending the message
to Bob containing the keys needed to calculate a shared secret key.
Now we can define the protocol in terms of algorithms.

Definition 1. A key exchange protocol Π is a combination of algorithms with a set

P containing all possible keys and a value λ which states how many random bits
are required in a session.

In our setting, the protocol consists of two key generation algorithms and two
algorithms to run the protocol:

• IdentityKeyGen(), which outputs the identity key pair (IK , ik ),

• PreKeyGen(ik ), which takes ik as input and outputs the signed prekey pair
(SPK , spk ),

• Initiateephemeral (ik , spk , role, targetid ), where ik and spk are the private
keys of the identity key and the signed prekey, role indicates whether this
party is initiating a conversation or is responding to it. In the case of the

25
 initiating party, there is also an identification of who the targeted responder
is. The ephemeral is the ephemeral private key that is used. With the input
and this ephemeral the algorithm creates the output, which is a state and
possibly a message. The goal of the Initiate algorithm is to define the first
stage of exchanging the prekey bundles.

• Runephemeral (ik , spk , state, message), where ik and spk are the private keys
of the identity key and the signed prekey, state is the state of the proto-
col, and message is an incoming message. This algorithm also uses the
ephemeral private key to create the output. The output is an updated state
and possibly a message. The goal of this algorithm is to create a session
between the two parties and making it possible for both parties to calculate
the shared secret key.

The algorithms are based on the ones used in Cohn-Gordon et al. but the Initiate
and Run algorithm have an extra input ephemeral to show that in this algorithm
an ephemeral key is used.
The state of the protocol that is used in the algorithms is a collection of vari-
ables. In order to access a single variable, an object-oriented approach is taken.
For example, the notation to access variable v in the state π is π.v .

Definition 2. A state π is a collection of variables. Both participants have a state

of the protocol. The collection contains the following variables:

• π.ephemeral ∈ {0, 1}λ , a random string for this stage, based on the security
parameter. Used as the ephemeral key.

• π.key, is the key that is derived from the X3DH protocol.

• π.otherid, the identifier of the other party.

• π.otherik, the identity key of the other party.

• π.otherspk, the prekey of the other party.

• π.role, the role of the participant, it is either initiator or responder.

• π.sessionid, the session identifier. This contains all the public keys to which
the participant has access.

• π.status, the status of the state. It can be either empty, active, accepted or
rejected . accepted or rejected means that it has fully completed the compu-
tations and accepted or rejected the outcome.

We denote πxi as the state of session i of user x. In comparison to the state variables
in Cohn-Gordon et al. we have removed some variables which are not necessary
for our proof.

26
 Combining the four algorithms gives an implementation of the X3DH protocol.
The key generation algorithms create the keys that are needed for the protocol. The
Initiate algorithm initiates the protocol. If the party that runs the Initiate algorithm
has the role of responder, it outputs a prekey bundle. If the party that runs the
Initiate algorithm has the role of initiator, it outputs nothing but receives the prekey
bundle. The Run algorithm handles the rest of the algorithm. If the party that
runs the Run algorithm has the role of initiator, it sends a message containing the
ephemeral key EK to the responder. If the party that runs the Initiate algorithm
has the role of responder, it outputs nothing but receives the message.

3.2.3 Modelling X3DH

Now we have to define the key indistinguishability experiment that is used in the
proof. Before we give a formal definition, we give an informal definition as to
provide a better understanding of the experiment. First the experiment establishes
the identity keys or long-term secret keys before the adversary can interact with the
model. The adversary has a lot of power in the model to try to break the protocol.
It can learn some long-term secrets or even secrets in a single session with the help
of reveal queries. These queries will reply the secret information that is requested,
however, if too much is revealed it is clear the adversary can break the protocol.
So we have to make sure that this will not be the case. This will be discussed in
Section 3.2.5.
It is also possible for the adversary to let two parties start a session with chosen
ephemeral keys. It can also control the delivery of these messages, for example
by changing or dropping the message. If the adversary wants, it can start a test
session, but it can do so only once. In that test session, the adversary is given a key,
which is either the session key that corresponds with this session or a random key.
It is then up to the adversary to decide if the key that it is given is the real key or a
random key and if it guesses correctly it wins the experiment.
Definition 3. Let Π be a key exchange protocol and p, s, e ∈ N as follows:
• p is the number of parties,
• s is the maximum number of sessions,
• e is the maximum number of ephemeral or medium term keys for every party.
Let A be an algorithm. Then we define
 
AdvΠ,p,s,e (A) = 2Pr ExpΠ,p,s,e (A) = 1 − 1 , (3.1)

where the experiment ExpΠ,p,s,e (A) is described in Algorithm 1. It internally calls

the procedures of Algorithms 2, 3, 4, 5, 6 and 7. The algorithms are given in pseu-
docode, which is a non-formal coding language, used to make algorithms readable
and understandable for the reader. We use the constructions for and if and some
other notations:

27
 • x ← y is used to assign a value y to a variable x.
$
• x←
− Y is used to randomly assign a value of Y to a variable x.

These algorithms use additional variables of the state that are defined below:

• π.prekeyid ∈ {1, . . . , e}, which is the index of which prekey is used.

• π.otherprekeyid ∈ {1, . . . , e}, which is the index of which prekey is used

by the other party.

• π.ephemeral ∈ {0, 1}λ , which is the ephemeral private key that is used.

• π.reveal ephemeral, a predicate that says if the reveal query for the ephemeral
key is called.

• π.reveal sessionkey, a predicate that says if the reveal query for the session
key is called.

In comparison to the additional state variables in Cohn-Gordon et al. we have

removed some variables which are not necessary for our proof.

3.2.4 Session Identifier

The state that we have defined is not specified in the Signal protocol itself. In
our definition it holds all public keys involved in a specific session. We use the
session identifier to restrict the adversary. If there is a session S which has the
same identifiers as the test session, then the adversary can query the session key of
S and use that to always succeed in the test session and the experiment. So we will
limit the adversary in such a way that it cannot query a session which has the same
session identifier as the test session.
The algorithms defined below are based on the algorithms from Cohn-Gordon
et al. They have been altered to be used by the X3DH protocol.

28
Algorithm 1 ExpΠ,p,s,e (A)
$
1: b← − {0, 1}
2: tested ← ⊥
3: for x = 1, . . . , p do . Initialize the keys for each user
$
4: (IKx , ikx ) ←
− IdentityKeyGen()
5: for y = 1, . . . , e do . Initialize signed prekeys for all sessions
$
6: (SPKyx , spkyx ) ←
− PreKeyGen(ikx )
7: public ← (IK1 , . . . , IKp , SPK11 , . . . , SPKep )
$
8: b0 ←− ASend,Reveal∗,Test (public) . Test can only be called once
9: if (tested 6= ⊥) ∧ fresh(tested) ∧ b = b0 then . Adversary was successful
10: return 1
11: else . Adversary was not successful
12: return 0

Algorithm 2 Send(x, i, m)
1: if πxi = ⊥ then . There is no session i yet
2: (peerid, y, role) ← m
$
3: πxi .ephemeral ← − {0, 1}λ
4: (πxi , m0 ) ← Initiateπxi .ephemeral (ikx , spkyx , role, peerid )
5: return m0
6: else . There is a session i
7: (πxi , m0 ) ← Runπxi .ephemeral (ikx , spkyx , πxi , m)
8: return m0

Algorithm 3 RevealIdentityKey(x) Algorithm 4 RevealPreKey(x, y)

1: reveal ikx ← true 1: reveal spkyx ← true
2: return ikx 2: return spkyx

Algorithm 5 RevealEphemeral(x, i) Algorithm 6 RevealKey(x, i)

1: πxi .reveal ephemeral ← true 1: πxi .reveal sessionkey ← true
2: return πxi .ephemeral 2: return πxi .key

29
Algorithm 7 Test(x, i)
1: if tested 6= ⊥ or πxi .status 6= accept then . Test can only be called once
2: return ⊥
3: tested ← (x, i)
4: if b = 0 then . Return the real key
5: return πxi .key
6: else . Return a random string that looks like a key
7: return random string

3.2.5 Predicates
With the current experiment it is possible for the adversary to break the protocol,
by just revealing all secrets. We will define some predicates in order to limit this.
If during the experiment, some of the predicates are not true, the adversary fails.
If we now define these predicates in a correct way, we will have an adversary who
cannot break the protocol by just revealing all secrets. For each predicate we will
first provide an informal definition followed by a formal logical definition.
All predicates given in this section are from the paper of Cohn-Gordon et al.
and only have slight modifications to them to only be used in the X3DH protocol.

First we will define the valid(x, i) predicate, where x is the user and i is the
index of a session of that user. A state is valid if it has fully completed the compu-
tations and it has accepted them and the session key is not queried by the adversary
for this session or another session with the same session identifier. This gives us
the following definition:

valid(x, i) = (πxi .status = accept) ∧ ¬πxi .reveal sessionkey

∧ ∀j : πxi .sessionid = ππj i .otherid .sessionid (3.2)
x
j

⇒ ¬ππi .otherid .reveal sessionkey .
x

Now we will define the clean(x, i) predicate. This predicate makes sure that
the adversary does not reveal too many secret keys, so that it can calculate the ses-
sion key. In order to calculate the session key in X3DH, one must calculate four
Diffie-Hellman secret keys. Each of these Diffie-Hellman keys is calculated by a
combination of personal keys of each party. For two parties Alice and Bob these
combinations are shown in Figure 3.2. For each of these combinations, we will de-
fine a cleanXY (x, i) predicate which states that the keys X and Y are not revealed
by the adversary, where X is either the identity key, signed prekey or ephemeral
key of Alice, and Y the same for Bob. We will denote by L the long-term iden-
tity key, M for the medium-term signed prekey and E for the ephemeral key. The
clean(x, i) predicate will be a disjunction of the four cleanXY (x, i) predicates, be-
cause at least one must be true in order for the adversary to not be able to calculate

30
the session key. This gives us the following definition:

clean(x, i) = cleanLM (x, i) ∨ cleanEL (x, i) ∨ cleanEM (x, i) ∨ cleanEE (x, i).
(3.3)
In all the subpredicates we need to make case distinctions on whether x is the
initiator of the protocol or the responder. This is to define which key must not be
revealed by the adversary. Thus, for the cleanLM (x, i) predicate we see that in the
case that x is the initiator, the identity key of x must not be revealed and the signed
prekey of the other party must not be revealed. In the case that x is the responder,
the identity key of the other party must not be revealed and the signed prekey of x
must not be revealed.

¬reveal ik ∧ ¬reveal spkπxi .otherprekeyid πxi .role = initiator
x πxi .otherid
cleanLM (x, i) =
π i .prekeyid
¬reveal ikπxi .otherid ∧ ¬reveal spkxx πxi .role = responder.

(3.4)

Ephemeral Keys
With ephemeral keys we must first address a minor issue. We must be sure that
the other party has generated an ephemeral key. In case of the initiator we must
make sure the ephemeral key is generated by the responder. We do so by checking
whether there exists a session for the responder, which we do by checking if the
ephemeral key is included in the session identifier. We cannot compare the session
identifiers, because the responder may not have responded yet, and as such has
not generated a session identifier. If a session with the responder does not exist,
then the ephemeral key would not be generated, or it could be generated by the
adversary. We must also make sure that this ephemeral key is not revealed by the
adversary in another session with the same session identifier.
In the case of the responder we already know that the initiator has generated
an ephemeral key. However, we must make sure that both parties have the same
session identifier and that the ephemeral key of the initiator is not revealed by the
adversary in another session with the same session identifier.
We will note a ⊂ b as: “a is a substring of b”. We will define a new sub-
predicate cleanEph (x, i) that will address this issue. For better readability we will
define these predicates for the initiator first, and then for the responder.

Initiator

In the case that πxi .role = initiator, cleaninit

Eph (x, i) is defined as follows:

cleaninit i
Eph (x, i) = ∃j : OP Kj ⊂ πx .sessionid

∧ ∀j : OP Kj ⊂ πxi .sessionid ⇒ ¬ππj i .otherid .reveal ephemeral .

x
(3.5)

31
Now we can define the rest of the cleaninit
XY (x, i) predicates for the initiator:

cleaninit i
EL (x, i) = ¬πx .reveal ephemeral ∧ ¬reveal ikπxi .otherid , (3.6)
π i .otherprekeyid
cleaninit i
EM (x, i) = ¬πx .reveal ephemeral ∧ ¬reveal spkπxi .otherid , (3.7)
x

cleaninit i init
EE (x, i) = ¬πx .reveal ephemeral ∧ cleanEph (x, i). (3.8)

Responder
In the case that πxi .role = responder, cleanresp
Eph (x, i) is defined as follows:

cleanresp i j
Eph (x, i) = ∃j : πx .sessionid = ππxi .otherid .sessionid

∧ ∀j : πxi .sessionid = ππj i .otherid .sessionid (3.9)
x

j
⇒ ¬ππi .otherid .reveal ephemeral .
x

Now we can define the rest of the cleanresp

XY (x, i) predicates for the responder:

cleanresp resp
EL (x, i) = cleanEph (x, i) ∧ ¬reveal ikx , (3.10)
i
cleanresp resp πx .prekeyid
EM (x, i) = cleanEph (x, i) ∧ ¬reveal spkx , (3.11)
cleanresp resp i
EE (x, i) = cleanEph (x, i) ∧ ¬πx .reveal ephemeral. (3.12)

Now we can define the fresh(x, i) predicate. This predicate states that a session is
valid and that not too many keys have been revealed by the adversary. So this will
be the the combination of the valid(x, i) and clean(x, i) predicates:

fresh(x, i) = valid(x, i) ∧ clean(x, i). (3.13)

Break Event
We denote the event breaki as the event that the adversary A wins Game i. We
denote Advi as the advantage of A against Game i and is defined as follows:

Advi := |2 · Pr(breaki ) − 1| . (3.14)

3.3 Proof
3.3.1 Scope of the Proof
There are some aspects of the X3DH protocol that we did not model and will
not prove. One of these aspects is the different implementations of the X3DH
protocol used by messaging services. We focus on the protocol as documented by
the developers of X3DH. We also do not make any assumptions on the underlying
primitives that are used, for example what elliptic curve is used.

32
 We do not prove all the security goals that Signal claims X3DH has, such as
plausible deniability, instead, we focus on one-to-one messaging. This means we
do not look at group messaging or other functionalities that can be offered.
As explained in Section 3.2.1 we do not assume side-channel attacks.
There are also some technicalities we have to discuss.
For the Test algorithm we will consider the party that is used in the Test al-
gorithm to be the initiator of the session. We will leave the proof in case of the
responder as analogous.
We assume that the Key Derivation Function that is used is a random oracle, so
we do not have to make any assumptions on the KDF.

3.3.2 Proof of Security

With the help of game hopping we can now provide a proof of security. The goal
is to prove that Adv0 is bounded by the Gap Diffie-Hellman hardness assumption
(See Section 2.6.4). In the X3DH protocol there are four keys that need to be kept
a secret. This means that we have to consider four cases in the proof. These cases
are somewhat similar, so we will give a proof for a specific case and for the other
cases we will discuss briefly the differences and how they impact the outcome.
First we will construct five games that affect all four cases, after which we
will construct four games for each case. An overview of the proof is shown in
Figure 3.3. In the last game for each case the shared secret key will be replaced
by a random value. Then we can calculate a bound on the success probability of
the adversary. We will construct each game towards a reduction to Gap Diffie-
Hellman (GDH). This means that we will replace some Diffie-Hellman keys with
values that we query from a GDH oracle. The games that are used in the proof are
from the proof given by Cohn-Gordon et al. [11]. The games are rewritten to be
used with the X3DH protocol. Game 3 is different than the games that were define
by Cohn-Gordon et al. and is our contribution to the proof.
The entity that the adversary sends his messages to is called the challenger,
which is often denoted as C. This entity ”challenges“ the adversary to break the
system.
Theorem 2. The Extended Triple Diffie-Hellman (X3DH) protocol used in the Sig-
nal protocol is a secure key exchange protocol under the Gap Diffie-Hellman as-
sumption and assuming the Key Derivation Function is a random oracle.
Proof. We start with constructing five games which are used in all four cases.
Next to the variables defined in Section 3.2.3 we will define a new variable, q,
which is the order of the group that we are working in. We will recall the previous
variables that we will use in the proof:
• p is the number of parties,
• s is the maximum number of sessions,
• e is the maximum number of ephemeral or medium term keys for every party.

33
 Case 1 Game 5 Game 6 Game 7 Game 8

Case 2 Similar to Case 1

Game 0 Game 1 Game 2 Game 3 Game 4

Case 3 Similar to Case 1

Case 4 Similar to Case 1

Figure 3.3: An overview of the proof. Most cases are similar to each other, so in
the proof we handle one case and explain the differences in the other cases.

Game Hops for All Cases

Game 0: The initial experiment

This is the experiment we have defined in Section 3.2.3. The advantage of the
adversary A against this game is Adv0 .

Game 1: No Diffie-Hellman collisions

In order to help us in further game hops, we will first make sure that there are no
Diffie-Hellman public keys that are the same. Having two keys that have the same
value is also called a collision. To be able to make sure that there are no collisions,
the challenger C will keep a list containing all the Diffie-Hellman private keys.
This way it is easy to check for C if a value appears twice. If this is the case, the
game is aborted and the adversary loses. Each party has generated a long-term
identity key and a maximum of e ephemeral
keys. This gives us a total of p + e · p
Diffie-Hellman keys and a total of p+e·p 2 pairs of keys. Every single pair of these
keys must not collide. Two keys in the same group with order q will collide with
a probability of 1q . Now we can give the following bound on the advantage of the
adversary:
p+e·p


2
Adv0 ≤ + Adv1 . (3.15)
q

34
Game 2: Guess test session
In this game, the challenger must guess which session will be tested by the adver-
sary with Test(x, i). This means that C must guess both x and i correctly. For x
there are a total of p possibilities, and for i there are s possibilities. That means that
1
the probability that the challenger guesses both of them correctly is xp . This will
∗ ∗
be a game hop with a large failure event. Let C guess (x , i ) ∈ [1 . . . p] × [1 . . . s].
We will define an event E where A will query Test(x, i), where (x, i) 6= (x∗ , i∗ ).
1
We will abort the game when E occurs. The probability that ¬E occurs is p·s .
From this we get the following:

Adv1 ≤ p · s · Adv2 . (3.16)

Game 3: Guess unique partner session

We must also guess the partner session that is tied to the test session. Since in
Game 1 we made sure that all the Diffie-Hellman keys are unique and as such
the combination of identity keys, we know that the partner session is also unique.
This closely follows Game 2, as in Game 2 we guessed a certain session as well.
This is a game hop with a large failure event. So C guesses a pair (x∗ , i∗ ) ∈
[1 . . . p] × [1 . . . s]. We will define an event E where the partner session is πxi
where (x, i) 6= (x∗ , i∗ ). Since the partner session is unique, we know that the
1
probability of ¬E occurring is p·s .
The session identifiers contain the public keys. However, since the adversary
can pick ephemeral keys, it is possible that there is another session that has the same
identifier as the test session that is not this partner session. We will make sure that
if such a session exists, then the challenger knows about it. This is another hop with
a large failure event. We do this by guessing the index j ∈ {1 . . . s} of this session.
We will define an event F where this session is πxj and i 6= j. The probability that
¬F occurs is 1s . Combining both failure events gives us the following bound:

Adv2 ≤ p · s2 · Adv3 . (3.17)

Game Hops for Specific Cases

Now we have to move to a game distinction. We can now write the advantage of A
in Game 3 as follows:
clean (x,i) clean (x,i) clean (x,i) clean (x,i)
Adv3 ≤ Adv3 LM + Adv3 EL + Adv3 EM + Adv3 EE .
| {z } | {z } | {z } | {z }
Case 1 Case 2 Case 3 Case 4
(3.18)
clean (x,i)
Where Adv3 XY is the the advantage of the adversary in the case that cleanXY (x, i)
must stay true.

35
 clean (x,i)
We will define all the game hops for the case Adv3 LM and πxi .role =
i
initiator. As was mentioned before, the case of πx .role = responder is analo-
gous, and only one of the two appears. The cases for the other clean(x, i) pred-
icates will be given later, but since they are very similar, we will only give the
differences.

Case 1: cleanLM (x, i)

In this case we must make sure that the cleanLM (x, i) stays true. This means that A
cannot have issued the queries RevealIdentityKey(x) and RevealPreKey(n, y)
where πxi .otherprekeyid = n.

Game 4: Guessing the prekey of the other party

In this game the challenger has to guess the index of the signed prekey that is used
by the other party that is used in the Test session. C will guess n ∈ {1 . . . e}. This
is a game hop with a large failure event. We will define an event E where n is not
the index of the signed prekey that is used. The probability of ¬E is 1e , which gives
us the following:
Adv3 ≤ e · Adv4 . (3.19)

Game 5: Allowing some duplicate values

To prepare for future game hops, we will allow the identity key of party x, IKx ,
and the signed prekey of party y with index n which we guessed in Game 4, SPKny ,
to be identical. We do this because we want to introduce a GDH challenger. With
this challenger these keys are allowed to be the same. We are working in a group
of order q, so the probability that the keys are the same is 1q . This is a game hop
with a small failure event and gives us the following:
1
Adv4 ≤ + Adv5 . (3.20)
q

Game 6: Introducing GDH

In order to calculate the shared secret key of the X3DH protocol, we need four parts
to be used as input to the KDF. We are in the case cleanLM (x, i), which means that
ikx and spkny remained a secret to the adversary. The shared secret key is calculated
as follows: KAB = KDF (K1 ||K2 ||K3 ||K4 ). Without loss of generality A knows
K2 , K3 and K4 and it wins if it queries KDF (K1 ||K2 ||K3 ||K4 ). So in order for
y
A to win, A must find K1 = g ikx ·spkn for the generator g of the group. We will

36
abort this game when A queries K1 to the KDF oracle it has access to, because
that is the case that the protocol is broken. We will define this event as E . We will
show that if E happens, the adversary will win the game, which we have defined
as Adv(break6 ). So we can split the advantage as follows:

Adv5 ≤ Adv(break6 ) + Adv6 . (3.21)

We will now show that in the case of E , we can create an algorithm A∗ that can
win the GDH problem. As was explained in Section 2.6.4, in the GDH problem
A∗ is given a triple (g, g a , g b ) , and its goal is to find K = g ab with access to a
DDH oracle.
Now A∗ will replace IKx with g a and SPKny with g b , with both a and b un-
known to A∗ . A∗ will then simulate Game 5. Since IKx and SPKny are replaced, it
is not possible to calculate some session keys between certain parties. Since the ad-
versary A can set up sessions between parties, A∗ must simulate these calculations
by giving random keys. These sessions are:

1. A session which is not the Test session that is between parties x and y, where
x is the initiator. Since g a and g b are both used to calculate the session key,
this would require knowledge about a or b.

2. A session which is not the Test session that is between party x and any other
party, including y, where x is the responder. Since g a is used and some other
ephemeral public key on which we have no information, this would require
knowledge about a.

3. A session which can be the Test session that is between any party that is not
x and party y, where y is the responder. Since g b is used and some other
ephemeral public key on which we have no information, this would require
knowledge about b.

A∗ will keep a list which contains, for each session for which a random key is used,
the random key and which public keys should have been used for the calculations.
By keeping this list, A∗ must be consistent in answering queries from A by giving
the right random keys for the right sessions. Before simulating a session and pick-
ing a random key, it is also important that A∗ will use the DDH oracle to check if
a previous random oracle query matches the session, in order to give the right key.
Otherwise, the simulation will not be consistent.
It is also important that A∗ will not answer the reveal queries which will violate
the clean predicate, as this predicate must stay true or the adversary loses.
If A queries the KDF oracle with a query of the form g z1 ||g z2 ||g z3 ||g z4 , then
A∗ must first go through its list and use the DDH oracle to check if the public keys
match the corresponding g zi , for i ∈ {1 . . . 4}. These g zi each match the Ki that
is used to calculate the shared secret key. We refer to Figure 3.2 to see which keys
are needed to calculate which Ki . For each session type that uses random keys we
can then construct DDH oracle queries to give us the information we need.

37
 For sessions of type 1, A∗ has no knowledge about a, b and some other ephemeral
private key e, so in that case A∗ will query the DDH oracle (g, g a , g b , g z1 ) to see
if the first key is correct, and (g, g e , g b , g z3 ) to see if the third key is correct. A∗
knows enough to check the other keys itself.
For sessions of type 2, A∗ has no knowledge about a and e, which is some other
ephemeral private key. In that case we will query the DDH oracle (g, g a , g e , g z2 ),
in order to see if the second key is correct. A∗ knows enough to check the other
keys itself.
For sessions of type 3, A∗ has no knowledge about b and e, which is some other
ephemeral private key. In that case we will query the DDH oracle (g, g b , g e , g z3 ),
in order to see if the third key is correct. A∗ knows enough to check the other keys
itself.
For each case, if the DDH oracle returns 1, meaning that the key is correct, then
∗
A can use the random keys that it generated from the list it keeps. If the oracle
does not return 1, then A∗ must generate a new random value and query that value
to the oracle.
It is important to note that if A∗ queries (g, g a , g b , g z1 ) to the DDH oracle, and
it returns 1, then A has found the solution to the GDH problem, and A∗ will just
return g z1 as the answer to the GDH challenger. In other words, if A breaks Game
6, then A∗ breaks the GDH problem.
So from this we have that if E occurs, then we have a solution to the GDH
problem. This gives us the following:
Adv(break 6 ) ≤ GDH (A∗ ). (3.22)
Where GDH (A∗ ) is the probability of guessing the right answer for the GDH
problem.

Game 7: Replacing the session key

The last game is where the adversary tries to find the session key. However, before
that happens, the experiment will generate a randomly chosen string that is from
the same space that all the keys in this protocol come from. This means that it is
not detectable by the adversary whether the keys have been replaced. We know
from Game 6 that A did not query the KDF oracle with the correct input. The
session key is now replaced with a random other key, depending on the bit b that
was randomly chosen at the start of the experiment. The adversary will have no
advantage anymore, which gives us the following:
Adv6 = Adv7 = 0. (3.23)
Of all these games combined in case 1, we can derive the following:
 
cleanLM (x,i) 1 ∗
Adv3 ≤e + GDH (A ) . (3.24)
q

38
Case 2: cleanEL (x, i)
In this case we make sure that the cleanEL (x, i) predicate stays true. This means
that A cannot have issued the queries RevealEphemeral(x, i) and RevealIdentityKey(y)
in the case that πxi .role = initiator and πxi .otherik = y is the other party of the
session. In the case that πxi .role = responder the queries RevealEphemeral(y, i)
and RevealIdentityKey(x) cannot have been issued.
The differences from the previous games is that we no longer have to guess
the index in Game 4. In Game 5 we allow EKx and IKy to be duplicate, and in
Game 6 we replace these keys with the GDH values g a and g b . From this we get
the following:
clean (x,i) 1
Adv3 EL ≤ + GDH (A∗ ). (3.25)
q

Case 3: cleanEM (x, i)

In this case we make sure that the cleanEM (x, i) predicate stays true. This means
that A cannot have issued the queries RevealEphemeral(x, i) and RevealPreKey(n, y),
where πxi .otherprekeyid = n and πxi .role = initiator. For πxi .role = responder
the queries RevealEphemeral(y, i) and RevealPreKey(πxi .prekeyid, x) cannot
have been issued.
In this case we do have to guess the index again in Game 4. We will allow EKx
and SPKy to be duplicate in Game 5. In Game 6 we will replace these keys with
the GDH values. From this we get the following:
 
cleanEM (x,i) 1 ∗
Adv3 ≤e + GDH (A ) . (3.26)
q

Case 4: cleanEE (x, i)

In this case we make sure that the cleanEE (x, i) predicate stays true. This means
that A cannot have issued the queries RevealEphemeral(x, i) and RevealEphemeral(y, i)
in both the cases that πxi .role = initiator and πxi .role = responder.
In this case we guess the index again in Game 4. However, this time we do not
incur a factor of e but a factor of s. This is because ephemeral keys are generated
on a session basis and not beforehand. In Game 5 we allow the ephemeral keys of
both parties to be the same, and in Game 6 we replace these keys with the GDH
values. From this we get the following:
 
cleanEM (x,i) 1 ∗
Adv3 ≤s + GDH (A ) . (3.27)
q

39
Combining the four cases
We see that all cases are bounded by the GDH problem. Now we can combine all
the cases to get the following bound on Game 3:
   
1 ∗ 1 ∗ 1 ∗
Adv3 ≤ e + GDH (A ) + + GDH (A ) + e + GDH (A )
q q q
  (3.28)
1 ∗
+s + GDH (A ) .
q

From this equation we can derive a bound for Game 0, the original experiment:
  
1 1
p+e·p

e + GDH (A ) + + GDH (A∗ )
∗
q q
Adv0 ≤ 2
+ p2 · s3 ·    
q 1 ∗ 1 ∗
+e + GDH (A ) + s + GDH (A )
q q
p+e·p

 
2 2 3 2e + s + 1 ∗
≤ +p ·s · + (2 · e + s + 1)GDH (A ) .
q q
(3.29)

40
Chapter 4

Conclusions

In this thesis, we have considered X3DH in the Signal protocol, and derived a proof
of security. From the proof it follows that X3DH provides secrecy and authentica-
tion.
We proved this by showing that a powerful adversary with control over the
network cannot calculate the shared secret key to expose the messages that are
being sent. This even holds if the adversary has access to some of the secret values
that are used to calculate the shared secret key. We proved it by showing that the
advantage that an adversary has in breaking the X3DH protocol is bounded by the
Gap Diffie-Hellman hardness assumption.
One could argue that the signatures of prekeys are not necessary, however be-
cause of these signatures, it is not possible for a malicious server to provide forged
prekeys to a party and then reveal the communication between two parties. This
signature shows that these keys were published by one of the parties and not by the
server itself [29].
While doing the literature research on this topic, it appeared that existing re-
search on the X3DH protocol was slim. It has been discussed in various papers as
part of the Signal protocol, but it is not looked at on its own.

4.1 Future Work

As was briefly discussed in Section 3.3.1, there are some parts of the X3DH pro-
tocol we did not include in our proof but are possible starting points for future
research. As this is a protocol which is widely used, new features will continue to
be developed and added to implementations of the protocol. These would deserve
future investigation.
We did not handle out-of-order decryption, which requires users to store secret
values until the message has been delivered. It is not yet clear how much impact
storing these secret values have, but it could reduce the forward secrecy that the
X3DH protocol provides.
While we have proven some security goals of the X3DH protocol, there are

41
some that are still not proven as of yet, for example plausible deniability. While
this may not be as impactful as secrecy, it is still a security goal and as such would
require a proof.
Each implementation of the Signal protocol differs, and as such, different im-
plementations of the X3DH protocol are used. We only proved the security of
X3DH protocol as documented by the developers. Therefore, the proof that is
given might not hold for other implementations of the X3DH protocol.
We assumed in our proof that the public keys were verified before they were
used in the protocol. In the real world, this is not always the case, and with no
verification of the keys on a different channel of communication, it is possible for
an adversary to impersonate other parties. It is difficult to make sure that public
keys are verified, and so far there is no real way to provide this verification by not
using another channel of communication.

42
Bibliography

[1] M. Hamburg A. Langley and S.Turner. Elliptic Curves for Security. Inter-
net Engineering Task Force; RFC 7748 (Informational); IETF, January 2016.
urlhttps://www.ietf.org/rfc/rfc7748.txt.

[2] N. Z. Almuzaini and I. Ahmad. Formal Analysis of the Signal Protocol Us-
ing the Scyther Tool. In 2019 2nd International Conference on Computer
Applications Information Security (ICCAIS), pages 1–6, 2019.

[3] Feng Bao, Robert H Deng, and Huafei Zhu. Variations of Diffie-Hellman
problem. In International conference on information and communications
security, pages 301–312. Springer, 2003.

[4] Boaz Barak and Shai Halevi. A model and architecture for pseudo-random
generation with applications to /dev/random. Cryptology ePrint Archive, Re-
port 2005/029, 2005. https://eprint.iacr.org/2005/029.

[5] Mihir Bellare and Phillip Rogaway. Entity Authentication and Key Distribu-
tion. In Proceedings of the 13th Annual International Cryptology Conference
on Advances in Cryptology, CRYPTO ’93, page 232–249, Berlin, Heidelberg,
1993. Springer-Verlag.

[6] Mihir Bellare and Phillip Rogaway. Random oracles are practical: A
paradigm for designing efficient protocols. In Proceedings of the 1st ACM
conference on Computer and communications security, pages 62–73, 1993.

[7] Mihir Bellare and Phillip Rogaway. Code-Based Game-Playing Proofs

and the Security of Triple Encryption. Cryptology ePrint Archive, Report
2004/331, 2004. https://eprint.iacr.org/2004/331.

[8] Dan Boneh. The decision diffie-hellman problem. In International Algorith-

mic Number Theory Symposium, pages 48–63. Springer, 1998.

[9] Ran Canetti, Shai Halevi, and Jonathan Katz. A forward-secure public-key
encryption scheme. In International Conference on the Theory and Applica-
tions of Cryptographic Techniques, pages 255–271. Springer, 2003.

43
[10] Rein Canetti, Cynthia Dwork, Moni Naor, and Rafail Ostrovsky. Deniable
encryption. In Annual International Cryptology Conference, pages 90–104.
Springer, 1997.
[11] K. Cohn-Gordon, C. Cremers, B. Dowling, L. Garratt, and D. Stebila. A
Formal Security Analysis of the Signal Messaging Protocol. In 2017 IEEE
European Symposium on Security and Privacy (EuroS P), pages 451–466,
2017.
[12] Katriel Cohn-Gordon, Cas Cremers, and Luke Garratt. Post-Compromise
Security. Cryptology ePrint Archive, Report 2016/221, 2016. https://
eprint.iacr.org/2016/221.
[13] Cas Cremers, Jaiden Fairoze, Benjamin Kiesl, and Aurora Naska. Clone De-
tection in Secure Messaging: Improving Post-Compromise Security in Prac-
tice. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and
Communications Security, CCS ’20, page 1481–1495, New York, NY, USA,
2020. Association for Computing Machinery.
[14] K. Igoe D. McGrew and M. Salter. Fundamental Elliptic Curve Cryptography
Algorithms. Internet Engineering Task Force; RFC 6090 (Informational);
IETF, February 2011. urlhttps://www.ietf.org/rfc/rfc6090.txt.
[15] Bert Den Boer. Diffie-Hellman is as strong as discrete log for certain primes.
In Conference on the Theory and Application of Cryptography, pages 530–
539. Springer, 1988.
[16] Alexander W. Dent. A Note On Game-Hopping Proofs. Cryptology ePrint
Archive, Report 2006/260, 2006. https://eprint.iacr.org/2006/
260.
[17] Whitfield Diffie and Martin Hellman. New directions in cryptography. IEEE
transactions on Information Theory, 22(6):644–654, 1976.
[18] Facebook. Messenger Secret Conversations Technical Whitepaper, July
2016. https://fbnewsroomus.files.wordpress.com/2016/
07/secret_conversations_whitepaper-1.pdf.
[19] A. Behrouz. Forouzan. Data communications & networking Fourth Edition,
pages 952–956. McGraw-Hill Education, fourth edition, 2006.
[20] A. Behrouz. Forouzan. Data communications & networking Fourth Edition,
pages 971–976. McGraw-Hill Education, fourth edition, 2006.
[21] Stefan Friedl. An elementary proof of the group law for elliptic curves.
Groups Complexity Cryptology, 9(2):117–123, 2017.
[22] Darrel Hankerson, Alfred J Menezes, and Scott Vanstone. Guide to elliptic
curve cryptography. Springer Science & Business Media, 2006.

44
[23] N. Kobeissi, K. Bhargavan, and B. Blanchet. Automated Verification for
Secure Messaging Protocols and Their Implementations: A Symbolic and
Computational Approach. In 2017 IEEE European Symposium on Security
and Privacy (EuroS P), pages 435–450, 2017.

[24] Paul C. Kocher. Timing attacks on implementations of diffie-hellman, rsa,

dss, and other systems. In Neal Koblitz, editor, Advances in Cryptology —
CRYPTO ’96, pages 104–113, Berlin, Heidelberg, 1996. Springer Berlin Hei-
delberg.

[25] H. Krawczyk and P. Eronen. HMAC-based Extract-and-Expand Key Deriva-

tion Function (HKDF). Internet Engineering Task Force; RFC 5869 (Infor-
mational); IETF, May 2010. urlhttps://www.ietf.org/rfc/rfc5869.txt.

[26] Hugo Krawczyk. Cryptographic Extraction and Key Derivation: The HKDF
Scheme. Cryptology ePrint Archive, Report 2010/264, 2010. https://
eprint.iacr.org/2010/264.

[27] Joshua Lund. Signal partners with Microsoft to bring end-to-end encryption
to Skype. https://signal.org/blog/skype-partnership/.

[28] Moxie Marlinspike and Trevor Perrin (editor). The Double Ratchet
Algorithm, November 2016. https://signal.org/docs/
specifications/doubleratchet/.

[29] Moxie Marlinspike and Trevor Perrin (editor). The X3DH Key Agree-
ment Protocol, November 2016. https://signal.org/docs/
specifications/x3dh/.

[30] Kevin S McCurley. The discrete logarithm problem. In Proc. of Symp. in

Applied Math, volume 42, pages 49–74. USA, 1990.

[31] Tatsuaki Okamoto and David Pointcheval. The gap-problems: A new class
of problems for the security of cryptographic schemes. In Kwangjo Kim,
editor, Public Key Cryptography, pages 104–118, Berlin, Heidelberg, 2001.
Springer Berlin Heidelberg.

[32] E. Rescorla. Diffie-Hellman Key Agreement Method. Network Working

Group; RFC 2631; IETF, June 1999. urlhttps://www.ietf.org/rfc/rfc2631.txt.

[33] E. Rescorla. The Transport Layer Security (TLS) Protocol Version 1.3.
Internet Engineering Task Force; RFC 8446; IETF, August 2018. url-
https://www.ietf.org/rfc/rfc8446.txt.

[34] P. Rösler, C. Mainka, and J. Schwenk. More is Less: On the End-to-End

Security of Group Chats in Signal, WhatsApp, and Threema. In 2018 IEEE
European Symposium on Security and Privacy (EuroS P), pages 415–429,
2018.

45
[35] Victor Shoup. Sequences of games: a tool for taming complexity in security
proofs. Cryptology ePrint Archive, Report 2004/332, 2004. https://
eprint.iacr.org/2004/332.

[36] Joseph H Silverman and Joe Suzuki. Elliptic curve discrete logarithms and the
index calculus. In International Conference on the Theory and Application
of Cryptology and Information Security, pages 110–125. Springer, 1998.

[37] WhatsApp. WhatsApp Encryption Overview Technical White Pa-

per, December 2017. https://www.whatsapp.com/security/
WhatsApp-Security-Whitepaper.pdf.

46