Automated Security Analysis of Exposure Notification Systems
Authors:
Kevin Morio,
Ilkan Esiyok,
Dennis Jackson,
Robert Künnemann
Abstract:
We present the first formal analysis and comparison of the security of the two most widely deployed exposure notification systems, ROBERT and the Google and Apple Exposure Notification (GAEN) framework. ROBERT is the most popular instalment of the centralised approach to exposure notification, in which the risk score is computed by a central server. GAEN, in contrast, follows the decentralised app…
▽ More
We present the first formal analysis and comparison of the security of the two most widely deployed exposure notification systems, ROBERT and the Google and Apple Exposure Notification (GAEN) framework. ROBERT is the most popular instalment of the centralised approach to exposure notification, 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 first 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 sniffing, database leakage or the compromise of phones, back-end systems and health authorities. We also investigate the security of the original specification of the DP3T protocol, in order to identify gaps between the proposed scheme and its ultimate deployment. We find 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 differentiate all three protocols. Our results suggest that ROBERT's centralised design is more vulnerable against both opportunistic and highly resourced attackers trying to perform mass-notification attacks.
△ Less
Submitted 2 October, 2022;
originally announced October 2022.
Verifying Accountability for Unbounded Sets of Participants
Authors:
Kevin Morio,
Robert Künnemann
Abstract:
Little can be achieved in the design of security protocols without trusting at least some participants. This trust should be justified or, at the very least, subject to examination. One way to strengthen trustworthiness is to hold parties accountable for their actions, as this provides a strong incentive to refrain from malicious behavior. This has led to an increased interest in accountability in…
▽ More
Little can be achieved in the design of security protocols without trusting at least some participants. This trust should be justified or, at the very least, subject to examination. One way to strengthen trustworthiness is to hold parties accountable for their actions, as this provides a strong incentive to refrain from malicious behavior. This has led to an increased interest in accountability in the design of security protocols.
In this work, we combine the accountability definition of Künnemann, Esiyok, and Backes, with the notion of case tests to extend its applicability to protocols with unbounded sets of participants. We propose a general construction of verdict functions and a set of verification conditions that achieve soundness and completeness.
Expressing the verification conditions in terms of trace properties allows us to extend Tamarin -- a protocol verification tool -- with the ability to analyze and verify accountability properties in a highly automated way. In contrast to prior work, our approach is significantly more flexible and applicable to a wider range of protocols.
△ Less
Submitted 20 May, 2021; v1 submitted 22 June, 2020;
originally announced June 2020.
