Universität Stuttgart

Permanent URI for this communityhttps://elib.uni-stuttgart.de/handle/11682/1

Browse

Search Results

Now showing 1 - 10 of 30

Open Access
Beschreibung und Analyse der W3C Browser Push APIs
(2024) Lüers, Alina
Die W3C Push API bietet die Möglichkeit der asynchronen Kommunikation zwischen einem Browser und einem Anwendungsserver. Der Anwendungsserver kann Push Nachrichten an einen Push Service senden. Der Push Service speichert die Nachricht bis der Browser erreichbar ist oder die Nachricht verfällt. Wenn der Browser die Push Nachricht erhält, wird die Push Nachricht an den Service Worker weitergeleitet, der die Nachricht verarbeitet und gegebenenfalls dem Nutzer anzeigt. In dieser Arbeit wird die W3C Push API zunächst abstrakt beschrieben und darauf aufbauend eine informelle Sicherheitsanalyse durchgeführt. Dafür werden zunächst die der Analyse zu Grunde liegenden Angreifermodelle und Annahmen definiert. Anschließend werden die Sicherheitsziele Vertraulichkeit, Privacy, Verfügbarkeit, Authentifizierung, Autorisierung und Session Integrität untersucht. In der Analyse konnten dabei keine neuen, gravierenden Sicherheitsprobleme festgestellt werden. Anschließend wird die Implementierung der Push API in Firefox näher betrachtet. Dabei wird der Push Service autopush beschrieben und es werden die zusätzlichen Sicherheitsmaßnahmen aufgezählt.
Open Access
Overview on web authentication and authorization protocol security evaluations
(2025) Schäberle, Victoria
Web authentication and authorization protocols such as OAuth 2.0 and OpenID Connect are widely used and have become established standards in the single sign-on (SSO) ecosystem. They enable users to grant third-party applications access to their resources and to use diverse online services conveniently and securely, while reducing the risks associated with password-based authentication. However, incorrect implementations have repeatedly led to severe vulnerabilities, ranging from token theft to account compromise. These risks highlight the importance of understanding the security properties and weaknesses of these protocols. This thesis investigates the security of OAuth 2.0 and OpenID Connect by providing a structured overview of existing evaluations, considering both foundational and widely cited studies as well as more recent contributions. Both scientific and non-scientific sources are considered, including formal analyses, empirical studies, and protocol specifications. Typical attacks and vulnerabilities are summarized and categorized into four fields, which include formal, empirical, protection-centered, and investigations of specific attacks and mitigations. The review highlights approaches that develop tools for empirical evaluation, focus on mobile applications, or analyze relying parties (RPs) and identity providers (IdPs). The methodology of the empirical studies examined range from active and passive attack strategies to white-box and black-box analyses. By synthesizing these findings, this thesis reveals a persistent gap between the formal security of the protocols and recurring weaknesses in real-world implementations. This gap underscores the need for continued research, clearer developer guidance, and systematic auditing.
Open Access
Mechanized modeling and security proofs for web protocols
(2025) Würtele, Tim; Küsters, Ralf (Prof. Dr.)
The Web plays a central role in modern life - not only for news and social interactions, but also in security-critical applications such as banking and healthcare. Many of these applications rely on standardized protocols, for example, for authentication and authorization. Hence, the security of many applications on the Web depends on the security of these protocols. Studying the security of protocols - not just on the Web - has been an active area of research for over four decades. An important branch of this research focuses on applying formal methods to obtain rigorous, formally proven security guarantees. However, in the context of Web protocols, the complexity of the underlying infrastructure - with multiple layers of sub-protocols and intricate interactions between involved parties (e.g., in-browser communication between websites) - poses significant challenges for such analyses. Yet this complexity must be captured, since even subtle design details may have security implications, as demonstrated by past attacks. This thesis advances the state of the art in Web protocol security analysis in several ways. First, we present a formal security analysis of the FAPI 2.0 protocol family, developed and used in high-risk domains such as banking and healthcare. Our analysis accompanied the development of the FAPI 2.0 protocols and is based on the most comprehensive and detailed security analysis framework for Web protocols to date, the Web Infrastructure Model (WIM) - a pen-and-paper Dolev-Yao-style model that captures many aspects of the Web environment, and in particular, many details of the inner workings of Web browsers. To faithfully model FAPI 2.0, we extend the WIM in several ways, for example, by introducing communication channels for push messaging and support for so-called HTTP Message Signatures. These extensions are derived from relatively recent, yet already established Web standards, and are therefore of independent interest for keeping the WIM up to date. Our analysis - the largest based on the WIM so far - uncovered multiple new attacks that led to fixes in the now-finalized FAPI 2.0 standards, and started an ongoing effort within the standardization body responsible for FAPI 2.0 to apply formal analysis to more and more of their standards. At the same time, this work illustrates the limitations of pen-and-paper proofs: our analysis spans more than 100 pages of hand-written, manually verified proofs. Hence, mechanized verification promises more reliable results, but existing mechanized tools struggle with the level of detail and resulting model size required for realistic Web models. To bridge this gap, we contribute to the development of DY*, a mechanized Dolev-Yao-style protocol analysis framework that supports implementation-level executable models, highly modular proofs over an explicit global trace, an extensible equational theory, and can cope well with unbounded data structures, loops, and recursion. While the long-term goal is to develop DY* into a Web protocol analysis framework - akin to the WIM, but fully mechanized - it has already been used in several nontrivial case studies, including the first formal analysis of the Signal protocol with an unbounded number of ratcheting rounds. Finally, as a first step toward such a mechanized Web protocol analysis framework based on DY*, we use DY* to analyze the immensely popular ACME certificate issuance protocol. In the course of this analysis, we extend DY* with authenticated channels, an enhanced equational theory to more precisely capture the properties of digital signatures, and develop a methodology to execute DY* models against real-world implementations. Our analysis is the first of the final ACME standard and ranks among the most detailed mechanized protocol security analyses to date - our executable model can even interact with real-world servers.
Open Access
MS-RAFT+ : high resolution multi-scale RAFT
(2023) Jahedi, Azin; Luz, Maximilian; Rivinius, Marc; Mehl, Lukas; Bruhn, Andrés
Hierarchical 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 .
Open Access
OpenID for Verifiable Credentials : formal security analysis using the Web Infrastructure Model
(2023) Hauck, Fabian
In 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.
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, Tim
Building 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.
Open Access
Formal modeling and verification of the authentication service exchange of the Kerberos protocol using DY*
(2025) Schaaf, Julius
Authentication is a fundamental challenge in distributed computing. Kerberos Version 5, standardized in RFC 4120, is the dominant enterprise authentication protocol, deeply embedded in organizational infrastructure worldwide. Despite its maturity, Kerberos has not been formally verified in a mechanized framework that connects symbolic reasoning with executable implementations. Previous analyses either operate at high abstraction levels that omit concrete message encodings and state machines, or focus on computational primitives without capturing protocol-level authentication dependencies. To the best of our knowledge no prior work combines symbolic reasoning about explicit protocol state and message structure with verification that corresponds directly to executable code, leaving a gap between abstract guarantees and operational behavior. This thesis presents the first mechanized verification of the Kerberos Authentication Service Exchange in the DY* framework. The Authentication Service Exchange forms the foundational phase of Kerberos, in which the client obtain a Ticket-Granting Ticket from the Key Distribution Center. All later protocol operations depend on the security guarantees established during this exchange. The RFC 4120 specification is translated into executable F* code using DY*’s receive-react methodology. The model defines explicit state machines with concrete message formats, validation logic, and trace-based semantics. Secrecy and authentication properties are formalized as predicates over traces and proven using inductive invariants that capture cryptographic correctness, state consistency, and event ordering under the symbolic Dolev-Yao adversary model. The verification establishes confidentiality of the encrypted reply and ticket parts and mutual authentication between client and Key Distribution Center, holding unless one of the involved principals is corrupted. It maintains fidelity to operational protocol behavior through explicit parsing, detailed state transitions, and concrete timing constraints, while remaining tractable through justified abstractions. This work demonstrates that mechanized verification of real-world authentication protocols within DY* can yield executable, proven models that align with operational specifications. The verified model provides a foundation for extending the formal analysis to the complete Kerberos protocol, including the Ticket-Granting Service exchange, pre-authentication mechanisms, and cross-realm operation.
Open Access
Composable accountability for distributed ledgers
(2024) Graf, Mike; Küsters, Ralf (Prof. Dr.)
Open Access
Formal analysis of web protocols and mechanized security proofs
(2026) Hosseyni, Pedram; Küsters, Ralf (Prof. Dr.)
Cryptographic protocols form the foundation of various real-world technologies, from social logins and secure messaging to financial applications, e-governance, and healthcare. The security of such protocols is clearly essential. The possibilities of an active attacker with the ability to manipulate messages and participate in different protocol runs, potentially mixing up messages between runs, make it infeasible to guarantee the security of protocols through informal argumentation. In contrast, formal methods based on meaningful protocol and attacker models make it possible to consider all potential attacks, ruling out the possibility that an attacker can break the security of the protocol within the bounds of the considered model. The main contributions of this thesis are as follows: Firstly, we accompanied the standardization process of OpenID Federation, an emerging real-world protocol, with a rigorous formal security analysis based on the Web Infrastructure Model, an established symbolic, Dolev-Yao-style model of the Web. OpenID Federation is a complex protocol that deals with trust establishment and the exchange of metadata necessary for running some other application-level protocol. Our analysis revealed three novel attacks, one of which extends beyond the scope of Federation and affects multiple widely used authorization and authentication protocols such as OAuth 2.0 and OpenID Connect. Secondly, we contribute to the field of mechanized symbolic analysis by developing DY⋆, a novel mechanized framework that, for the first time, bridges the gap between two established verification paradigms. DY⋆ enables the scalable verification of large-scale cryptographic protocols and provides a rich set of features, including a verification method that is inherently modular, support for explicit global traces, mutable global state, equational theories, and models that can include implementation-level details. We also propose a verification methodology that facilitates the analysis of protocol stacks within DY⋆ in a composable manner.
Open Access
Efficient federated learning for gaze estimation
(2023) Kittelberger, Jonas
Gaze 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.

Universität Stuttgart

Browse

Filters

Settings

Sort By

Results per page

Search Results