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

Pedram Hosseyni; Ralf Küsters; Tim Würtele

Paper 2024/1540

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

Pedram Hosseyni

, University of Stuttgart

Ralf Küsters

, University of Stuttgart

Tim Würtele

, University of Stuttgart

Abstract

FAPI 2.0 is a suite of Web protocols developed by the OpenID Foundation's FAPI Working Group (FAPI WG) for third-party data sharing and digital identity in high-risk environments. Even though the specifications are not completely finished, several important entities have started to adopt the FAPI 2.0 protocols, including Norway's national HelseID, Australia's Consumer Data Standards, as well as private companies like Authlete and Australia-based connectID; the predecessor FAPI 1.0 is in widespread use with millions of users. The FAPI WG asked us to accompany the standardization of the FAPI 2.0 protocols with a formal security analysis to proactively identify vulnerabilities before widespread deployment and to provide formal security guarantees for the standards. In this paper, we report on our analysis and findings. Our analysis is based on a detailed model of the Web infrastructure, the so-called Web Infrastructure Model (WIM), which we extend to be able to carry out our analysis of the FAPI 2.0 protocols including important extensions like FAPI-CIBA. Based on the (extended) WIM and formalizations of the security goals and attacker model laid out in the FAPI 2.0 specifications, we provide a formal model of the protocols and carry out a formal security analysis, revealing several attacks. We have worked with the FAPI WG to fix the protocols, resulting in several amendments to the specifications. With these changes in place, we have adjusted our protocol model and formally proved that the security properties hold true under the strong attacker model defined by the FAPI WG.

Note: This is a full version of a paper published in ACM TOPS with extended material.

Metadata

Available format(s): PDF
Category: Cryptographic protocols
Publication info: Published elsewhere. Major revision. ACM Transactions on Privacy and Security
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-10-04: approved; 2024-10-02: received; See all versions
Short URL: https://ia.cr/2024/1540
License: CC BY-SA

BibTeX

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