Guest Blog: Formal Analysis of the OpenID Financial-grade API
Published March 27, 2019
Guest blog post by Daniel Fett (yes.com), Pedram Hosseyni, and Ralf Küsters (University of Stuttgart).
The security of a web protocol is crucial, especially in the domain of financial applications and in other high-stakes environments. For identifying weaknesses in protocols and ensuring security, formal protocol analysis is the state-of-the-art method.
The OpenID Financial-grade API (FAPI) is based on the OAuth 2.0 protocol, which we verified formally in previous work (http://arxiv.org/abs/1601.01229). To ensure a high degree of security for the FAPI, the OpenID Foundation approached us to perform a similar formal security analysis of the protocol flows of the FAPI.
In contrast to plain OAuth, the FAPI aims at providing security even if some attacks on the flows are successful, for example, if an attacker manages to phish an access token or obtain requests and responses of a flow in which an honest user is involved.
To achieve such a high level of security, the FAPI incorporates several new security mechanisms. These extensions aim at increasing the security of the protocol, but the question arises whether they actually fulfill this purpose, or if maybe the opposite happens, and corner cases arise in which a combination of new features breaks the security of the whole protocol.
Finding such corner cases is the showcase discipline of formal analysis. We can use it to examine all flows and options in the protocol at the same time and thus find problematic settings that may evade a thorough expert review. In a nutshell, formal protocol analysis works as follows:
Formal Protocol Analysis
The first step is to create a model of the protocol that is to be analyzed. In our work, this model is based on a comprehensive model of the web created at the Institute of Information Security at the University of Stuttgart. This step leads to a compact yet detailed and precise description of the protocol, which is particularly important for protocols that draw from many specifications.
The second step is to define the security properties. For example, in case of the FAPI, it is intuitively clear that an attacker should not gain access to the financial account of a customer. But what exactly does this mean? And under which conditions should this property be guaranteed by the protocol? At this point, the formal model is used to turn the intuition into concrete and precise statements.
The third and last step is the proof of the security properties. The goal of this step is to prove that the properties that were defined hold true for the model. Therefore, if the proof is done correctly, there exists no protocol flow in which the properties are violated; hence, the absence of attacks can be shown in the model.
But what happens if the protocol contains vulnerabilities? In this case, the statement that the model fulfills the security properties is not true, and therefore, the correctness of the statement cannot be proven.
For the attacks discovered during the analysis, the mitigations can often be found with the aid of the proof (which at this stage is not yet complete).
After fixing all vulnerabilities, the proof can be finished, showing that no attack is possible in the formal model of the protocol.
Analysis of the FAPI
For the formal analysis of the FAPI, we modeled both the Read-Only and the Read-Write profiles. We created a model of the FAPI containing all participants, i.e., with clients, authorization servers, and resource servers. Other participants, like browsers and the network, are already defined by the underlying web model.
Within the model, we tried to capture the behavior of the participants as precisely as possible. As a result, our model does not only cover the underlying OAuth flow but also several extensions: Proof Key for Code Exchange (PKCE), OAuth 2.0 Token Binding, OAuth 2.0 Mutual TLS, and the recently developed JWT Secured Authorization Response Mode (JARM).
Regarding the security properties, we consider the FAPI to be secure if the following properties hold true:
- Authorization, which means that an attacker should not be able to get read-only or read-write access to the resources of an honest user,
- Authentication, which means that an attacker should not be able to log in (at a client) with the identity of an honest user, and
- Session Integrity, which means that an honest user should never be logged in with the account of an attacker or use the resources of an attacker.
