Paper Info
Title
An Extensive Formal Security Analysis of the OpenID Financial-Grade API
Abstract
Forced by regulations and industry demand, banks worldwide are working to open their customers' online banking accounts to third-party services via web-based APIs. By using these so-called Open Banking APIs, third-party companies, such as FinTechs, are able to read information about and initiate payments from their users' bank accounts. Such access to financial data and resources needs to meet particularly high security requirements to protect customers. One of the most promising standards in this segment is the OpenID Financial-grade API (FAPI), currently under development in an open process by the OpenID Foundation and backed by large industry partners. The FAPI is a profile of OAuth 2.0 designed for high-risk scenarios and aiming to be secure against very strong attackers. To achieve this level of security, the FAPI employs a range of mechanisms that have been developed to harden OAuth 2.0, such as Code and Token Binding (including mTLS and OAUTB), JWS Client Assertions, and Proof Key for Code Exchange. In this paper, we perform a rigorous, systematic formal analysis of the security of the FAPI, based on an existing comprehensive model of the web infrastructure - the Web Infrastructure Model (WIM) proposed by Fett, Küsters, and Schmitz. To this end, we first develop a precise model of the FAPI in the WIM, including different profiles for read-only and read-write access, different flows, different types of clients, and different combinations of security features, capturing the complex interactions in a web-based environment. We then use our model of the FAPI to precisely define central security properties. In an attempt to prove these properties, we uncover partly severe attacks, breaking authentication, authorization, and session integrity properties. We develop mitigations against these attacks and finally are able to formally prove the security of a fixed version of the FAPI. Although financial applications are high-stakes environments, this work is the first to formally analyze and, importantly, verify an Open Banking security profile. By itself, this analysis is an important contribution to the development of the FAPI since it helps to define exact security properties and attacker models, and to avoid severe security risks before the first implementations of the standard go live. Of independent interest, we also uncover weaknesses in the aforementioned security mechanisms for hardening OAuth 2.0. We illustrate that these mechanisms do not necessarily achieve the security properties they have been designed for.
Year
DOI
Venue
2019
10.1109/SP.2019.00067
2019 IEEE Symposium on Security and Privacy (SP)
Keywords
Field
DocType
Web-Security,Single-Sign-On,OAuth,Formal-Analysis,Security-Protocols,OpenID-Connect,Financial-grade-API,Open-banking-API
Bank Accounts,Authentication,Computer security,Computer science,Authorization,OpenID,Concrete security,Security analysis,Security properties,Payment
Journal
Volume
ISSN
ISBN
abs/1901.11520
1081-6011
978-1-5386-6661-6
Citations 
PageRank 
References 
3
0.38
0
Authors
3
Name
Order
Citations
PageRank
Daniel Fett1512.96
Pedram Hosseyni251.76
Ralf Küsters3101469.62