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.
Der digitale Wandel ist Chance und Risiko zugleich: eine große Chance, weil er Prozesse und Abläufe vereinfacht und beschleunigt, und ein Risiko für diejenigen Unternehmen, die (noch) nicht darauf vorbereitet sind, dass ihre IT angegriffen werden kann. Kommt es zu einem Sicherheitsvorfall, kann das für kleine und mittlere Unternehmen existenzbedrohend sein, wenn nicht schnell und angemessen darauf reagiert wird. Im Pilotprojekt Cyberwehr Baden-Württemberg werden daher Infrastrukturen für die Ersthilfe bei IT-Sicherheitsvorfällen in kleinen und mittleren Unternehmen entwickelt und erprobt.
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.
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.
In a democracy, it is essential that voters cast their votes independently and freely, without any improper influence. Particularly, mechanisms must be put into place that prevent—or at least severely impede—the coercion of voters. One possible countermeasure to coercion is revoting: after casting a vote under coercion, the voter can re-cast and overwrite her choice. However, revoting is only meaningful as a strategy to evade coercion if the adversary cannot infer whether the voter has modified her choice—revoting needs to be deniable, while still being publicly verifiable. We define the notions of correctness, verifiability, and deniability for a tallying protocol which allows for revoting. We also present a protocol realizing these notions. To the best of our knowledge, our solution is the first to achieve both deniability and public verifiability without asking information about the voter’s previously-cast ballots for revoting. A seemingly competitive line of work, started by the well-known work of Juels, Catalano, and Jakobsson, uses fake credentials as a strategy to evade coercion: the voter presents to the adversary a fake secret for voting. In this work, we extend Juels et al.’s work to achieve deniable revoting. Their solution also allows for revoting, however not deniably. Our solution supports fake credentials as an opt-in property, providing the advantages of both worlds.
Die Kryptographie war über Jahrhunderte eine Geheimwissenschaft. Das hat sich erst mit der Entwicklung des Internet und des daraus resultierenden Bedarfs an allgemeiner Verfügbarkeit kryptographischer Mechanismen geändert. Dennoch zählen die Hintergründe und Funktionsweisen kryptographischer Verfahren nach wie vor nicht zum Allgemeinwissen. Hier will das Kryptologikum abhelfen — eine Ausstellung für die anschauliche Vermittlung von Kryptographiegeschichte und modernen kryptographischen Verfahren und Anwendungen.
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.
The biggest impediment for the adoption of cloud computing practices is the lack of trust in the confidentiality of one's data in the cloud. The prevalent threat in the cloud computing model are so-called insider attacks. Full data encryption can only solve the problem in the trivial case of backups. Any sophisticated service provided on data requires insight into the structure of that data. One purpose of encryption is to prevent such insights. We introduce the MimoSecco project. In MimoSecco, we are investigating reasonable compromises. We employ two techniques, separation of duties and secure hardware. With separation of duties, we fragment a database and separate the fragments geographically. The goal is to make it infeasible to reconstruct the database from one fragment alone. The secure hardware tokens we employ are hard-to-copy devices which offer encryption, decryption and cryptographically signing of data. The keys used are stored in the tamper-proof hardware device and never leave it. We are in the process of developing a prototypical database adapter that behaves like a SQL database, but stores data securely.
Security of public key cryptography is steadily threatened by advancements in algorithmics and computing power. In this work we propose a novel approach to long-term secure key exchange based on security assumptions that are independent of strong complexity assumptions. We present a key propagation scheme that sets up a network of distributed keys. Whenever two parties meet, they exchange new keys (e.g. using near field communication) and pass on all keys received so far. This establishes a dense key network growing and spreading with each meeting of protocol participants. Even two parties that have never met in person can use this network to obtain a common secret. A notable security feature of our scheme is the anonymity of the established keys, making it hard for an adversary to track movements of protocol participants.