With the rise of attacks on online accounts in the past years, more and more services offer two-factor authentication for their users. Having factors out of two of the three categories something you know, something you have and something you are should ensure that an attacker cannot compromise two of them at once. Thus, an adversary should not be able to maliciously interact with one's account. However, this is only true if one considers a weak adversary. In particular, since most current solutions only authenticate a session and not individual transactions, they are noneffective if one's device is infected with malware. For online banking, the banking industry has long since identified the need for authenticating transactions. However, specifications of such authentication schemes are not public and implementation details vary wildly from bank to bank with most still being unable to protect against malware. In this work, we present a generic approach to tackle the problem of malicious account takeovers, even in the presence of malware. To this end, we define a new paradigm to improve two-factor authentication that involves the concepts of one-out-of-two security and transaction authentication. Web authentication schemes following this paradigm can protect security-critical transactions against manipulation, even if one of the factors is completely compromised. Analyzing existing authentication schemes, we find that they do not realize one-out-of-two security. We give a blueprint of how to design secure web authentication schemes in general. Based on this blueprint we propose FIDO2 With Two Displays (FIDO2D), a new web authentication scheme based on the FIDO2 standard and prove its security using Tamarin. We hope that our work inspires a new wave of more secure web authentication schemes, which protect security-critical transactions even against attacks with malware.

The cryptographic methodology of formal security analysis usually works in three steps: choosing a security model, describing a system and its intended security properties, and creating a formal proof of security. For basic cryptographic primitives and simple protocols this is a well understood process and is performed regularly. For more complex systems, as they are in use in real-world settings it is rarely applied, however. In practice, this often leads to missing or incomplete descriptions of the security properties and requirements of such systems, which in turn can lead to insecure implementations and consequent security breaches. One of the main reasons for the lack of application of formal models in practice is that they are particularly difficult to use and to adapt to new use cases. With this work, we therefore aim to investigate how cryptographic security models can be used to argue about the security of real-world systems. To this end, we perform case studies of three important types of real-world systems: data outsourcing, computer networks and electronic payment. First, we give a unified framework to express and analyze the security of data outsourcing schemes. Within this framework, we define three privacy objectives: \emph{data privacy}, \emph{query privacy}, and \emph{result privacy}. We show that data privacy and query privacy are independent concepts, while result privacy is consequential to them. We then extend our framework to allow the modeling of \emph{integrity} for the specific use case of file systems. To validate our model, we show that existing security notions can be expressed within our framework and we prove the security of CryFS---a cryptographic cloud file system. Second, we introduce a model, based on the Universal Composability (UC) framework, in which computer networks and their security properties can be described We extend it to incorporate time, which cannot be expressed in the basic UC framework, and give formal tools to facilitate its application. For validation, we use this model to argue about the security of architectures of multiple firewalls in the presence of an active adversary. We show that a parallel composition of firewalls exhibits strictly better security properties than other variants. Finally, we introduce a formal model for the security of electronic payment protocols within the UC framework. Using this model, we prove a set of necessary requirements for secure electronic payment. Based on these findings, we discuss the security of current payment protocols and find that most are insecure. We then give a simple payment protocol inspired by chipTAN and photoTAN and prove its security within our model. We conclude that cryptographic security models can indeed be used to describe the security of real-world systems. They are, however, difficult to apply and always need to be adapted to the specific use case.

The home Battery Energy Storage System (BESS) industry is on the rise [1]. Newer models are built as Internet-connected devices that offer new service models for customers and manufacturers alike. This approach, as can be observed from emerging Internet of Things (IoT) devices in the last decade, brings new challenges and issues with it. First of all, threats to user privacy and botnet attacks come to mind. More importantly, there are now substantial advances to put flexible BESS in more critical roles in the power grid and let them provide primary balancing power in order to compensate fluctuations [2]. However, while the safety properties of such systems are currently being explored by researchers [3], their security is mostly unexplored and unregulated. To explore the state of security of residential BESS, we systematically analyzed commercially available storage systems from ten different manufacturers, who have a combined market share of more than 60 percent in Germany [4]. We show that all of them have security issues and four of them contain severe security flaws. In order to exemplify the deficit in the industry to properly secure Internet connected devices, we present three attacks in detail.

EMV, also known as Chip and PIN, is the world-wide standard for card-based electronic payment. Its security wavers: over the past years, researchers have demonstrated various practical attacks, ranging from using stolen cards by disabling PIN verification to cloning cards by pre-computing transaction data. Most of these attacks rely on violating certain unjustified and not explicitly stated core assumptions upon which EMV is built, namely that the input device (e.g. the ATM) is trusted and all communication channels are non-interceptable. In addition, EMV lacks a comprehensive formal description of its security. In this work we give a formal model for the security of electronic payment protocols in the Universal Composability (UC) framework. A particular challenge for electronic payment is that one participant of a transaction is a human who cannot perform cryptographic operations. Our goal is twofold. First, we want to enable a transition from the iterative engineering of such protocols to using cryptographic security models to argue about a protocol's security. Second, we establish a more realistic adversarial model for payment protocols in the presence of insecure devices and channels. We prove a set of necessary requirements for secure electronic payment with regards to our model. We then discuss the security of current payment protocols based on these results and find that most are insecure or require unrealistically strong assumptions. Finally, we give a simple payment protocol inspired by chipTAN and photoTAN and prove its security. Our model captures the security properties of electronic payment protocols with human interaction. We show how to use this to reason about necessary requirements for secure electronic payment and how to develop a protocol based on the resulting guidelines. We hope that this will facilitate the development of new protocols with well-understood security properties.

Die IT-Sicherheit, eine Grundvoraussetzung für Digitale Souveränität, ist in einem kritischen Zustand. Hersteller von IT-Produkten sind häufig nicht bereit, das Problem eigenverantwortlich anzugehen, und es fehlen wirksame, für alle geltende gesetzliche Regelungen. Die Autoren schlagen daher, inspiriert durch die Datenschutzgrundverordnung, die Einführung einer „IT-Sicherheits-Grundverordnung“ vor und diskutieren die dafür wichtigen Regelungen.

Using the cloud to store data offers many advantages for businesses and individuals alike. The cloud storage provider, however, has to be trusted not to inspect or even modify the data they are entrusted with. Encrypting the data offers a remedy, but current solutions have various drawbacks. Providers which offer encrypted storage themselves cannot necessarily be trusted, since they have no open implementation. Existing encrypted file systems are not designed for usage in the cloud and do not hide metadata like file sizes or directory structure, do not provide integrity, or are prohibitively inefficient. Most have no formal proof of security. Our contribution is twofold. We first introduce a comprehensive formal model for the security and integrity of cloud file systems. Second, we present 𝖢𝗋𝗒𝖥𝖲 , a novel encrypted file system specifically designed for usage in the cloud. Our file system protects confidentiality and integrity (including metadata), even in presence of an actively malicious cloud provider. We give a proof of security for these properties. Our implementation is easy and transparent to use and offers performance comparable to other state-of-the-art file systems.

In der modernen Kryptographie wird „Sicherheit“ mathematisch definiert. Einer der etablierten Ansätze, Sicherheit zu definieren, ist die „Simulationsbasierte Sicherheit“, bei der Sicherheit keine absolute Größe ist, sondern durch Vergleich mit fiktionalen, ideal sicheren kryptographischen Protokollen definiert wird. Dieser Artikel stellt neue Entwicklungen vor.

Es gibt verschiedene Ausprägungen der Blockchain-Technologie; einige davon wurden in DuD 8/2017 vorgestellt. Sie unterscheiden sich insbesondere in den ihnen zugrundeliegenden (Sicherheits-) Annahmen und Mechanismen. Daher darf die Blockchain nicht als Universaltechnologie gesehen werden–die Gründe dafür diskutieren die Autoren im vorliegenden Beitrag.

Electronic voting machines promise to determine election results more efficiently without sacrificing reliability. Two desirable security properties seem to contradict each other however: First, the voter's choice is to be kept secret at all costs, even from election officers who set up and administrate the election machine. On the other hand, ballot secrecy should not compromise the correctness of the tally. We present a construction that conceals the voter's choice even from the voting machine while producing a provably-correct tally. Our scheme is an improvement of Bingo Voting [1]. To hide the voter's choice from the voting machine, we conceive of an electro-mechanical physical oblivious transfer (pOT) device. We further use blind commitments, an extension of cryptographic commitments. Blind commitments can jointly be created by a group of entities, while no single entity is aware of the hidden secret. They can later be unveiled in another multi-party computation. This work is an extended version of a conference paper [2]. In this version, we work out the details of our construction. Our results corroborate the feasibility of an electronic voting machine that is oblivious to the voters' choices.

When designing an electronic voting scheme it is notoriously difficult to guarantee the secrecy of the vote as well as the correctness of the tally, even in the presence of a malicious adversary. Research in (offline) cryptographic voting schemes has largely relied on a trusted voting machine for guaranteeing security. We alleviate part of this trust requirement. Our scheme ensures the confidentiality of the vote even in the presence of an honest-but-curious voting machine. We improve on Bohli et al.’s Bingo Voting scheme (Bohli et al., 2007). Bingo Voting already guarantees the correctness and public verifiability of the election in spite of a malicious voting machine. The voting machine learns the voter’s input however, and is trusted not to violate ballot secrecy. Our novel construction’s output is identical to that of Bingo Voting. We devise an electro-mechanical Physical Oblivious Transfer (pOT) device to remove that trust requirement by hiding the voter’s choice from the voting machine. The pOT device is realised in such a way that the voter merely operates a button to express her choice. Our construction is thus particularly user-friendly.

Designers of modern IT networks face tremendous security challenges. As systems grow ever more complex and connected it is essential that they resist even previously-unknown attacks. Using formal models to analyse the security of cryptographic protocols is a well-established practice. However, the security of complex networks is often still evaluated in an ad-hoc fashion. We analyse the applicability of formal security models for complex networks and narrow the gap between security proofs for abstract cryptographic protocols and real-world systems. Specifically we use the Universal Composability framework together with Katz et al.’s extensions for synchronous computation and bounded-delay channels [15]. This allows us to model availability guarantees. We propose a 5-phase paradigm for specifying protocols in a clear representation. To capture redundant formalisms and simplify defining network topologies, we introduce two functionalities ℱ_𝗐𝗋𝖺𝗉 and ℱ_𝗇𝖾𝗍 . Demonstrating the applicability of our approach, we re-prove Lamport et al.’s well-known solution to the Byzantine Generals Problem [16] with four parties. We further complete a result of Achenbach et al. [1], proving that a “firewall combiner” for three network firewalls is available.

We study formal privacy notions for data outsourcing schemes. The aim of our efforts is to define a security framework that is applicable to highly elaborate as well as practical constructions. First, we define the privacy objectives data privacy, query privacy, and result privacy. We then investigate fundamental relations among them. Second, to make them applicable to practical constructions, we define generalisations of our basic notions. Lastly, we show how various notions from the literature fit into our framework. Data privacy and query privacy are independent concepts, while result privacy is consequential to them. The generalised notions allow for a restriction on the number of the adversary’s oracle calls, as well as a “leakage relation” that restricts the adversary’s choice of challenges. We apply the generalised notions to existing security notions from the fields of searchable encryption, private information retrieval, and secure database outsourcing. Some are direct instantiations of our notions, others intertwine the concepts. This work provides a privacy framework for data outsourcing schemes from various cryptographic fields with an unified view, from which several new interesting research questions emerge.

Network firewalls are a standard security measure in computer networks that connect to the Internet. Often, ready-to-use firewall appliances are trusted to protect the network from malicious Internet traffic. However, because of their black-box nature, no one can be sure of their exact functionality. We address the possibility of actively compromised firewalls. That is, we consider the possibility that a network firewall might collaborate with an outside adversary to attack the network. To alleviate this threat, we suggest composing multiple firewalls from different suppliers to obtain a secure firewall architecture. We rigorously treat the composition of potentially malicious network firewalls in a formal model based on the Universal Composability framework. Our security assumption is trusted hardware. We show that a serial concatenation of firewalls is insecure even when trusted hardware ensures that no new packages are generated by the compromised firewall. Further, we show that the parallel composition of two firewalls is only secure when the order of packets is not considered. We prove that the parallel composition of three firewalls is insecure, unless a modified trusted hardware is used.

Searchable Encryption schemes allow searching within encrypted data without prior decryption. Various index-based schemes have been proposed in the past, which are only adequate for certain use cases. There is a lack of schemes with exact pattern matching capabilities. We introduce Symmetric Searchable Encryption for Exact Pattern Matching, a new class of searchable encryption schemes. To this end, we define the XPM-SSE primitive and two privacy notions for the new primitive. Our own construction, SEDAWG, is a XPM-SSE scheme which uses Directed Acyclic Word Graphs. We discuss and prove its properties.