-
Decentralized Privacy-Preserving Proximity Tracing
Authors:
Carmela Troncoso,
Mathias Payer,
Jean-Pierre Hubaux,
Marcel Salathé,
James Larus,
Edouard Bugnion,
Wouter Lueks,
Theresa Stadler,
Apostolos Pyrgelis,
Daniele Antonioli,
Ludovic Barman,
Sylvain Chatel,
Kenneth Paterson,
Srdjan Čapkun,
David Basin,
Jan Beutel,
Dennis Jackson,
Marc Roeschlin,
Patrick Leu,
Bart Preneel,
Nigel Smart,
Aysajan Abidin,
Seda Gürses,
Michael Veale,
Cas Cremers
, et al. (9 additional authors not shown)
Abstract:
This document describes and analyzes a system for secure and privacy-preserving proximity tracing at large scale. This system, referred to as DP3T, provides a technological foundation to help slow the spread of SARS-CoV-2 by simplifying and accelerating the process of notifying people who might have been exposed to the virus so that they can take appropriate measures to break its transmission chai…
▽ More
This document describes and analyzes a system for secure and privacy-preserving proximity tracing at large scale. This system, referred to as DP3T, provides a technological foundation to help slow the spread of SARS-CoV-2 by simplifying and accelerating the process of notifying people who might have been exposed to the virus so that they can take appropriate measures to break its transmission chain. The system aims to minimise privacy and security risks for individuals and communities and guarantee the highest level of data protection. The goal of our proximity tracing system is to determine who has been in close physical proximity to a COVID-19 positive person and thus exposed to the virus, without revealing the contact's identity or where the contact occurred. To achieve this goal, users run a smartphone app that continually broadcasts an ephemeral, pseudo-random ID representing the user's phone and also records the pseudo-random IDs observed from smartphones in close proximity. When a patient is diagnosed with COVID-19, she can upload pseudo-random IDs previously broadcast from her phone to a central server. Prior to the upload, all data remains exclusively on the user's phone. Other users' apps can use data from the server to locally estimate whether the device's owner was exposed to the virus through close-range physical proximity to a COVID-19 positive person who has uploaded their data. In case the app detects a high risk, it will inform the user.
△ Less
Submitted 25 May, 2020;
originally announced May 2020.
-
Improving Automated Symbolic Analysis for E-voting Protocols: A Method Based on Sufficient Conditions for Ballot Secrecy
Authors:
Cas Cremers,
Lucca Hirschi
Abstract:
We advance the state-of-the-art in automated symbolic analysis for e-voting protocols by introducing three conditions that together are sufficient to guarantee ballot secrecy. There are two main advantages to using our conditions, compared to existing automated approaches. The first is a substantial expansion of the class of protocols and threat models that can be automatically analysed: we can sy…
▽ More
We advance the state-of-the-art in automated symbolic analysis for e-voting protocols by introducing three conditions that together are sufficient to guarantee ballot secrecy. There are two main advantages to using our conditions, compared to existing automated approaches. The first is a substantial expansion of the class of protocols and threat models that can be automatically analysed: we can systematically deal with (a) honest authorities present in different phases, (b) threat models in which no dishonest voters occur, and (c) protocols whose ballot secrecy depends on fresh data coming from other phases. The second advantage is that it can significantly improve verification efficiency, as the individual conditions are often simpler to verify. E.g., for the LEE protocol, we obtain a speedup of over two orders of magnitude. We show the scope and effectiveness of our approach using ProVerif in several case studies, including FOO, LEE, JCJ, and Belenios. In these case studies, our approach does not yield any false attacks, suggesting that our conditions are tight.
△ Less
Submitted 15 March, 2019; v1 submitted 1 September, 2017;
originally announced September 2017.
-
An Object-Oriented and Fast Lexicon for Semantic Generation
Authors:
Maarten Hijzelendoorn,
Crit Cremers
Abstract:
This paper is about the technical design of a large computational lexicon, its storage, and its access from a Prolog environment. Traditionally, efficient access and storage of data structures is implemented by a relational database management system. In Delilah, a lexicon-based NLP system, efficient access to the lexicon by the semantic generator is vital. We show that our highly detailed HPSG-…
▽ More
This paper is about the technical design of a large computational lexicon, its storage, and its access from a Prolog environment. Traditionally, efficient access and storage of data structures is implemented by a relational database management system. In Delilah, a lexicon-based NLP system, efficient access to the lexicon by the semantic generator is vital. We show that our highly detailed HPSG-style lexical specifications do not fit well in the Relational Model, and that they cannot be efficiently retrieved. We argue that they fit more naturally in the Object-Oriented Model. Although storage of objects is redundant, we claim that efficient access is still possible by applying indexing, and compression techniques from the Relational Model to the Object-Oriented Model. We demonstrate that it is possible to implement object-oriented storage and fast access in ISO Prolog.
△ Less
Submitted 20 May, 2009;
originally announced May 2009.
-
On the Protocol Composition Logic PCL
Authors:
Cas Cremers
Abstract:
A recent development in formal security protocol analysis is the Protocol Composition Logic (PCL). We identify a number of problems with this logic as well as with extensions of the logic, as defined in [DDMP05,HSD+05,He05,Dat05,Der06,DDMR07]. The identified problems imply strong restrictions on the scope of PCL, and imply that some currently claimed PCL proofs cannot be proven within the logic,…
▽ More
A recent development in formal security protocol analysis is the Protocol Composition Logic (PCL). We identify a number of problems with this logic as well as with extensions of the logic, as defined in [DDMP05,HSD+05,He05,Dat05,Der06,DDMR07]. The identified problems imply strong restrictions on the scope of PCL, and imply that some currently claimed PCL proofs cannot be proven within the logic, or make use of unsound axioms. Where possible, we propose solutions for these problems.
△ Less
Submitted 22 February, 2008; v1 submitted 7 September, 2007;
originally announced September 2007.
-
A framework for compositional verification of security protocols
Authors:
Suzana Andova,
Cas Cremers,
Kristian Gjosteen,
Sjouke Mauw,
Stig F. Mjolsnes,
Sasa Radomirovic
Abstract:
Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach.
We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verifi…
▽ More
Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach.
We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation.
To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMax consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.
△ Less
Submitted 1 May, 2007; v1 submitted 14 November, 2006;
originally announced November 2006.
-
Counting Coordination Categorially
Authors:
Crit Cremers,
Maarten Hijzelendoorn
Abstract:
This paper presents a way of reducing the complexity of parsing free coordination. It lives on the Coordinative Count Invariant, a property of derivable sequences in occurrence-sensitive categorial grammar. This invariant can be exploited to cut down deterministically the search space for coordinated sentences to minimal fractions. The invariant is based on inequalities, which is shown to be the…
▽ More
This paper presents a way of reducing the complexity of parsing free coordination. It lives on the Coordinative Count Invariant, a property of derivable sequences in occurrence-sensitive categorial grammar. This invariant can be exploited to cut down deterministically the search space for coordinated sentences to minimal fractions. The invariant is based on inequalities, which is shown to be the best one can get in the presence of coordination without proper parsing. It is implemented in a categorial parser for Dutch. Some results of applying the invariant to the parsing of coordination in this parser are presented.
△ Less
Submitted 7 May, 1996; v1 submitted 6 May, 1996;
originally announced May 1996.
