[Openid-specs-fapi] Security Analysis of FAPI

[Daniel Fett]

All,

Pedram, Ralf, and I have worked on analyzing the security of the FAPI
profiles using formal methods.

The "executive summary" of our findings is that we have found some
attacks when specific, relatively strong attacker models are used. (From
our point of view, it would be very useful to make the attacker model in
the FAPI more explicit, see Issue #175 [1].) Apart from that, we were
able to prove the security of FAPI when certain fixes are applied.

This makes FAPI the only Open Banking security profile with proven security!

We have communicated details of the attacks we found to the authors
listed in the draft over the last months. We will now also follow up
with filing more specific Bitbucket Issues for mitigations that are not
in the spec yet.

Our research paper based on the analysis will be published at Security
and Privacy in May. A preprint version is now available at [2].

-Daniel

[1]
https://bitbucket.org/openid/fapi/issues/175/clarify-attacker-model-pkce-method-and
[2] https://arxiv.org/abs/1901.11520

An Extensive Formal Security Analysis of the OpenID Financial-grade API

Daniel Fett (yes.com AG), Pedram Hosseyni (University of Stuttgart),
Ralf Küsters (University of Stuttgart)


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 develop-
ment 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 analy-
sis 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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.openid.net/pipermail/openid-specs-fapi/attachments/20190201/498d85ea/attachment.html>