Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Verifiable Timed Signatures Made Practical
A verifiable timed signature (VTS) scheme allows one to time-lock a signature on a known message for a given amount of time T such that after performing a sequential computation for time T anyone can extract s from the time-lock. Verifiability ensures that anyone can publicly check if a time-lock contains a valid signature on m without solving it first, and that the signature can be obtained by solving the same for time T.
This work formalizes VTS, presents efficient constructions compatible with BLS, Schnorr, and ECDSA signatures, and experimentally demonstrates that (unlike the predecessors) our constructions can be employed in practice. On a technical level, we design an efficient cut-and-choose protocol based on the recently proposed homomorphic time-lock puzzles to prove the validity of a signature encapsulated in a time-lock puzzle. We also present a new efficient range proof protocol that significantly improves upon existing proposals in terms of the proof size, and is of independent interest.
VTS is a versatile tool with numerous existing applications. In this work, we demonstrate VTS’s applicability to resolve three challenging issues in the space of cryptocurrencies. Specifically, we show how VTS is the cryptographic cornerstone to construct:
(i) Payment channel networks with improved on-chain unlinkability of users involved in a transaction,
(ii) multi-party signing of transactions
for cryptocurrencies without any on-chain notion of time and
(iii) cryptocurrency-enabled fair multi-party computation protocol
A Spectral Analysis of Noise:A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols
The Noise specification describes how to systematically construct a large family of Diffie-Hellman based key exchange protocols, including the secure transports used by WhatsApp,Lightning, and WireGuard. As the specification only makes informal security claims, earlier work has explored which formal security properties may be enjoyed by protocols in the Noise framework, yet many important questions remain open.In this work we provide the most comprehensive, systematic analysis of the Noise framework to date. We start from first principles and, using an automated analysis tool, compute the strongest threat model under which a protocol is secure,thus enabling formal comparison between protocols. Our results allow us to objectively and automatically associate each informal security level presented in the Noise specification with a formal security claim. We also provide a fine-grained separation of Noise protocols that were previously described as offering similar security properties, revealing a subclass for which alternative Noise protocols exist that offer strictly better security guarantees. Our analysis also uncovers missing assumptions in the Noise specification and some surprising consequences,e.g.,in some situations higher security levels yield strictly worse securit
Cash, Cards or Cryptocurrencies? A Study of Payment Culture in Four Countries
Payment cultures around the globe are diverse and have significant implications on security, privacy and trust. We study usable security aspects of payment cultures in four culturally distinct societies. Based on a qualitative study in Germany and Iran, we developed an online survey and deployed it in Germany, Iran, China, and the United States. The results reveal significant differences between the studied countries. For example, we found that participants from Iran and China are more comfortable with credential sharing and German participants were most accepting towards cryptocurrencies. We suggest these kinds of differences in payment culture need to be considered in the context of HCI research when evaluating current payment mechanisms or designing new ones
On the Parameterized Complexity of Maximum Degree Contraction Problem
In the Maximum Degree Contraction problem, input is a graph G on n vertices, and integers k, d, and the objective is to check whether G can be transformed into a graph of maximum degree at most d, using at most k edge contractions. A simple brute-force algorithm that checks all possible sets of edges for a solution runs in time n^O(k). As our first result, we prove that this algorithm is asymptotically optimal, upto constants in the exponents, under Exponential Time Hypothesis (ETH). Belmonte, Golovach, van't Hof, and Paulusma studied the problem in the realm of Parameterized Complexity and proved, among other things, that it admits an FPT algorithm running in time (d + k)^(2k) ⋅ n^O(1) = 2^O(k log (k+d)) ⋅ n^????(1), and remains NP-hard for every constant d ≥ 2 (Acta Informatica (2014)). We present a different FPT algorithm that runs in time 2^O(dk) ⋅ n^O(1). In particular, our algorithm runs in time 2^O(k) ⋅ n^O(1), for every fixed d. In the same article, the authors asked whether the problem admits a polynomial kernel, when parameterized by k + d. We answer this question in the negative and prove that it does not admit a polynomial compression unless NP ⊆ coNP/poly
Isomorphism Testing for Graphs Excluding Small Minors
We prove that there is a graph isomorphism test running in time n^{polylog(h)} on n-vertex graphs excluding some h-vertex graph as a minor. Previously known bounds were n^{poly(h)} (Ponomarenko, 1988) and n^{polylog(n)} (Babai, STOC 2016). For the algorithm we combine recent advances in the group-theoretic graph isomorphism machinery with new graph-theoretic arguments
Raccoon: Automated Verification of Guarded Race Conditions in Web Applications
Web applications are distributed, asynchronous applications that can span multiple concurrent processes. They are intended to be used by a large amount of users at the same time. As concurrent applications, web applications have to account for race conditions that may occur when database access happens concurrently. Unlike vulnerability classes, such as XSS or SQL Injection, dbms based race condition flaws have received little attention even though their impact is potentially severe. In this paper, we present Raccoon, an automated approach to detect and verify race condition vulnerabilities in web application. Raccoon identifies potential race conditions through interleaving execution of user traces while tightly monitoring the resulting database activity. Based on our methodology we create a proof of concept implementation. We test four different web applications and ten use cases and discover six race conditions with security implications. Raccoon requires neither security expertise nor knowledge about implementation or database layout, while only reporting vulnerabilities, in which the tool was able to successfully replicate a practical attack. Thus, Raccoon complements previous approaches that did not verify detected possible vulnerabilities
TrollThrottle — Raising the Cost of Astroturfing
Astroturfing, i.e., the fabrication of public discourse by private or state-controlled sponsors via the creation of fake online accounts, has become incredibly widespread in recent years. It gives a disproportionally strong voice to wealthy and technology-savvy actors, permits targeted attacks on public forums and could in the long run harm the trust users have in the internet as a communication platform. Countering these efforts without deanonymising the participants has not yet proven effective; however, we can raise the cost of astroturfing. Following the principle `one person, one voice', we introduce Trollthrottle, a protocol that limits the number of comments a single person can post on participating websites. Using direct anonymous attestation and a public ledger, the user is free to choose any nickname, but the number of comments is aggregated over all posts on all websites, no matter which nickname was used. We demonstrate the deployability of Trollthrottle by retrofitting it to the popular news aggregator website Reddit and by evaluating the cost of deployment for the scenario of a national newspaper (168k comments per day), an international newspaper (268k c/d) and Reddit itself (4.9M c/d)
RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft
The autonomous control of unmanned aircraft is a highly safety-critical domain with great economic potential in a wide range of application areas, including logistics, agriculture, civil engineering, and disaster recovery. We report on the development of a dynamic monitoring framework for the DLR ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) family of unmanned aircraft based on the formal specification language RTLola. RTLola is a stream-based specification language for real-time properties. An RTLola specification of hazardous situations and system failures is statically analyzed in terms of consistency and resource usage and then automatically translated into an FPGA-based monitor. Our approach leads to highly efficient, parallelized monitors with formal guarantees on the noninterference of the monitor with the normal operation of the autonomous system