Christiane Kuhn

Christiane Kuhn, Martin Beck, Thorsten Strufe

The recent SARS-CoV-2 pandemic gave rise to management approaches using mobile apps for contact tracing. The corresponding apps track individuals and their interactions, to facilitate alerting users of potential infections well before they become infectious themselves. Naive implementation obviously jeopardizes the privacy of health conditions, location, activities, and social interaction of its users. A number of protocol designs for colocation tracking have already been developed, most of which claim to function in a privacy preserving manner. However, despite claims such as "GDPR compliance", "anonymity", "pseudonymity" or other forms of "privacy", the authors of these designs usually neglect to precisely define what they (aim to) protect. We make a first step towards formally defining the privacy notions of proximity tracing services, especially with regards to the health, (co-)location, and social interaction of their users. We also give a high-level intuition of which protection the most prominent proposals can and cannot achieve. This initial overview indicates that all proposals include some centralized services, and none protects identity and (co-)locations of infected users perfectly from both other users and the service provider.

Christiane Kuhn, Martin Beck, Thorsten Strufe

After several years of research on onion routing, Camenisch and Lysyanskaya, in an attempt at rigorous analysis, defined an ideal functionality in the universal composability model, together with properties that protocols have to meet to achieve provable security. A whole family of systems based their security proofs on this work. However, analyzing HORNET and Sphinx, two instances from this family, we show that this proof strategy is broken. We discover a previously unknown vulnerability that breaks anonymity completely, and explain a known one. Both should not exist if privacy is proven correctly. In this work, we analyze and fix the proof strategy used for this family of systems. After proving the efficacy of the ideal functionality, we show how the original properties are flawed and suggest improved, effective properties in their place. Finally, we discover another common mistake in the proofs. We demonstrate how to avoid it by showing our improved properties for one protocol, thus partially fixing the family of provably secure onion routing protocols.

Christiane Kuhn, Martin Beck, Stefan Schiffner et al.

Many anonymous communication networks (ACNs) with different privacy goals have been developed. However, there are no accepted formal definitions of privacy and ACNs often define their goals and adversary models ad hoc. However, for the understanding and comparison of different flavors of privacy, a common foundation is needed. In this paper, we introduce an analysis framework for ACNs that captures the notions and assumptions known from different analysis frameworks. Therefore, we formalize privacy goals as notions and identify their building blocks. For any pair of notions we prove whether one is strictly stronger, and, if so, which. Hence, we are able to present a complete hierarchy. Further, we show how to add practical assumptions, e.g. regarding the protocol model or user corruption as options to our notions. This way, we capture the notions and assumptions of, to the best of our knowledge, all existing analytical frameworks for ACNs and are able to revise inconsistencies between them. Thus, our new framework builds a common ground and allows for sharper analysis, since new combinations of assumptions are possible and the relations between the notions are known.