  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.
  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.
  In this paper, we perform a rigorous, systematic formal analysis of the
security of the FAPI, based on the Web Infrastructure Model (WIM) proposed by
Fett, Kuesters, and Schmitz. To this end, we first develop a precise model of
the FAPI in the WIM, including different profiles and combinations of security
features. 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.
  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.
  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.
