Automated Security Analysis of Exposure Notification Systems

2025-05-02 0 0 1.76MB 23 页 10玖币

侵权投诉

Automated Security Analysis of Exposure Notiﬁcation Systems

(Full Version)∗

Kevin Morio1Ilkan Esiyok1Dennis Jackson2Robert Künnemann1

1CISPA Helmholtz Center for Information Security

2Mozilla

Abstract

We present the ﬁrst formal analysis and comparison of the

security of the two most widely deployed exposure notiﬁca-

tion systems: the ROBust and privacy-presERving proximity

Tracing protocol (ROBERT) and the Google Apple Exposure

Notiﬁcation (GAEN) framework.

ROBERT is the most popular instalment of the centralised

approach to exposure notiﬁcation, in which the risk score is

computed by a central server. GAEN, in contrast, follows

the decentralised approach, where the user’s phone calculates

the risk. The relative merits of centralised and decentralised

systems have proven to be a controversial question. The

majority of the previous analyses have focused on the privacy

implications of these systems, ours is the ﬁrst formal analysis

to evaluate the security of the deployed systems—the absence

of false risk alerts.

We model the French deployment of ROBERT and the most

widely deployed GAEN variant, Germany’s Corona-Warn-

App. We isolate the precise conditions under which these

systems prevent false alerts. We determine exactly how an

adversary can subvert the system via network and Bluetooth

snifﬁng, database leakage or the compromise of phones, back-

end systems and health authorities. We also investigate the

security of the original speciﬁcation of the DP3T protocol, in

order to identify gaps between the proposed scheme and its

ultimate deployment.

We ﬁnd a total of 27 attack patterns, including many that

distinguish the centralised from the decentralised approach,

as well as attacks on the authorisation procedure that differen-

tiate all three protocols. Our results suggest that ROBERT’s

centralised design is more vulnerable against both opportunis-

tic and highly resourced attackers trying to perform mass-

notiﬁcation attacks.

1 Introduction

In response to the COVID-19 pandemic, digital exposure no-

tiﬁcation systems (ENS) have been designed, deployed and

∗This is an extended version of [25].

are now used by hundreds of millions of people around the

world. These systems complement manual contact tracing

efforts, providing automated notiﬁcation to users that were

potentially exposed to COVID-19 allowing them to take ap-

propriate precautions.

Although various designs have been proposed, the systems

which have seen real world deployment can be split into two

families: centralised [12] or decentralised [31], depending on

whether the risk calculation is performed on a central server or

on the user’s device. The merits of both approaches have been

the subject of extensive debate, with much of the argument

focused on potential privacy risks. Less attention, however,

was paid to the comparative security of the two categories of

systems.

In this work, we formally analyse the security of the two

most widely deployed centralised and decentralised ENS: the

ROBust and privacy-presERving proximity Tracing protocol

(ROBERT), the leading centralised solution, and the Google

Apple Exposure Notiﬁcation framework (GAEN), which fol-

lows a decentralised design. Whilst ROBERT was proposed

and developed as a cohesive whole, the GAEN framework

leaves many security-critical components of the system open

for the developers to implement. The countries that deployed

applications based on the GAEN framework thus had to de-

cide how to authenticate positive test results, how to dissemi-

nate this information to a central back end, and how to inter-

operate with other countries’ back ends. Clearly, these design

decisions critically impact the overall security of the system.

Consequently, we focus on one of the most popular applica-

tions built with the GAEN framework, the Corona-Warn-App

(CWA) developed in Germany, but also investigate the se-

curity of the DP3T system as originally speciﬁed. DP3T’s

speciﬁcation informed the design of GAEN-based applica-

tions deployed in Austria, Belgium, Croatia, Ireland, Italy,

the Netherlands, Portugal and Switzerland.

We carry out our formal analysis with Tamarin [23], a

security protocol veriﬁer. Our models include all the com-

ponents of the deployed ENS including the user phones, a

granular temporal and spatial model and the various back-end

arXiv:2210.00649v1 [cs.CR] 2 Oct 2022

components and associated protocols. Our models allow for

an unbounded number of users engaging in an unbounded

number of sessions and allow the adversary to control user

location and travel patterns, COVID-19 diagnostics and net-

work communication. We further consider an attacker who

can compromise any entity in the system, including users’

phones, health authorities and national back ends. For each

of the models, we ask the following questions:

Under what circumstances can an attacker pollute the

ENS with forged information which will impact the risk

computation?

Under what circumstances can an attacker mislead a user

into believing they are at risk of infection?

By ﬁnding answers to these questions, we develop an ontol-

ogy of possible attacks which systematises the result of much

previous work claiming various attacks or proposing improve-

ments without evidence (discussed in Section 2). The gener-

ality of our threat model allows us to compare the discussed

systems with the required level of detail.

We discover attack patterns that are common across all

systems, but also attacks that distinguish centralised and de-

centralised systems. This is fairly obvious in scenarios with

back end compromise, but we also discover an important dif-

ference in the scalability of an attack when a phone of an

infected user is under the adversary’s control. While isolated

false alarms can severely impact individuals, a large-scale

attack can render the whole system unusable, severely impact-

ing epidemic control efforts.

Independent of the architecture, the authentication schemes

used in the three proposals give vastly different guarantees,

which is largely because interactive schemes are hard to de-

ploy at the necessary scale. We also ﬁnd that federation in-

creases the vulnerability to attacks on other countries’ health

authorities, with a stronger impact on centralised than decen-

tralised systems. In total, we ﬁnd 27 attack patterns across

ROBERT, DP3T and the CWA, providing a detailed answer

of the two previously posed questions.

Contributions

This paper makes the following contribu-

tions: (a) The ﬁrst formal security analysis of the most widely

deployed ENS. (b) A systematic evaluation of the trade-offs

between these systems w.r.t. a powerful shared threat model.

pects of these protocols. They are amenable for automated

analysis and can be reused to model proposed reﬁnements,

extensions and designs.

Outline

In Section 2, we discuss related work on the se-

curity of ENS. We then introduce ROBERT, DP3T and the

CWA in Section 3. The modelling of the systems is discussed

in Section 4and their security properties in Section 5. The

results of our analysis are presented in Section 6, limitations

in Section 7. Finally, we conclude in Section 8.

2 Related Work

A substantial amount of previous work has proposed alter-

native ENS [11,28,29] and presented informal assessments

of their properties [30,18,2,33,9,5,6]. However, only

three [15,22,10] undertook a formal analysis of the security

properties of ENS. In this section, we review these in detail,

postponing a discussion of previously published attacks until

we discuss our taxonomy in Section 6.

Danz et al. [15] investigate the security and privacy of the

Temporary Contact Numbers Protocol and the early DP3T

proposals, as well as the currently deployed GAEN frame-

work. Their analysis is focused on the ‘cryptographic core’ of

each proposal, speciﬁcally the Bluetooth proximity protocol.

Unlike our work, they do not consider the security of the au-

thorisation procedure for uploads and do not model the back

end infrastructure or the spatial distribution of users. How-

ever, as they carry out their analysis by hand in the computa-

tional model, they are able to deﬁne and prove various privacy

properties for the respective Bluetooth proximity protocols.

Kobeissi, Nicolas, and Tiwari [22] build a model of DP3T

in order to demonstrate the ﬂexibility and friendliness of their

new protocol analysis tool. As the model was developed as an

example, it only captures some parts of the protocol, limited

to only three participants interacting in a prescribed pattern

without an authorisation procedure.

Canetti et al. [10] propose two novel ENS and investigate

their security and privacy. They formalise their security no-

tions partly in the UC (universal composability) model and

partly via game based deﬁnitions. Although their UC model

provides a computational proof that the modelled systems

meet their speciﬁed ideal functionality, the concrete implica-

tions of this ideal functionality are not explored and extracting

the resulting security properties is a considerable challenge.

Similar to Danz et al. [15], they model their proposed Blue-

tooth proximity protocols in detail, but leave the rest of their

system, e.g. back end infrastructure and upload authorisation,

abstract.

3 Exposure Notiﬁcation Systems

In this section, we describe the design of ROBERT, GAEN,

DP3T and the CWA.

We ﬁrst introduce ROBERT, the centralised ENS de-

signed by INRIA PRIVATICS and Fraunhofer AISEC [12].

ROBERT was proposed in April 2020 and deployed in the ofﬁ-

cial French contact tracing application ‘StopCovid’ on 2 June

2020 (later rebranded to ‘TousAntiCovid’). With over 12.3

million downloads, it is the most popular centralised ENS.

We then describe the GAEN framework which underlies

many deployed decentralised systems. It is a library inte-

grated with Google’s Android OS and Apple’s iOS to provide

a Bluetooth proximity protocol. Next, we detail DP3T which

predates the GAEN speciﬁcation and is substantially similar

in design, but also describes the various other components of

ENS and guides the design of many European exposure noti-

ﬁcation applications. We also discuss the DP3T proposal for

user upload authentication in detail. Finally, we elaborate on

the design of the CWA, the ofﬁcial German exposure notiﬁca-

tion application, based on DP3T and the GAEN framework.

Terminology

As we refer to the phone more frequently

than to its owner, we will call a phone infected or diagnosed

if its owner has been infected (or diagnosed) with COVID-19.

The contagious period is the time period in which the phone’s

owner is assumed to be contagious. Ephemeral keys that are

associated with this period are called infected keys. If two

phones are close enough that one’s beacon message reaches

the other, they are in proximity.

3.1 ROBERT

In ROBERT, mobile phones continuously broadcast ephem-

eral identiﬁers and store the identiﬁers they receive from other

users. If a user is diagnosed with COVID-19, they upload

all the recorded ephemeral identiﬁers on their phone to a

central back end, which is then able to link these ephemeral

identiﬁers to the users that broadcast them, carry out a risk

calculation and notify any impacted users.

For linking ephemeral identiﬁers to users, phones must ﬁrst

nent identiﬁer, gives them an authorisation key and stores an

encryption key for them. The server then periodically gener-

ates batches of ephemeral Bluetooth identiﬁers (EBIDs) and

transmits them to the phone.

In normal operation (Fig. 1), phones continuously broad-

cast their EBID for the current epoch and record any received

EBIDs transmitted by other phones (1). Should a user test

positive, the health authority provides them with a special au-

thorisation code which they enter into their phone (2). The

phone then transmits this code and all witnessed EBIDs dur-

ing the contagious period to the central server (3). The server

veriﬁes the authorisation code with the help of the health au-

thority (not shown). Knowing each user’s encryption key, the

server can decrypt the EBIDs and learn the permanent iden-

tiﬁers of each user who has been in proximity to the conta-

gious user (4). After performing a risk calculation, the central

server informs the impacted users of the risk (5), but does not

disclose any information about the cause of the risk.

The speciﬁcation explicitly leaves the authorisation proce-

dure for step (2) open, but requires that ‘only authorised and

positive-tested users are allowed to upload’. We thus inves-

tigated the source code of the back-end server, submission

code server and the REST API speciﬁcation

and found that

the submission code server produces long codes for health

Available under

https://gitlab.inria.fr/stopcovid19

Note that we cannot be sure (a) that this code actually runs on the server and

(b) if system parameters like token validity deviate from their defaults.

professionals with a default expiration time of 8 days and

short codes with a default expiration time of 60 minutes. A

positively tested user is given such a code in form of a QR

code, which can be scanned to initiate the upload of EBIDs.

ROBERT also supports a federated deployment, in which

different ROBERT deployments can interoperate with one an-

other. In this case, all servers in the federation are provided

with a federation key which is used to encrypt a country code

for each EBID. When receiving EBIDs from an infectious

user, the back end can always learn the country code of an

EBID and forward the EBID to the relevant server for process-

ing. We provide a more detailed description of registration,

broadcast, authorisation, risk calculation and federation in

Appendix A.

3.2 GAEN

In April 2020, Google and Apple announced a framework for

decentralised ENS (substantially similar to previous propos-

als such as DP3T, PACT

and TCN

) which they deployed

via their respective mobile phone operating systems. This

framework implements the broadcast protocol and risk calcu-

lation, but leaves the other components such as the interaction

with the health authority and between back ends to the de-

velopers of the country-speciﬁc contact tracing applications,

such as the CWA and other DP3T implementations.

In the GAEN framework (Fig. 1), phones do not need to

fresh secret key at the start of each day, called the Temporary

Exposure Key (TEK), which is then used to generate ephem-

eral identiﬁers. Those are broadcast (1) and recorded by other

nearby phones. If a user is diagnosed as infected, they will re-

ceive authorisation from a health authority (2) to upload their

tracing keys to the system’s back end (3). The back end vali-

dates the authorisation token and stores the keys (4). These

can then be downloaded by other users of the system (5), who

can use the information to evaluate whether they have been

near the infected phone and if necessary, notify the user.

Unlike ROBERT, infected phones upload their own keys

instead of payloads received from other phones. Further, the

central server does not process user data and instead acts as a

bulletin board for contagious keys which are distributed to all

users. We provide a more detailed description of broadcast

and risk calculation in Appendix A.

3.3 DP3T

Prior to the release of the GAEN framework, the DP3T ENS

was proposed by a pan-European group of researchers [31]

in March 2020. DP3T uses a Bluetooth protocol very similar

to the GAEN framework, but, in contrast, also proposed a

number of authorisation procedures.

2Privacy Automated Contact Tracing

3Temporary Contact Numbers

Figure 1: An overview of ROBERT (left) and the GAEN framework (right). The colour of the icons on an edge refers to the

entity which originally generated that value.

In the GAEN framework, users who have been diagnosed

with COVID-19 must upload their TEKs to a central server,

which distributes them to all other users to begin the risk

evaluation process. Consequently, the security of this upload

procedure is critical to the overall system, as users could

maliciously upload their TEKs to cause a false alert and

trigger quarantine procedures for users who are not actually

at risk.

In the vast majority of GAEN deployments, the user must

be diagnosed as infected with COVID-19 by a health pro-

fessional. The DP3T consortium proposed three different

authorisation protocols, which detail how the user can authen-

ticate with a health authority and use the resulting credential

to upload their TEKs to the back end. Variants 1 and 2 are

very similar to the ones used by the CWA which we describe

in Section 3.4. We describe Variant 3, designed to have the

strongest security properties, below.

Device Bound Authorisation Codes

The three-party pro-

tocol between the user, health authority and back end is de-

picted in Fig. 2. The user generates a blinded commitment of

their previous TEKs and transmits them (via the Internet or

by displaying a QR code) to the health authority before being

tested. Later, if the test is positive, the health authority pro-

vides the user with an authorisation code (a digital signature).

The user can then transmit this authorisation code to the back

end which checks if the code is both valid and recent. The

user is assumed to share an authentic channel with the health

authority and, separately, with the back end.

This protocol is claimed to ensure that only users who have

tested positive can upload and that the keys they upload cor-

respond to those on the device at testing time. Hence, any

user wishing to upload malicious values (e.g. from another

user) must tamper with their device before being tested. This

is argued to signiﬁcantly raise the cost of any attack on the

system, as an attacker must coerce (persuade, bribe) individu-

als prior to their testing, rather than only targeting those who

test positive.

Federation

In the GAEN framework, each country must

provide its own back end and national infrastructure. This

raises the question of how to handle travellers between coun-

tries, who are typically a high-risk category for COVID-19

exposure. In DP3T, phones inform their ‘home‘ back end

about regions they frequently visit, which then forwards trac-

ing data from these regions’ back ends to the phone.

Phone Healthcare Authority Backend

Gen. and store r

t,H=h(tek,t,r)

Store t,HUndergo test

AC =signskHA (t,H)

tek,t,r,AC

trecent?

verifypkHA ((t,h(tek,t,r)),AC)?

Store t,tek

Figure 2: Authorisation procedure for Variant 3 of DP3T. Let

be the starting epoch number of the

tek

and

a random value.

For each

tek

in the contagious period, an additional

and

AC are exchanged, up to a maximum of 14.

3.4 CWA

The Corona-Warn-App was developed by SAP SE and

Deutsche Telekom and is based on the GAEN framework.

It uses a different authorisation scheme from DP3T. Users

are issued a QR code when they visit a testing facility. They

scan the code with their device, which automatically retrieves

their test result. If the test is positive, they can request a TAN

(transaction authentication number) that can be used once to

upload the TEKs. As this process is vulnerable to human

error, e.g. forgetting to scan the QR code or the medical facil-

ity not providing the code, a telephone authentication option

(teleTAN) is offered as backup. These two authentication pro-

tocols are similar to DP3T variants 1 and 2. They are detailed

further in Appendix C.

European Federation Gateway Service

The European

Federation Gateway Service [24] was developed to provide a

solution across the EU. Each country’s back end connects to

a central database server via mutually authenticated TLS. See

Appendix Cfor more details.

4 Formalisation

In this section, we discuss the scope of our formal models

and the decisions we had to make. We have created models

for ROBERT, DP3T and the CWA (using the GAEN frame-

work) in Tamarin.

In cases where the speciﬁcations lack

important details or are ambiguous, we examined the public

source code of ROBERT and the CWA to inform our deci-

sions. Limitations of our approach are discussed in more

detail in Section 7.

Tamarin

We perform our analysis with Tamarin [23], a

protocol veriﬁcation tool in the Dolev-Yao model. In this

model, messages are described as abstract terms composed

from function symbols that represent cryptographic primitives.

The behaviour of these cryptographic primitives is speciﬁed

by an equational theory on terms.

For example, a hash function is represented by function

symbol

and the empty equational theory, essentially describ-

ing it as a random oracle. Symmetric encryption and decryp-

tion are typically written as the function symbols

senc

sdec

and the equation

sdec(k,senc(k,m)) = m

, which describes

the behaviour of the decryption function. A term is either an

atomic value, a variable or composed from other terms with

a function symbol. Atomic values are either public names,

which are known to the attacker and protocol, or fresh names,

which are drawn uniquely and model keys and nonces.

Protocols are modelled as a combination of multiset rewrite

rules (MSRs) and trace-based ‘restrictions’. MSRs describe

the possible actions in a protocol, such as sending a particular

network message or updating local state.

4The models are available in the Tamarin repository.

Consider the following example:

[ Phone(id,t,k) ] --[ UseKey(id,k) ]-> [ Out(senc(k,t)) ]

Phone(...)

UseKey(...)

and

Out(...)

are facts containing

one or more terms (like

senc(k,t)

). The state is modelled as

a multiset of facts and is rewritten by subsequent application

of MSRs. An MSR can be applied if the facts on the left-

hand side (

Phone(...

)) are part of the state. When the MSR is

applied, these facts are removed and substituted by the facts

on the right-hand side (

Out(...)

). The transition is labelled

with one or more events, also called action facts, in the middle

of the rule (UseKey(...)).

The trace of a system is the sequence of events starting

from an empty state. A set of default rules deﬁnes the adver-

sary behaviour, incorporating the special facts

Out

and

for

protocol output and input.

Security properties and the aforementioned restrictions are

deﬁned in the form of trace properties. These are speciﬁed

in a ﬁrst-order logic with two sorts,

temp

for time points, i.e.

the position within a trace, and

msg

for terms. The atoms of

this ﬁrst-order logic are:

⊥

for false,

t1≈t2

for term equality,

i⋖j

for time point ordering,

for time point equality

and

F@i

, where

is an event and

is a variable of sort

temp

, for the appearance of

at index

. We use

i̸=j

as a

shorthand for

=j=⇒ ⊥

. Restrictions (also speciﬁed via

trace properties) allow for complex conditions to be imposed

on the protocol execution, e.g. checking the validity of a

signature or timestamp. A restriction is assumed to be true,

while a security property is to be veriﬁed.

Scope

Our models cover the entire ENS, from user devices

and their interactions over Bluetooth, to their communication

with the back-end servers and health authorities. There is no

limit to the number of users in the system or the sessions they

engage in. Similarly, there may be multiple back-end systems

in operation, simultaneously and alongside their associated

health authorities. The back-end systems may be in federation

with one another. By lines of code, our models are (individu-

ally) among the largest models compared to Tamarin’s model

repository (see Appendix E).

Temporal Model

Both ROBERT and GAEN divide time

into two different size windows, typically on the order of 24

hours and 10 minutes. We dub the former ‘days’ and the latter

‘epochs’ for clarity. Any particular epoch is said to belong

to a unique day. In GAEN, epochs are aligned with Unix

time (i.e. seconds since 1 January 1970). ROBERT, however,

aligns epochs with the starting time of each country’s back-

end services, which we model faithfully.

The temporal model is critical for our analysis and required

several iterations to achieve the necessary performance. All

three protocols have timestamps that occur in messages, re-

quiring a distinction between timestamps and the time point

they refer to. For example, a particular timestamp (‘Monday’)

can refer to many time points during some period.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

AutomatedSecurityAnalysisofExposureNotificationSystems(FullVersion)∗KevinMorio1IlkanEsiyok1DennisJackson2RobertKünnemann11CISPAHelmholtzCenterforInformationSecurity2MozillaAbstractWepresentthefirstformalanalysisandcomparisonofthesecurityofthetwomostwidelydeployedexposurenotifica-tionsystems:theROBus...

展开>> 收起<<

Automated Security Analysis of Exposure Notification Systems.pdf

共23页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Automated Security Analysis of Exposure Notification Systems

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: