05 Fakultät Informatik, Elektrotechnik und Informationstechnik

Permanent URI for this collectionhttps://elib.uni-stuttgart.de/handle/11682/6

Browse

Filters

2018 - 201912020 - 20233

Settings

Institute: search.filters.UBSInstitut.Institut für InformationssicherheitAuthor: search.filters.author.Hosseyni, Pedram

Search Results

Now showing 1 - 4 of 4
  • Thumbnail Image
    ItemOpen 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.
  • Thumbnail Image
    ItemOpen 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, Tim
    The 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.
  • Thumbnail Image
    ItemOpen Access
    Security analysis of the OpenID financial-grade API
    (2018) Hosseyni, Pedram
    The OpenID Financial-grade API provides a mechanism for accessing data and resources that need a high degree of protection, such as in the context of financial applications. As a profile of the OAuth 2.0 Authorization Framework designed for high-risk scenarios, the Financial-grade API aims at being secure even if the procedure is attacked at several points leading to wrongly configured endpoints, the leakage of tokens and even whole requests and responses. To achieve this degree of security, several additional mechanisms are used, which protect against the usage of leaked tokens and protect messages against modification. We modeled both the Read-Only Profile and the Read-Write Profile of the Financial-grade API in the FKS Web Model, including all underlying assumptions that might affect the security of the flows. Through formal analysis, we discovered several attacks not only on mechanisms specific to the Financial-grade API but also on more general concepts of OAuth, namely, Token Binding and the Proof Key for Code Exchange extension. We provide mitigations against these attack scenarios and show that the modified flows are secure as specified by our security definitions. More precisely, these modified flows prevent an attacker from logging in under the identity of an honest user and accessing protected resources belonging to the honest user.
  • Thumbnail Image
    ItemOpen Access
    Layered symbolic security analysis in DY*
    (2023) Bhargavan, Karthikeyan; Bichhawat, Abhishek; Hosseyni, Pedram; Küsters, Ralf; Pruiksma, Klaas; Schmitz, Guido; Waldmann, Clara; Würtele, Tim
    While cryptographic protocols are often analyzed in isolation, they are typically deployed within a stack of protocols, where each layer relies on the security guarantees provided by the protocol layer below it, and in turn provides its own security functionality to the layer above. Formally analyzing the whole stack in one go is infeasible even for semi-automated verification tools, and impossible for pen-and-paper proofs. The DY* protocol verification framework offers a modular and scalable technique that can reason about large protocols, specified as a set of F* modules. However, it does not support the compositional verification of layered protocols since it treats the global security invariants monolithically. In this paper, we extend DY* with a new methodology that allows analysts to modularly analyze each layer in a way that compose to provide security for a protocol stack. Importantly, our technique allows a layer to be replaced by another implementation, without affecting the proofs of other layers. We demonstrate this methodology on two case studies. We also present a verified library of generic authenticated and confidential communication patterns that can be used in future protocol analyses and is of independent interest.