<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body dir="auto">
<br>
<br>
<div id="AppleMailSignature" dir="ltr">Don Thibeau
<div>Executive Director </div>
<div>The OpenID Foundation </div>
<div>
<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;">
<span style="font-size: 12pt;"><a href="http://openid.net/">http://openid.net/</a></span></p>
</div>
</div>
<div dir="ltr"><br>
On Feb 1, 2019, at 2:33 PM, Daniel Fett via Openid-specs-fapi <<a href="mailto:openid-specs-fapi@lists.openid.net">openid-specs-fapi@lists.openid.net</a>> wrote:<br>
<br>
</div>
<blockquote type="cite">
<div dir="ltr">
<p>All,<br>
<br>
Pedram, Ralf, and I have worked on analyzing the security of the FAPI profiles using formal methods.<br>
<br>
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.</p>
<p>This makes FAPI the only Open Banking security profile with proven security!<br>
</p>
<p>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.<br>
<br>
Our research paper based on the analysis will be published at Security and Privacy in May. A preprint version is now available at [2].<br>
<br>
-Daniel<br>
<br>
[1] <a class="moz-txt-link-freetext" href="https://bitbucket.org/openid/fapi/issues/175/clarify-attacker-model-pkce-method-and">
https://bitbucket.org/openid/fapi/issues/175/clarify-attacker-model-pkce-method-and</a><br>
[2] <a class="moz-txt-link-freetext" href="https://arxiv.org/abs/1901.11520">https://arxiv.org/abs/1901.11520</a></p>
<p>An Extensive Formal Security Analysis of the OpenID Financial-grade API<br>
</p>
<p>Daniel Fett (<a href="http://yes.com">yes.com</a> AG), Pedram Hosseyni (University of Stuttgart), Ralf Küsters (University of Stuttgart)<br>
</p>
<p><br>
Abstract:</p>
<p>Forced by regulations and industry demand, banks<br>
worldwide are working to open their customers’ online banking<br>
accounts to third-party services via web-based APIs. By using<br>
these so-called Open Banking APIs, third-party companies, such<br>
as FinTechs, are able to read information about and initiate<br>
payments from their users’ bank accounts. Such access to<br>
financial data and resources needs to meet particularly high<br>
security requirements to protect customers.</p>
<p>One of the most promising standards in this segment is the<br>
OpenID Financial-grade API (FAPI), currently under develop-<br>
ment in an open process by the OpenID Foundation and backed<br>
by large industry partners. The FAPI is a profile of OAuth 2.0<br>
designed for high-risk scenarios and aiming to be secure against<br>
very strong attackers. To achieve this level of security, the FAPI<br>
employs a range of mechanisms that have been developed to<br>
harden OAuth 2.0, such as Code and Token Binding (including<br>
mTLS and OAUTB), JWS Client Assertions, and Proof Key for<br>
Code Exchange.</p>
<p>In this paper, we perform a rigorous, systematic formal analy-<br>
sis of the security of the FAPI, based on an existing comprehensive<br>
model of the web infrastructure—the Web Infrastructure Model<br>
(WIM) proposed by Fett, Küsters, and Schmitz. To this end, we<br>
first develop a precise model of the FAPI in the WIM, including<br>
different profiles for read-only and read-write access, different<br>
flows, different types of clients, and different combinations of<br>
security features, capturing the complex interactions in a web-<br>
based environment. We then use our model of the FAPI to<br>
precisely define central security properties. In an attempt to<br>
prove these properties, we uncover partly severe attacks, breaking<br>
authentication, authorization, and session integrity properties.<br>
We develop mitigations against these attacks and finally are able<br>
to formally prove the security of a fixed version of the FAPI.</p>
<p>Although financial applications are high-stakes environments,<br>
this work is the first to formally analyze and, importantly, verify<br>
an Open Banking security profile.</p>
<p>By itself, this analysis is an important contribution to the<br>
development of the FAPI since it helps to define exact security<br>
properties and attacker models, and to avoid severe security risks<br>
before the first implementations of the standard go live.</p>
<p>Of independent interest, we also uncover weaknesses in the<br>
aforementioned security mechanisms for hardening OAuth 2.0.<br>
We illustrate that these mechanisms do not necessarily achieve<br>
the security properties they have been designed for.<br>
<br>
</p>
</div>
</blockquote>
<blockquote type="cite">
<div dir="ltr"><span>_______________________________________________</span><br>
<span>Openid-specs-fapi mailing list</span><br>
<span><a href="mailto:Openid-specs-fapi@lists.openid.net">Openid-specs-fapi@lists.openid.net</a></span><br>
<span><a href="http://lists.openid.net/mailman/listinfo/openid-specs-fapi">http://lists.openid.net/mailman/listinfo/openid-specs-fapi</a></span><br>
</div>
</blockquote>
</body>
</html>