Formal Security Analysis of the OpenID FAPI 2.0: Accompanying a Standardization Process

Pedram Hosseyni; Ralf Kuesters; Tim Würtele

Paper 2024/078

Formal Security Analysis of the OpenID FAPI 2.0: Accompanying a Standardization Process

Pedram Hosseyni

, University of Stuttgart, Germany

Ralf Kuesters

, University of Stuttgart, Germany

Tim Würtele

, University of Stuttgart, Germany

Abstract

In recent years, the number of third-party services that can access highly-sensitive data has increased steadily, e.g., in the financial sector, in eGovernment applications, or in high-assurance identity services. Protocols that enable this access must provide strong security guarantees. A prominent and widely employed protocol for this purpose is the OpenID Foundation's FAPI protocol. The FAPI protocol is already in widespread use, e.g., as part of the UK's Open Banking standards and Brazil's Open Banking Initiative as well as outside of the financial sector, for instance, as part of the Australian government's Consumer Data Rights standards. Based on lessons learned from FAPI 1.0, the OpenID Foundation has developed a completely new protocol, called FAPI 2.0. The specifications of FAPI 2.0 include a concrete set of security goals and attacker models under which the protocol aims to be secure. Following an invitation from the OpenID Foundation's FAPI Working Group (FAPI WG), we have accompanied the standardization process of the FAPI 2.0 protocol by an in-depth formal security analysis. In this paper, we report on our analysis and findings. Our analysis incorporates the first formal model of the FAPI 2.0 protocol and is based on a detailed model of the web infrastructure, the Web Infrastructure Model, originally proposed by Fett, Küsters, and Schmitz. Our analysis has uncovered several types of attacks on the protocol, violating the aforementioned security goals set by the FAPI WG. We subsequently have worked with the FAPI WG to fix the protocol, resulting in several changes to the specifications. After adapting our model to the changed specifications, we have proved the security properties to hold under the strong attacker model defined by the FAPI WG.

Note: This is a full version of a paper published at CSF 2024 with extended material.

Metadata

Available format(s): PDF
Category: Cryptographic protocols
Publication info: Published elsewhere. Major revision. CSF 2024
Keywords: authorization protocols formal security analysis web security
Contact author(s): pedram hosseyni @ sec uni-stuttgart de
ralf kuesters @ sec uni-stuttgart de
tim wuertele @ sec uni-stuttgart de
History: 2024-01-19: approved; 2024-01-17: received; See all versions
Short URL: https://ia.cr/2024/078
License: CC BY-SA

BibTeX

@misc{cryptoeprint:2024/078,
      author = {Pedram Hosseyni and Ralf Kuesters and Tim Würtele},
      title = {Formal Security Analysis of the OpenID FAPI 2.0: Accompanying a Standardization Process},
      howpublished = {Cryptology ePrint Archive, Paper 2024/078},
      year = {2024},
      note = {\url{https://eprint.iacr.org/2024/078}},
      url = {https://eprint.iacr.org/2024/078}
}