Universität Stuttgart
Permanent URI for this communityhttps://elib.uni-stuttgart.de/handle/11682/1
Browse
Search Results
Item Open Access Formal security analysis of the OpenID FAPI 2.0 Security Profile with FAPI 2.0 Message Signing, FAPI-CIBA, Dynamic Client Registration and Management : technical report(2023) Hosseyni, Pedram; Küsters, Ralf; Würtele, TimBuilding on our recent formal security analysis of the FAPI 2.0 Security Profile, we here extend the analysis effort to FAPI 2.0 Message Signing, combined with Dynamic Client Registration, Dynamic Client Management, and FAPI-CIBA. Overall, we model an ecosystem which uses all these profiles and extensions in parallel. Like the previous work on the FAPI 2.0 Security Profile, this analysis is based on the Web Infrastructure Model, a Dolev-Yao style model of the web infrastructure - in fact, it is the most comprehensive and detailed model of the web infrastructure to date. We identify several attacks, propose fixes and prove the fixed protocols secure with respect to authorization, authentication, session integrity for both authorization and authentication, and non-repudiation for the messages covered by FAPI 2.0 Message Signing. The attacks and proposed fixes have been reported to the responsible FAPI Working Group at the OpenID Foundation, and fixes have since been incorporated into the specifications.Item Open Access OpenID for Verifiable Credentials : formal security analysis using the Web Infrastructure Model(2023) Hauck, FabianIn our increasingly connected world, digital identities play a fundamental role in delivering secure online services around the globe. To enable the seamless exchange of identification data among various entities, the adoption of standardized protocols is essential. The protocol family OpenID for Verifiable Credentials (OID4VC) is ideally suited for exchanging identities. The two most important protocols in this family are OpenID for Verifiable Credential Issuance (OID4VCI) and OpenID for Verifiable Presentations (OID4VP) with a wide range of applications in e-government as well as in the private sector. A prominent example is the European Digital Identity Framework, which includes these two protocols, among others. This means that any future wallet in the European Union will implement OID4VCI and OID4VP. Therefore, it is extremely important to guarantee their security. This thesis performs a rigorous formal security analysis of both the OpenID for Verifiable Credential Issuance and the OpenID for Verifiable Presentations protocols. In particular, we focus on analyzing the security of both protocols when they interact in an ecosystem. It is not sufficient to consider the two protocols separately, because the interaction between them may introduce new vulnerabilities. Therefore, the formal model created in this thesis models both protocols simultaneously. The model is based on the Web Infrastructure Model (WIM), which closely follows existing web technologies. To describe what security means in this context, we define an authentication security property and a session integrity security property for OID4VCI and OID4VP. We prove that the model is secure with respect to the security properties under the assumption of a vigilant user. If this assumption is violated, we have discovered a number of attacks. This work makes several contributions to the protocol specifications: First, the discovered vulnera- bilities were brought to the attention of the working group. Second, several issues were filed to improve the quality and security of the specifications. Lastly, we engaged in ongoing discussions on related issues.Item Open Access The Grant Negotiation and Authorization Protocol : attacking, fixing, and verifying an emerging standard(2023) Helmschmidt, Florian; Hosseyni, Pedram; Küsters, Ralf; Pruiksma, Klaas; Waldmann, Clara; Würtele, TimThe Grant Negotiation and Authorization Protocol (GNAP) is an emerging authorization and authentication protocol which aims to consolidate and unify several use-cases of OAuth 2.0 and many of its common extensions while providing a higher degree of security. OAuth 2.0 is an essential cornerstone of the security of authorization and authentication for the Web, IoT, and beyond, and is used, among others, by many global players, like Google, Facebook, and Microsoft. Historical limitations of OAuth 2.0 and its extensions have led prominent members of the OAuth community to create GNAP, a newly designed protocol for authorization and authentication. Given GNAP's advantages over OAuth 2.0 and its support within the OAuth community, GNAP is expected to become at least as important as OAuth 2.0. In this work, we present the first formal security analysis of GNAP. We build a detailed formal model of GNAP, based on the Web Infrastructure Model (WIM) of Fett, Küsters, and Schmitz, and provide formal statements of the key security properties of GNAP, namely authorization, authentication, and session integrity. We discovered several attacks on GNAP in the process of trying to prove these properties. We present these attacks, as well as changes to the protocol that prevent them. These modifications have been incorporated into the GNAP specification after discussion with the GNAP working group. We give the first formal security guarantees for GNAP, by proving that GNAP, with our modifications applied, satisfies the mentioned security properties. GNAP was still an early draft when we began our analysis, but is now on track to be adopted as an IETF standard. Hence, our analysis is just in time to help ensure the security of this important emerging standard.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 MS-RAFT+ : high resolution multi-scale RAFT(2023) Jahedi, Azin; Luz, Maximilian; Rivinius, Marc; Mehl, Lukas; Bruhn, AndrésHierarchical concepts have proven useful in many classical and learning-based optical flow methods regarding both accuracy and robustness. In this paper we show that such concepts are still useful in the context of recent neural networks that follow RAFT’s paradigm refraining from hierarchical strategies by relying on recurrent updates based on a single-scale all-pairs transform. To this end, we introduce MS-RAFT+: a novel recurrent multi-scale architecture based on RAFT that unifies several successful hierarchical concepts. It employs a coarse-to-fine estimation to enable the use of finer resolutions by useful initializations from coarser scales. Moreover, it relies on RAFT’s correlation pyramid that allows to consider non-local cost information during the matching process. Furthermore, it makes use of advanced multi-scale features that incorporate high-level information from coarser scales. And finally, our method is trained subject to a sample-wise robust multi-scale multi-iteration loss that closely supervises each iteration on each scale, while allowing to discard particularly difficult samples. In combination with an appropriate mixed-dataset training strategy, our method performs favorably. It not only yields highly accurate results on the four major benchmarks (KITTI 2015, MPI Sintel, Middlebury and VIPER), it also allows to achieve these results with a single model and a single parameter setting. Our trained model and code are available at https://github.com/cv-stuttgart/MS_RAFT_plus .Item Open Access Critical infrastructure security in the age of cyberwarfare(2023) Sliwa, RobinOur modern critical infrastructure of the 21st century is not only digited; it is also more interconnected than ever before. While this progress has provided many improvements in efficiency, functionality and maintainability, it also introduced new attack vectors. It subsequently has become a target for coordinated attacks by cybercriminal and government-affiliated hacking groups. Especially current circumstances such as the Russian invasion of Ukraine have made the protection of critical infrastructure a central topic of (inter-)national security. This thesis provides an overview over critical infrastructure security in the context of cybersecurity. To that end, modern critical infrastructure is introduced and put in the context of legislative frameworks through the lens of European Union regulations. The central part of this thesis explores landmark attacks and incidents in form of Stuxnet and NotPetya. Followed by this, the adversaries behind such attacks and the resources available by them are analyzed; correspondingly, potential countermeasures and paths to enhanced cybersecurity are introduced. Overall, this thesis finds that critical infrastructure cybersecurity requires a much higher priority by public and private organizations. More than that, it suggests the pursuit of more holistic approaches over isolated measures - and a consideration of cybersecurity implications during all stages of business design and operation.Item Open Access Analysis of selected cryptographic protocols with DY*(2023) Holderbach, SamuelDY* is a framework implemented in the proof-oriented programming language F*, aiming at symbolic analysis of cryptographic protocols on the structural and on the implementation level. In this master's thesis, we analyse three selected authentication and key exchange protocols with DY*: the Otway-Rees protocol, the Yahalom protocol and the Denning-Sacco protocol with public keys. Each of these protocols is designed to establish a secure channel between two users while involving a trusted third party in the authentication process. The Otway-Rees and Yahalom protocols rely on pre-shared symmetric keys with this trusted third party, while the Denning-Sacco protocol relies on digital signatures and public key encryption. In addition, the Denning-Sacco protocol proposes the use of timestamps in messages to provide users with guarantees about the timeliness of the conversation, a protocol feature that has not yet been attempted to be modeled and analyzed in DY*. We developed accurate models for each of the three protocols in DY*, documented possible attacks and proposed improvements to prevent them, and finally proved the security of the protocol or its improved version. We found several attacks on the Otway-Rees protocol that allow an adversary to impersonate one or possibly both of the users involved in the protocol, and based on these attacks, presented improvements to prevent them. For the Yahalom protocol, we show that it satisfies security goals derived from its formal specification, and draw parallels to other approaches with similar results. We also comment on the differences between our results and those of other analyses that describe the Yahalom protocol as flawed. Moreover, we developed an extension to DY* for modeling time-based properties of protocols with timestamps and demonstrated it on the Denning-Sacco protocol. As a result, we provide the first symbolic security proof, including timestamp-dependent security properties, of the Denning-Sacco protocol in DY*.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 Das Leftover Hash Lemma und seine Anwendung in der Kryptographie(2023) Gutknecht, LeonDas Leftover Hash Lemma ist ein in verschiedenen Bereichen der Kryptographie verwendeter Hilfsatz, welcher eine Aussage über den durch Anwendung universeller Hashfamilie erzeugten Quasizufall trifft. Diese Arbeit verwendet eine allgemeine Formulierung des Leftover Hash Lemmas für universelle Hashfamilien mit einer maximalen Kollisionswahrscheinlichkeit 𝛿, welche in verschiedenen Anwendungen eingebracht werden kann. Es werden alle nötigen mathematischen Grundlagen dargelegt, um eine in sich geschlossene Darstellung des Themas zu ermöglichen. Daraufhin wird das Leftover Hash Lemma bewiesen und explizit in zwei verschiedenen Kontexten angewandt. Die erste Anwendung beschäftigt sich mit der Privacy Amplification beim Austausch eines symmetrischen Schlüssels. Das betrachtete Szenario wird genau beschrieben und anhand der gegebenen Entropien wird mithilfe des Leftover Hash Lemmas argumentiert, dass ein Angreifer nur exponentiell kleine Information über den geheimen Schlüssel besitzt. Als weitere Anwendung wird das gitterbasierte Regev-Kryptosystem betrachtet. Dieses wird definiert und seine Korrektheit gezeigt. Um schließlich die Sicherheit des Kryptosystems zu beweisen, wird eine Reduktion auf das Decisional Learning With Errors-Problem durchgeführt, welche eine Verwendung des Leftover Hash Lemmas beinhaltet.Item Open Access Efficient federated learning for gaze estimation(2023) Kittelberger, JonasGaze estimation is the task of deciding for given face images, in which direction people are looking. It is particularly useful for various applications including psychological analysis, authentication, and eye tracking in the context of virtual or augmented reality. To reduce the error of the predictions of gaze estimators, the training data should be collected from a large number of users to ensure the ability of the model to generalize correctly during the inference phase. However, the large data collection requirements conflict with privacy concerns. Building on existing federated learning approaches, this project aims to increase the efficiency of the training process. Hence, (i) we split the model into a part owned by the client and another part owned by a server. This results in strong data protection properties as well as model privacy. In addition, only a part of the model has to be stored and run by each client leading to decreasing computational effort for the typically substantially resource-constrained clients. (ii) We further train the gaze estimation model in an unsupervised fashion and (iii) prune the model weights to enhance the training efficiency. Furthermore, we extend our approach with several privacy-preserving techniques, e.g. Multi-Party Computation (MPC) and Differential Privacy (DP) mechanisms. We empirically demonstrate the effectiveness of these mechanisms with an implemented attack on our system. Our experiments show that our implemented system manages to predict gaze angles with an average deviation of less than 6.5 degrees from the actual angle in about 10 minutes and thus outperforms other privacy-preserving gaze estimators.