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.
To demonstrate DP-3T, we will assume that the principals participating in this simulation are the following:
- A population of 3 individuals: Alice, Bob, and Charlie, each of them possessing a smartphone:
- A Healthcare Authority serving this population;
- A Backend Server, that individuals can communicate with to obtain daily information.
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):
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 generate 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
// 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:
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:
// 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:
SmartphoneC -> SmartphoneB: EphID01C SmartphoneB -> SmartphoneC: EphID01B
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.
// 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.
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.
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.
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:
Alice decides to announce her infection anonymously using DP-3T. This means that she will have to securely communicate
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
ephemeral_sk and send it to both Alice and the Backend Server.
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
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
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
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.
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:
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.
SK1A 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.
queries[ // Would someone who shared a value 15 days before they got tested get flagged? // ie in phase, before phase 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:
EphIDsgenerated by Alice are known by any parties before Alice announces her illness.
EphID02Aremains confidential even after Alice declaring her illness. Note that it was generated 15 Days before Alice got tested.
- All of the following values
EphID22Ahave been recoverable by an attacker in
phaseafter Alice announces her illness.
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
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.
2 thoughts on “How Verifpal Dramatically Sped Up the Formal Modeling Efforts for a New Pandemic-Tracing Protocol”
Comments are closed.