05 Fakultät Informatik, Elektrotechnik und Informationstechnik
Permanent URI for this collectionhttps://elib.uni-stuttgart.de/handle/11682/6
Browse
9 results
Search Results
Item Open Access Verifiable tally-hiding remote electronic voting(2023) Liedtke, Julian; Küsters, Ralf (Prof. Dr.)Electronic voting (e-voting) refers to casting and counting votes electronically, typically through computers or other digital interfaces. E-voting systems aim to make voting secure, efficient, convenient, and accessible. Modern e-voting systems are designed to keep the votes confidential and provide verifiability, i.e., everyone can check that the published election result corresponds to how voters intended to vote. Several verifiable e-voting systems have been proposed in the literature, with Helios being one of the most prominent ones. However, almost all verifiable e-voting systems reveal not just the voting result but also the tally, consisting of the exact number of votes per candidate or even all single votes. Publishing the tally causes several issues. For example, in elections with only a few voters (e.g., boardroom or jury votings), exposing the tally prevents ballots from being anonymous, thus deterring voters from voting for their actual preference. Furthermore, attackers can exploit the tally for so-called Italian attacks that allow for easily coercing voters. Often, the voting result merely consists of a single winner or a ranking of candidates, so disclosing only this information, not the tally, is sufficient. Revealing the tally unnecessarily embarrasses defeated candidates and causes them a severe loss of reputation. For these reasons, there are several real-world elections where authorities do not publish the tally but only the result - while the current systems for this do not ensure verifiability. We call the property of disclosing the tally tally-hiding. Tally-hiding offers entirely new opportunities for voting. However, a secure e-voting system that combines tally-hiding and verifiability does not exist in the literature. Therefore, this thesis presents the first provable secure e-voting systems that achieve both tally-hiding and verifiability. Our Ordinos framework achieves the strongest notion of tally-hiding: it only reveals the election result. Many real-world elections follow an alternative variant of tally-hiding: they reveal the tally to the voting authorities and only publish the election result to the public - so far without achieving verifiability. We, for the first time, formalize this concept and coin it public tally-hiding. We propose Kryvos, which is the first provable secure e-voting system that combines public tally-hiding and verifiability. Kryvos offers a new trade-off between privacy and efficiency that differs from all previous tally-hiding systems and allows for a radically new protocol design, resulting in a practical e-voting system. We implemented and benchmarked Ordinos and Kryvos, showing the practicability of our systems for real-world elections for significant numbers of candidates, complex voting methods, and result functions. Moreover, we extensively analyze the impact of tally-hiding on privacy compared to existing practices for various elections and show that applying tally-hiding improves privacy drastically.Item Open Access Improved usability of differential privacy in machine learning : techniques for quantifying the privacy-accuracy trade-off(2022) Bernau, Daniel; Küsters, Ralf (Prof.)Differential privacy allows bounding the influence that training data records have on a neural network. To use differential privacy in machine learning with neural networks, data scientists must choose privacy parameter epsilon. Choosing meaningful privacy parameters is key since differentially private neural networks that have been trained with weak privacy parameters might result in excessive privacy leakage, while strong privacy parameters might overly degrade model utility. However, privacy parameter values are difficult to choose for two main reasons. First, the theoretical upper bound on privacy loss epsilon might be loose, depending on the chosen sensitivity and data distribution of practical datasets. Second, legal requirements and societal norms for anonymization often refer to individual identifiability, to which epsilon is only indirectly related. Within this thesis, we address the problem of choosing epsilon from two angles. First, we quantify the empirical lower bound on the privacy loss under empirical membership inference attacks to allow data scientists to compare the empirical privacy-accuracy trade-off between local and central differential privacy. Specifically, we consider federated and non-federated discriminative models, as well as generative models. Second, we transform the privacy loss under differential privacy into an analytical bound on identifiability map legal and societal expectations w.r.t. identifiability to corresponding privacy parameters. The thesis contributes techniques for quantifying the trade-off between accuracy and privacy over epsilon. The techniques provide information for interpreting differentially private training datasets or models trained with the differentially private stochastic gradient descent to improve usability of differential privacy in machine learning. In particular, we identify preferable ranges for privacy parameter epsilon and compare local and central differential privacy mechanisms for training differentially private neural networks under membership inference adversaries. Furthermore, we contribute an implementable instance of the differential privacy adversary that can be used to audit trained models w.r.t. identifiability.Item Open Access An expressive formal model of the web infrastructure(2018) Fett, Daniel; Küsters, Ralf (Prof. Dr.)The World Wide Web is arguably the most important medium of our time. Billions of users rely on the security of the web each day for tasks such as banking, shopping, and business and private communication. The web is a heterogeneous infrastructure developing at a high pace. The question of whether the web infrastructure or certain web applications are secure is not easy to answer. Standards and applications today are reviewed by experts before they are deployed, but all too often even serious security vulnerabilities are simply overlooked. In this thesis, we propose a formal model for the web infrastructure which enables a rigorous formal analysis of security and privacy in the web. Our model is the most comprehensive and expressive model of the web infrastructure to date. It facilitates accurate security and privacy analyses of current web standards and applications, and can serve as a reference for web security researchers, developers of new technologies and standards, and for teaching web security concepts. As a case study we analyze the security of two important standards for federated authorization and authentication, OAuth 2.0 and OpenID Connect. Standardized by the IETF and OpenID Foundation, respectively, they are among the most widely deployed single sign-on systems in the web. For our analysis, we develop detailed formal models for both systems based on our model of the web infrastructure. These models then allow us to precisely define the security goals of authentication, authorization and session integrity. While proving security with respect to these goals, we found a total of five new attacks on the two single sign-on systems, breaking all of the security goals. In particular OAuth 2.0 had been analyzed many times before; the fact that we were able to find new attacks in OAuth 2.0 demonstrates the potential of rigorous analyses in our web infrastructure model. We develop fixes against the underlying vulnerabilities and are then able to prove the security of OAuth 2.0 and OpenID Connect. Since our results are based on a comprehensive model, our proofs can exclude large classes of attacks against OAuth and OpenID Connect, including yet unknown attack vectors. Our attacks and fixes led to the development of new security recommendations by the standardization organizations.Item Open Access Differential privacy for sequential and directional data(2023) Weggenmann, Benjamin; Küsters, Ralf (Prof. Dr.)This dissertation is concerned with mechanisms to protect the privacy of individuals in special types of data that are sequential or directional in nature. Importantly, sequential data includes human language which is commonly conveyed as text or speech (i.e., a sequence of words, symbols, or speech sounds), whereas directional data includes natural examples such as geographic locations and periodic time specifications. In many cases, such data may expose sensitive information that violate the privacy of individuals or even reveal their identity. Differential privacy (DP) is a formal notion of privacy based on randomness that allows quantifying and limiting information disclosure about individuals. While many DP mechanisms exist for structured data such as scalars or numerical vectors, we found a lack of suitable mechanisms for sequential and directional data: For instance, at the time of starting this dissertation, we found no existing DP mechanisms for textual data, and existing mechanisms for geolocations assumed only planar coordinates. To fill these gaps, we aim at constructing novel privacy mechanisms for sequential and directional data and assessing their DP properties. Specifically, we develop methods to obfuscate text as an example of sequential data which either produce differentially private text representations or human-readable texts. Moreover, we introduce directional privacy, a special variant of DP for directional data along with two suitable directional privacy mechanisms that intrinsically respect the directional nature of the data to be obfuscated. We evaluate our proposed methods in realistic use cases to assess their performance regarding protection of privacy and preservation of utility in the obfuscated data. The results show that our methods for text effectively reduce re-identification risks of authorship attribution attacks while maintaining high utility for topic or sentiment analysis tasks. Furthermore, our directional mechanisms typically require fewer data to achieve a certain level of utility than standard privacy mechanisms adapted to directional data. To our best knowledge, our work contributes the first DP mechanism for text and also has inspired other mechanisms that work on a word-level. Moreover, we are the first to exploit synergies between variational autoencoders and the Gaussian mechanism to achieve DP for human-readable text - an approach that is likely extensible to other domains of sequential data. Lastly, our work on directional privacy further provides theoretical contributions to directional statistics including a novel sampling algorithm for the Purkayastha distribution.Item Open Access Privacy-preserving web single sign-on : formal security analysis and design(2019) Schmitz, Guido; Küsters, Ralf (Prof. Dr.)Web-based single sign-on (SSO) systems enable Web sites, so-called relying parties (RPs), to outsource user authentication to other entities, so-called identity providers (IdPs). Such systems are widely deployed in the Web, e.g., Facebook Login or Google Sign-in. RPs do not need to maintain authentication data of their users, and users can log in at RPs in a convenient way. Fundamental to SSO is security: The SSO protocol must not permit an attacker to impersonate anyone else, nor must it allow a false identity to be imposed on anyone. If this is not the case, attacks are possible that have devastating effects on the security of RPs and their users. While aiming at security, most SSO systems, however, neglect privacy. IdPs can track their users as they (by design) learn at which RP a user logs in. This lack of privacy allows IdPs to create extensive user profiles and might cause some users not to use SSO at all. Moreover, IdPs are enabled to decide ad-hoc whether they allow a user to log in at a specific RP. Therefore, privacy-preserving systems, which do not reveal to IdPs to which RP a user would like to log in or has logged in, are highly desirable in many situations. The design of such systems, however, is very challenging because privacy can easily be compromised. So far, only one SSO system has been proposed with this kind of privacy in mind: Mozilla's BrowserID (a.k.a. Mozilla Persona). In this thesis, we use the Web Infrastructure Model (WIM) to analyze the security of SSO protocols. The WIM is the most comprehensive formal model of the Web infrastructure to date, which applies to a wide range of Web applications and standards. We also extend the WIM to be able to analyze privacy. We use the extended WIM to, for the first time, carry out a systematic and rigorous formal analysis of privacy for Web SSO systems. Using our approach, we analyze the Web SSO system BrowserID. As a result of this first rigorous analysis of an SSO system in the Web infrastructure, we find severe attacks. These attacks not only affect the security of BrowserID but also show that BrowserID's unique privacy claim does not hold. We propose fixes for BrowserID and prove that the fixed system provides security. Regarding privacy, we show that BrowserID, unfortunately, is broken beyond repair. Inspired by BrowserID's goal, we propose the first privacy-preserving Web SSO system, called SPRESSO (for Secure Privacy-REspecting Single Sign-On). SPRESSO is easy to use, decentralized and based solely on native Web features. We design SPRESSO within the WIM right from the start and prove that SPRESSO satisfies strong security and privacy guarantees.Item Open Access Composable accountability for distributed ledgers(2024) Graf, Mike; Küsters, Ralf (Prof. Dr.)Item Open Access Design and cryptographic security analysis of e-voting protocols(2019) Müller, Johannes; Küsters, Ralf (Prof. Dr.)Electronic voting (e-voting) systems are used in numerous countries for political elections, but also for less critical elections within clubs and associations, and hence affect the lives of millions of people. It is therefore important to ensure that single voters' choices remain private, and to be able to verify that an election result coincides with the voters' intention. Unfortunately, for most e-voting systems employed in real elections, these fundamental security and privacy properties cannot be guaranteed, so that in particular the legitimacy of such political elections is challenged. This demonstrates the importance of employing e-voting systems that are rootedly designed to guarantee the required security. However, it turned out to be highly challenging to construct secure yet practical e-voting systems since one always has to find a balance between the (possibly conflicting) requirements of the given kind of election. In the first two chapters of the thesis' main part, we present two practical e-voting systems which are both meant for low-risk and non-political elections, e.g., within clubs or associations. We have implemented both systems to demonstrate their practicability. The first system, called sElect, is designed to be as simple as possible while still guaranteeing a good level of security. The second system, called Ordinos, provides a superior level of privacy as it only reveals the most necessary information about the election outcome, e.g., solely the winner's name but nothing else. We will rigorously analyze the security of sElect and Ordinos. To do this, we formally define the required security properties and then mathematically prove that sElect and Ordinos achieve them. In the third chapter of the thesis' main part, we provide substantial work on the fundamental notion of verifiability of e-voting systems. We analyze and compare all formal verifiability definitions from the literature regarding how meaningful, expressive, or general they are.Item Open Access Simple and flexible universal composability : definition of a framework and applications(2020) Rausch, Daniel; Küsters, Ralf (Prof. Dr.)Security protocols, such as TLS, SSH, IEEE~802.11, and DNSSEC, have become crucial tools in modern society to protect people, data, and infrastructure. They are used throughout virtually all electronic devices to achieve a wide range of different security goals, such as confidentiality, authentication, and integrity. As the long history of attacks on security protocols illustrates, it is indispensable to perform a formal security analysis of such protocols. A central tool in cryptography for taming the complexity of the design and the analysis of modern protocols is modularity, provided by security models for universal composability. Such models allow for designing and analyzing small parts of a protocol in isolation and then reusing these security results in the context of the overall protocol. This is not just easier than analyzing the whole protocol as a monolithic block but also reduces the overall effort required in building and analyzing multiple different protocols based on the same underlying components, such as cryptographic primitives. Ideally, a model for universal composability should support a protocol designer in easily creating full, precise, and detailed specifications as well as sound security proofs of various protocols for various types of adversarial models, instead of being an additional obstacle one has to overcome during a security analysis. In particular, such a model should be sound, flexible/expressive, and easy to use. Unfortunately, despite the wide spread use of models for universal composability, existing models and frameworks are still unsatisfying in these respects as none combines all of these requirements simultaneously. In this thesis we therefore develop a model for universal composability, called the iUC framework, which combines soundness, usability, and flexibility in a so far unmatched way, and hence constitutes a solid framework for designing and analyzing essentially any protocol and application in a modular, universally composable, and sound manner. We use our model in a case study to analyze multiple different key exchange protocols precisely as they are deployed in practice. This illustrates the combination of both flexibility and usability of our model. This case study is also an important independent contribution as this is the first faithful security analysis of these unmodified protocols in a universal composability setting.Item Open Access Implementation-level analysis of cryptographic protocols and their applications to e-voting systems(2018) Scapin, Enrico; Küsters, Ralf (Prof. Dr.)Formal verification of security properties of both cryptographic operations, such as encryption, and protocols based on them, such as TLS, has been the goal of a substantial research effort in the last three decades. One fundamental limitation in the verification of these security properties is that analyses are typically carried out at the design level and hence they do not provide reliable guarantees on the implementations of these operations/protocols. To overcome this limitation, in this thesis we aim at establishing formally justified cryptographic guarantees directly at the implementation level for systems that are coded in Java and use cryptography. Our approach is based on a general framework for the cryptographic verification of Java programs (the CVJ framework) which formally links cryptographic indistinguishability properties and noninterference properties. In this way, it enables existing tools that can check standard noninterference properties, but a priori cannot deal with cryptography, to also establish cryptographic privacy properties for Java systems. The CVJ framework is stated and proven for a Java-like formal language which however does not cover all the data types and features commonly used in Java programs. Moreover, the framework originally supports only one cryptographic operation, namely public-key encryption. The first contribution of this thesis is hence to extend and to instantiate the CVJ framework in order to make it more widely applicable. We extend the underlying formal language with some features of Java which have not been captured yet, such as concurrency, and we restate and prove all the results of the framework to carry them over into this extended language. We then further instantiate the framework with additional cryptographic operations: digital signatures and public-key encryption, both now also including a public-key infrastructure, (private) symmetric encryption, and nonce generation. The methods and techniques developed within the CVJ framework are relevant and applicable independently of any specific tool employed. However, to illustrate the usefulness of this approach, we apply the framework along with two verification tools for Java programs, namely the fully automated static checker Joana and the interactive theorem prover KeY, to establish strong cryptographic privacy properties for systems which use cryptography, such as client-server applications and e-voting systems. In this context, the second major contribution of this thesis is the design, the implementation, and the deployment of a novel remote voting system called sElect (secure/simple elections). sElect is designed to be particularly simple and lightweight in terms of its structure, the cryptography it uses, and the user experience. One of its unique features is a fully automated procedure which does not require any user interaction and it is triggered as soon as voters look at the election result, allowing them to verify that their vote has been properly counted. The component of sElect which provides vote privacy is implemented in Java such that we can establish cryptographic guarantees directly on its implementation: by combining the techniques of the CVJ framework with a hybrid approach for proving noninterference, we are able to show that the Java implementation ensures strong cryptographic privacy of the votes cast with our proposed voting system. sElect is therefore the first full-fledged e-voting system with strong cryptographic security guarantees not only at the design level, but also on its implementation.