Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Constant Ciphertext-Rate Non-committing Encryption from Standard Assumptions
Non-committing encryption (NCE) is a type of public key encryption which comes with the ability to equivocate ciphertexts to encryptions of arbitrary messages, i.e., it allows one to find coins for key generation and encryption which “explain” a given ciphertext as an encryption of any message. NCE is the cornerstone to construct adaptively secure multiparty computation [Canetti et al. STOC’96] and can be seen as the quintessential notion of security for public key encryption to realize ideal communication channels.
A large body of literature investigates what is the best message-to-ciphertext ratio (i.e., the rate) that one can hope to achieve for NCE. In this work we propose a near complete resolution to this question and we show how to construct NCE with constant rate in the plain model from a variety of assumptions, such as the hardness of the learning with errors (LWE), the decisional Diffie-Hellman (DDH), or the quadratic residuosity (QR) problem. Prior to our work, constructing NCE with constant rate required a trusted setup and indistinguishability obfuscation [Canetti et al. ASIACRYPT’17]
Normalizing Flows with Multi-scale Autoregressive Priors
Flow-based generative models are an important class of exact inference models that admit efficient inference and sampling for image synthesis.
Owing to the efficiency constraints on the design of the flow layers, \eg~split coupling flow layers in which approximately half the pixels do not undergo further transformations, they have limited expressiveness for modeling long-range data dependencies compared to autoregressive models that rely on conditional pixel-wise generation.
In this work, we improve the representational power of flow-based models by introducing channel-wise dependencies in their latent space through multi-scale autoregressive priors (mAR).
Our mAR prior for models with split coupling flow layers (mAR-SCF) can better capture dependencies in complex multimodal data.
The resulting model achieves state-of-the-art density estimation results on MNIST, CIFAR-10, and ImageNet.
Furthermore, we show that mAR-SCF allows for improved image generation quality, with improvements in FID and Inception scores compared to state-of-the-art flow-based models
When does my Program do this? Learning Circumstances of Software Behavior
We introduce Alhazen—an approach that automatically determines the circumstances under which a particular program behavior, such as a failure, takes place. Alhazen starts with a run that exhibits this behavior and automatically determines _input features_ associated with the behavior in question:
(1) We use a _grammar_ to parse the input into individual elements.
(2) We determine _features_ from the elements such as existence, length, or numerical values.
(3) We use a decision tree learner to _observe_ and _learn_ which input features are associated with the behavior in question.
(4) We use the grammar to _generate additional inputs_ to further strengthen or refute hypotheses as learned associations.
(5) By repeating steps 2 to 4, we obtain a _theory_ that explains and predicts the given behavior.
In our evaluation using inputs for find, grep, NetHack, and a JavaScript transpiler, the theories produced by Alhazen predict and produce failures with high accuracy and allow developers to focus on a small set of input features: “grep fails whenever the --fixed-strings option is used in conjunction with an empty search string.
Is FIDO2 the Kingslayer of User Authentication? A Comparative Usability Study of FIDO2 Passwordless Authentication
The newest contender for succeeding passwords as the incumbent web authentication scheme is the FIDO2 standard. Jointly developed and backed by the FIDO Alliance and the W3C, FIDO2 has found support in virtually every browser, finds increasing support by service providers, and has adoptions beyond browser-software on its way. While it supports MFA and 2FA, its single-factor, passwordless authentication with security tokens has received the bulk of attention and was hailed by its supporters and the media as the solution that will replace text-passwords on the web. Despite its obvious security and deployability benefits—a setting that no prior solution had in this strong combination—the paradigm shift from a familiar knowledge factor to purely a possession factor raises questions about the acceptance of passwordless authentication by end-users.
This paper presents the first large-scale lab study of FIDO2 single-factor authentication to collect insights about end-users' perception, acceptance, and concerns about passwordless authentication. Through hands-on tasks our participants gather first-hand experience with passwordless authentication using a security key, which they afterwards reflect on in a survey. Our results show that users are willing to accept a direct replacement of text-based passwords with a security key for single-factor authentication. That is an encouraging result in the quest to replace passwords. But, our results also identify new concerns that can potentially hinder the widespread adoption of FIDO2 passwordless authentication. In order to mitigate these factors, we derive concrete recommendations to try to help in the ongoing proliferation of passwordless authentication on the web
A Formal Security Analysis of Key Establishment in the Signal Messaging Protocol
The Signal protocol is a cryptographic messaging protocol that provides end-to-end encryption for instant messaging in WhatsApp, Wire, and Facebook Messenger among many others, serving well over 1 billion active users. Signal includes several uncommon security properties (such as “future secrecy” or “post-compromise security”), enabled by a technique called ratcheting in which session keys are updated with every message sent.
We conduct a formal security analysis of Signal’s initial extended triple Diffie-Hellman (X3DH) key agreement and Double Ratchet protocols as a multi-stage authenticated key exchange protocol. We extract from the implementation a formal description of the abstract protocol, and define a security model which can capture the “ratcheting” key update structure as a multi-stage model where there can be a “tree” of stages, rather than just a sequence. We then prove the security of Signal’s key exchange core in our model, demonstrating several standard security properties. We have found no major flaws in the design, and hope that our presentation and results can serve as a foundation for other analyses of this widely adopted protocol
Decentralized Privacy-Preserving Proximity Tracing
This document describes and analyzes a system for secure and privacy-preserving proximity tracing at large scale.This system 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.
The system provides the following security and privacy protections:
•Ensures data minimization. The central server only observes anonymous identifiers of COVID-19 positive users without any proximity information. Health authorities learn no information except that provided when a user reaches out to them after being notified.
•Prevents abuse of data. As the central server receives the minimum amount of information tailored to its requirements, it can neither misuse the collected data for other purposes, nor can it be coerced or subpoenaed to make other data available.
•Prevents tracking of users. No entity can track users that have not reported a positive diagnosis.Depending on the implementation chosen, others can only track COVID-19 positive users in a small geographical region limited by their capability to deploy infrastructure that can receive broadcasted Bluetooth beacons.
•Graceful dismantling. The system will dismantle itself after the end of the epidemic. COVID-19 positive users will stop uploading their data to the central server, and people will stop using the app. Data on the server and in the apps is removed after 14 days.
We are publishing this document to inform the discussion revolving around the design and implementation of proximity tracing systems. This document is accompanied by other documents containing an overview of the data protection compliance of the design, an extensive privacy and security risk evaluation of digital proximity tracing systems, a proposal for interoperability of multiple systems deployed in different geographical regions,and alternatives for developing secure upload authorisation mechanisms
Spatio-Temporal Model-Checking of Cyber-Physical Systems Using Graph Queries
We explore the application of graph database technology to
spatio-temporal model checking of cooperating cyber-physical systems-of-systems such as vehicle platoons. We present a translation of spatio-temporal automata (STA) and the spatio-temporal logic STAL to semantically equivalent property graphs and graph queries respectively. We prove a sound reduction of the spatio-temporal verification problem to graph database query solving. The practicability and efficiency of this approach is evaluated by introducing NeoMC, a prototype implementation of our explicit model checking approach based on Neo4j. To evaluate NeoMC we consider case studies of verifying vehicle platooning models. Our evaluation demonstrates the effectiveness of our approach in terms
of execution time and counterexample detection
Certified Lattice Reduction
Quadratic form reduction and lattice reduction are fundamental tools in computational number theory and in computer science, especially in cryptography. The celebrated Lenstra–Lenstra–Lovász reduction algorithm (so-called lll) has been improved in many ways through the past decades and remains one of the central methods used for reducing integral lattice basis. In particular, its floating-point variants—where the rational arithmetic required by Gram–Schmidt orthogonalization is replaced by floating-point arithmetic— are now the fastest known. However, the systematic study of the reduction theory of real quadratic forms or, more generally, of real lattices is not widely represented in the literature. When the problem arises, the lattice is usually replaced by an integral approximation of (a multiple of) the original lattice, which is then reduced. While practically useful and proven in some special cases, this method doesn’t offer any guarantee of success in general. In this work, we present an adaptive-precision version of a generalized lll algorithm that covers this case in all generality. In particular, we replace floating-point arithmetic by Interval Arithmetic to certify the behavior of the algorithm. We conclude by giving a typical application of the result in algebraic number theory for the reduction of ideal lattices in number fields
Person Recognition in Personal Photo Collections
People nowadays share large parts of their personal lives through social media. Being able to automatically recognise people in personal photos may greatly enhance user convenience by easing photo album organisation. For human identification task, however, traditional focus of computer vision has been face recognition and pedestrian re-identification. Person recognition in social media photos sets new challenges for computer vision, including non-cooperative subjects (e.g., backward viewpoints, unusual poses) and great changes in appearance. To tackle this problem, we build a simple person recognition framework that leverages convnet features from multiple image regions (head, body, etc.). We propose new recognition scenarios that focus on the time and appearance gap between training and testing samples. We present an in-depth analysis of the importance of different features according to time and viewpoint generalisability. In the process, we verify that our simple approach achieves the state of the art result on the PIPA [1] benchmark, arguably the largest social media based benchmark for person recognition to date with diverse poses, viewpoints, social groups, and events. Compared the conference version of the paper [2] , this paper additionally presents (1) analysis of a face recogniser (DeepID2+ [3] ), (2) new method naeil2 that combines the conference version method naeil and DeepID2+ to achieve state of the art results even compared to post-conference works, (3) discussion of related work since the conference version, (4) additional analysis including the head viewpoint-wise breakdown of performance, and (5) results on the open-world setup