Last week, numerous researchers published the timely fruits of their recent collaboration to provide a proximity-tracking solution that can help during pandemics while still being privacy-preserving: the result, Decentralized Privacy-Preserving Proximity Tracing (DP-3T), provides a promising first step in bringing real-world cryptography into the effort to combat the COVID-19 pandemic. As mentioned in Troncoso et al.’s whitepaper, the goal of DP-3T is:

"…to simplify and accelerate the process of identifying people who have been in contact with an infected person, thus providing a technological foundation to help slow the spread of the SARS-CoV-2 virus. The system aims to minimise privacy and security risks for individuals and communities and guarantee the highest level of data protection."

Troncoso et al, Decentralized Privacy-Preserving Proximity Tracing

In support of this project, we at Symbolic Software decided to test out Verifpal, our open source protocol verification framework, to see how well its promises of easier and more accessible protocol modeling and verification can hold up in the face of a new and ambitious protocol that targets a novel use case.

In this post, we will go through DP-3T while modeling it using the Verifpal Language, and conclude by comparing our results to the designers’ security goals.

Modeling DP-3T

To demonstrate DP-3T, we will assume that the principals participating in this simulation are the following:

After installing Verifpal, we can start by creating a new model called “dp-3t.vp” in which we begin by defining an attacker which matches with our security model. In this case we will be using an active attacker (i.e. one that can not only monitor but also intercept and overwrite unprotected messages on the network):

1

attacker[active]

We then proceed to illustrate our model as a sequence of days in which DP-3T is in operation within the lifecycle of a pandemic.

Day 0 (setup phase)

We assume that no new individuals were diagnosed with the disease on Day 0 of using DP-3T. This means that the Healthcare Authority and the Backend Server will not act at this stage and we can simply ignore them for now.

The DP-3T specification states that every principal, when first joining the system, should gene_rate a random secret key_ (SK) to be used for one day only. For every SK value, and the knowledge of a public “broadcast key” value, principals should compute multiple Unique Ephemeral ID values (EphID) using a combination of a PRG and a PRF. The method of generating EphID is analogous with the HKDF function from Verifpal. We could add the following lines of code to our file in order to model Alice’s SmartphoneA:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19

// All lines that start with "//" are treated as comments and ignored by Verifpal
// A principal block looks like the following
principal SmartphoneA[
    // In the line below we state that Alice knows the public BroadcastKey
    
    knows public BroadcastKey
    
    // SK is going to be a secret random value
    // To define it we use the "generates" keyword
    // We will use the following template for SK variable names
    // SK[day number][principal initial]
    
    generates SK0A
    
    // We will use the following template for EphID variable names
    // EphID[day number][value number][principal initial]
    
    EphID00A, EphID01A, EphID02A = HKDF(nil, SK0A, BroadcastKey)
]

The same thing goes for Bob, and Charlie:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

principal SmartphoneB[
    knows public BroadcastKey
    generates SK0B
    EphID00B, EphID01B, EphID02B = HKDF(nil, SK0B, BroadcastKey)
]

principal SmartphoneC[
    knows public BroadcastKey
    generates SK0C
    EphID00C, EphID01C, EphID02C = HKDF(nil, SK0C, BroadcastKey)
]

Whenever two principals would come be in physical proximity of each other, they would automatically exchange EphIDs. Once a principal uses an EphID value, they discard it and use another one when performing an exchange with another principal.

Let’s imagine that Alice and Bob came into contact. It would mean that Alice sent EphID00A in a message to Bob and that Bob sent EphID00B to Alice:

Here is how the above message exchange is modeled in Verifpal:

1
2
3
4

// Sender -> Recipient : Name of Value

SmartphoneA -> SmartphoneB: EphID00A
SmartphoneB -> SmartphoneA: EphID00B

Now, let’s say that in the conclusion of Day 0, Bob sits behind Charlie in the Bus:

Modeling this is equally simple:

1
2

SmartphoneC -> SmartphoneB: EphID01C
SmartphoneB -> SmartphoneC: EphID01B

Day 1

On Day 1, the Backend Server will automatically publish the SK values of people who were infected to the members of the general population. These values were previously unpublished and thus were private and only known by their generators and the server.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

// A server is just like any other principal

principal BackendServer[
    // Let's assume that infectedPatients0 is the list of infected patients on day 0
    knows private infectedPatients0
]

BackendServer -> SmartphoneA: infectedPatients0
BackendServer -> SmartphoneB: infectedPatients0
BackendServer -> SmartphoneC: infectedPatients0

We should not forget that every day starting from Day 1, DP-3T mandates that principals will generate new SK values. The new value will be equal to the hash of the SK value from the day before. Principals will also generate EphIDs just like before.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14

principal SmartphoneA[
    SK1A = HASH(SK0A)
    EphID10A, EphID11A, EphID12A = HKDF(nil, SK1A, BroadcastKey)
]

principal SmartphoneB[
    SK1B = HASH(SK0B)
    EphID10B, EphID11B, EphID12B = HKDF(nil, SK1B, BroadcastKey)
]

principal SmartphoneC[
    SK1C = HASH(SK0C)
    EphID10C, EphID11C, EphID12C = HKDF(nil, SK1C, BroadcastKey)
]

Thankfully, Alice, Bob and Charlie are committed to self-confinement and have stayed at home, so they did not exchange EphIDs with anyone.

Day 2

On Day 2, a similar sequence of events takes place. Since it is sufficient to define the values that we will need later on in our model, we will just define a block for Alice.

1
2
3
4

principal SmartphoneA[
    SK2A = HASH(SK1A)
    EphID20A, EphID21A, EphID22A = HKDF(nil, SK2A, BroadcastKey)
]

Fast-Forward to Day 15

Unfortunately, Alice tests positive for COVID-19. Since this breaks the routine that happened between Day 1 and Day 15, we will announce a new phase in our protocol model:

1

phase[1]

Alice decides to announce her infection anonymously using DP-3T. This means that she will have to securely communicate SK1A (her SK value from 14 days ago) to the Backend Server, using a unique trigger token provided by the healthcare authority. Assuming that the Backend Server and the Healthcare Authority share a secure connection, and that a private key encryption key ephemeral_sk has been exchanged off the wire by the Healthcare Authority, Alice, and the Backend Server, the Healthcare Authority will encrypt a freshly generated triggerToken using ephemeral_sk and send it to both Alice and the Backend Server.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

principal HealthCareAuthority[
    generates triggerToken
    knows private ephemeral_sk
    m1 = ENC(ephemeral_sk, triggerToken)
]

// The brackets around m1 here mean that the value is guarded
// ie: an active attacker cannot inject a value in its place

HealthCareAuthority -> BackendServer : [m1]
HealthCareAuthority -> SmartphoneA : m1

Then, Alice would have to use an AEAD cipher to encrypt SK1A using ephemeral_sk as the key and triggerToken as additional data and send the output to the Backend Server. Note that Alice can only obtain triggerToken after decrypting m1 using ephemeral_sk.

1
2
3
4
5
6
7

principal SmartphoneA[
    knows private ephemeral_sk
    m1_dec = DEC(ephemeral_sk, m1)
    m2 = AEAD_ENC(ephemeral_sk, SK1A, m1_dec)
]

SmartphoneA -> BackendServer: m2

The Backend Server will now have to decrypt m1 to receive the triggerToken in the same way that Alice did, then attempt to decrypt m2. If that decryption was successful, the server would obtain SK1A and would be sure that the value came from Alice because it is only Alice who knows both triggerToken and SK1A at the same time as defined in the protocol.

Finally, the Backend Server will add SK1A to the list of infected patients previously defined, and then send this list to all of the individuals in this community.

1
2
3
4
5
6
7
8
9

principal BackendServer [
    knows private ephemeral_sk
    m2_dec = AEAD_DEC(ephemeral_sk, m2, DEC(ephemeral_sk, m1))?
    infectedPatients1 = CONCAT(infectedPatients0, m2_dec)
]

BackendServer -> SmartphoneA: infectedPatients1
BackendServer -> SmartphoneB: infectedPatients1
BackendServer -> SmartphoneC: infectedPatients1

Everything that happened in Day 15 can be summarized in the following diagram:

Queries

Now, we may finally define the queries block, in which we ask Verifpal about the state of certain security guarantees that we expect from the protocol.

SinceSK1A is now shared publicly, the DP-3T software running on anyone’s phone should be able to re-generate all EphID values generated by the owner of SK1A starting from 14 days prior to the day of diagnosis. These values would then be compared them with the list of EphIDs they have received. Everyone who came in contact with Alice will therefore be notified that they have exchanged EphIDs with someone who has been diagnosed with the illness without revealing the identity of that person.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15

queries[
    // Would someone who shared a value 15 days before they got tested get flagged?
    // ie in phase[0], before phase[1]
    confidentiality? EphID02A
    // Will people who came in contact with Alice be able to compute
        // all of Alice's EphIDs starting from Day 1
    confidentiality? EphID10A
    confidentiality? EphID11A
    confidentiality? EphID12A
    confidentiality? EphID20A
    confidentiality? EphID21A
    confidentiality? EphID22A
    // Is the server able to Authenticate Alice as the sender of m2
    authentication? SmartphoneA -> BackendServer: m2
]

The results of our initial modeling in Verifpal suggest to us the following:

These results come in line with what is expected from the protocol. We note that the security of communication channels between Healthcare Authorities, Backend Servers, and Individuals have not been defined, and we have placed our hypothetical own security conditions with in order to focus on quickly sketching the DP-3T protocol. Further analysis will be required in order to better elucidate the extent of the obtained security guarantees.

Generating Models for Further Analysis in ProVerif and Coq

Verifpal generating ProVerif models live from the Verifpal model, through the Verifpal Visual Studio Code extension.

We’re very excited to be working on automatically generating ProVerif and Coq models directly from Verifpal models. The resulting ProVerif and Coq models will be human-readable and thus easily extensible, allowing for more profound protocol analysis and supplementing Verifpal’s insight with that of tools that have existed for more than two decades.

In working on DP-3T, we were able to generate baseline ProVerif and Coq models after less than an hour of work on the Verifpal model itself. This is an immeasurably huge leap forward in terms of obtaining working material for the formal modeling and analysis of a novel protocol, and we are very excited to post further updates as this new feature matures in Verifpal.

ProVerif and Coq model generation is currently under development, and we expect a beta release to be ready by the end of April.

Coming soon!