资源描述
Security Analysis of the Open Banking Account and Transaction API Protocol Abdulaziz Almehrej1, Leo Freitas1 and Paolo Modesti2 1 School of Computing, Newcastle University, UK 2 Computer Science and Information Systems, Teesside University, UK Abstract. To counteract the lack of competition and innovation in the nancial services industry, the EU has issued the Second Payment Ser- vices Directive (PSD2) encouraging account servicing payment service providers to share data. The UK, similarly to other European countries, has promoted a standard API for data sharing: the Open Banking Stan- dard. We present a formal security analysis of its APIs, focusing on the correctness of the Account and Transaction API protocol. The work re- lies on a previously proposed methodology, which provided a practical approach to protocol modelling and veri cation. 1 Introduction The lack of competition in the nancial services industry has been one of the main factors that led the European Union to introduce the second version of the Payment Services Directive (PSD2) 27, which aims to improve competition by enabling and encouraging bank account holders to share, in a controlled and secure way, their account data. This approach, along with economic opportuni- ties, has clearly also important privacy and security implications that must be carefully considered when building systems allowing data sharing on such scale. To provide a standard API for the sharing of customer data across di er- ent banks, the UK, similarly to other European countries, introduced the Open Banking Standard 24. The regulation encompasses several API speci cations suitable for di erent Third Party Providers (TPPs) who aim to service con- sumers that consent to sharing their data. The adoption of a standardised in- terface allows interoperability and simpli es the implementation of systems for sharing data between banks and TPPs. In such context, it is clear that formally validating complex software systems, like the one covered in the present work, that can a ected by design error and implementation bugs, is of upmost importance to ensure that the system behaves correctly with respect to the speci cation and a number of desirable properties. Contribution In this paper, we present a formal security analysis of the Open Banking Standard APIs, focusing on the veri cation of the correctness of the Account and Transaction API protocol. The work relies on a previously proposed methodology 8 which provided a practical approach to protocol modelling and 2 Abdulaziz Almehrej, Leo Freitas and Paolo Modesti veri cation. The methodology utilises the Alice and Bob notation (AnB) 12 to specify a formal model of the protocol that can be formally veri ed with the OFMC model checker3, which has been used to model and verify a signi cant number of security protocols, for example a projects like AVANTSSAR 2. We formalised and veri ed a number of security goals that are implicit in the requirements. Although most goals were satis ed in our analysis, the lack of rigourous de nition of security properties in the standard can be a source of ambiguity, potentially leading to di erent interpretation of the security re- quirements in the implementation. Moreover, the standard seems to rely on a number of current web technologies that could potentially become obsolete to future technological and security needs. To the best of our knowledge, our formal model represents the rst attempt to formally analyse Open Banking protocols. Recently, other authors 10 made an evaluation of the integration of a web application with the Danish Nordeas Open Banking APIs considering the security threats of the underlining technology, in light of OWASP Top 10 Web Application Security Risks list. However, they did not analyse the security of Open Banking itself considering and assessing security goals as we did. Therefore, we believe a formal analysis can be valuable for stakeholders considering the adoption of a standard that can have a signi cant and long impact on the e ciency and security of the nancial sector. 2 Background 2.1 The Open Banking Standard Overview The Payment Services Directive (PSD) is a European legislation, which aims to improve payment services across the EU in terms of safety and innovation 6. The rst version of PSD was adopted in 2007 26, but as the digitalisation of the economy progressed, and new payment services appeared, it became outdated and insu cient to ensure the provision of consumer protection and adequate competition. Therefore, a revised version was adopted in November 2015 in an attempt to: Ensure that all payment service providers have equal operating conditions; Expand the market for new means of payment; Ensure the security of consumers using the payment services 27. To deliver the standard, the Open Banking Implementation Entity was es- tablished in 2016 by the UK Competition and Markets Authority (CMA) 17. The Open Banking Working Group (OBWG) published a report on the Open Banking Standard 24, in which they outlined two key outcomes: An open API for sharing data regarding the services o ered by Account Servicing Payment Service Providers (ASPSPs), e.g. banks; An open API for sharing the account data of Payment Service Users (PSUs) provided by ASPSPs. Security Analysis of the Open Banking ATP 3 Open Banking is not only concerned about the API endpoints (e.g. location of resources accessible by third parties, such as developers, to build banking and nancial applications), but also about data and security standards. The data standard provides data models to the API data format. The API standard covers the APIs operational requirements. The security standard covers API security requirements. The Open Banking Standard has been released in phases with the latest in September 2018 20. By October 2019, the standard has been adopted by 65 regulated ASPSPs with 123 TPPs providing services 19. This illustrates the signi cance Open Banking has on the nancial services industry and thereby the importance of verifying its standards correctness. 2.2 Account Information Service Provider (AISP) The Account and Transaction API protocol (ATP) ow 18, which allows AISPs access to the PSUs account data, is shown in Figure 1. An AISP is a regulated entity allowed by ASPSPs to access a PSUs account data if the PSU provides their consent. This type of access is read-only as the AISPs are not expected to directly a ect the payment accounts they are allowed access to. An AISP can then provide di erent services having the PSUs account and transaction data, including applications that provide a user-friendly view of the states of the di erent payment accounts held by the PSU, budgeting advice, price comparisons and product recommendations. Fig.1. The Account and Transaction API protocol high-level ow (adapted from 18) The protocol is initiated with the PSU asking for information regarding their payment account(s) from an AISP (Step 1). The AISP then attempts to create 4 Abdulaziz Almehrej, Leo Freitas and Paolo Modesti an account access consent with the corresponding ASPSP, based on the access permissions agreed upon with the PSU. First, the AISP authenticates itself to the ASPSP through a client credential grant, which is an approach for machine- to-machine authentication. The ASPSP then provides the AISP with an access token used to request the creation of the consent resource (Step 2). At this point, the created account access consent has to be authorised to be used by the AISP to access the PSUs account data. This requires the PSUs to authenticate them- selves to the ASPSP, followed by authorising the consent. During this phase, the PSU has to select the payment accounts(s) for which the chosen permissions should apply. The AISP then obtains an access token to the account data (Step 3). With this token, the AISP has to rst retrieve the accessible accounts, in- cluding their unique IDs, through the accounts endpoint. The IDs can later be used to request the data of speci c accounts (Step 4). To retrieve speci c PSU account data (e.g. balances, transactions, direct debits, bene ciaries, etc.) the AISP will have to request the data via the appropriate link using the correct endpoint and method from the ASPSP. 2.3 Methodology and Speci cation Language The formal veri cation of Open Banking API presented in this work is based on a protocol veri cation methodology proposed in 8. The methodology utilises the Alice and Bob notation (AnB) 12 to specify a formal model of the protocol that can be formally veri ed through information ow (secrecy and authenticity) goals. Such notation abstracts from implementation details, but allows formal representation and analysis of the security-relevant characteristics of protocols. An AnB speci cation comprises of several sections. The Types section de- clares the di erent identi ers used in the protocol. This includes the agents, constant and variable (random) numbers and transparent functions. Transpar- ent functions are user-de ned through their signature, thereby abstracting from their implementation details (i.e. they are uninterpreted). The Knowledge sec- tion describes the initial data each agent has before running the protocol. Fresh values, The information ow is described in the Actions section, where details about messages exchanged by agents are speci ed. Furthermore, the model can be used to verify speci c security properties, such as (weak and strong) authen- tication and secrecy goals: A weakly authenticates B on M: agent A has evidence that the message M has been endorsed by agent B with the intention to send it to A (i.e. non-injective agreement 11); A authenticates B on M: weak authentication plus evidence of the fresh- ness of the message M (i.e injective agreement 11); M secret between A, B: message M is kept secret among listed agents. The formal model captures the protocol requirements 22. While the Open Banking API describes in details the information- ow, it lacks de nitions of security goals that the exchanges between agents are meant to convey. Therefore, part of our work consisted in identifying suitable goals for the protocol model. Security Analysis of the Open Banking ATP 5 For the veri cation, we used the Open-Source Fixed-Point Model-Checker (OFMC) 13, a symbolic model-checker supporting the AnB notation. Moreover, the AnBx Compiler and Code Generator 15 was used to pre-process the model to bene t from a stricter type system and support the extension to AnB that allows named expression abstractions (De nitions section). 3 Implementation We de ne an AnBx model of the Account and Transaction API protocol (ATP) 18 to analyse and verify its information ow accurately. We abstract from, and do not directly specify dependant technologies like OAuth 2.0 9, which are de ned in the Open Banking Security pro le 21. Con dential messages are exchanged over the internet. Therefore, the spec- i cation 23 mandates the use of Transport Layer Security (TLS) between all parties, as in the Financial API speci cation 25. Verifying TLS is not our fo- cus: we assume its security guarantees by partially simulating TLS with con den- tial and authentic communication using AnB bullet channels 14. For example, *-* represents a secure channel (authenticated and con dential) and can be used as a suitable abstraction for TLS with mutual authentication 14. We abstract from signing exchanged payloads too. Our objective is to model the weakest version the speci cation allows for as it is likely to be the most vulnerable. Consequently, as the additional layer of encryption is optional, we do not cover it in the model, and may be part of future work. To help explain the model, a sequence diagram containing AnBx action labels is given in Figure 2. We describe each of the AnBx model sections next. Roles and Responsibilities There are four agents that participate in the protocol. The PSU initiates the protocol aiming to grant an AISP limited access to their account data. The AISP aims to obtain access to the PSUs account data to provide the user with a service. The ASPSP has two separate roles: the authorisation server (aspspA), authenticating AISPs and PSUs to generate tokens that enable AISPs access to endpoints; and the resource server (aspspR), maintaining resources like consents and PSU account data. By observing the responsibilities of each agent, the authorisation and resource servers must be trusted parties: if any of them acts maliciously, the protocol can be trivially broken. Trusted agents in AnB are represented by identi ers beginning with a lower-case letter. Agent PSU, AISP, aspspA, aspspR; Initial Knowledge The PSU and AISP know each other given that before protocol execution, the PSU has been in contact with the AISP to exchange permissions and to inform 6 Abdulaziz Almehrej, Leo Freitas and Paolo Modesti Fig.2. Model sequence diagram of the ASPSP of contact intent. The AISP is assumed to identify the ASPSPs corresponding authorisation and resource servers. Thus, the AISP knows the identities of both servers. The authorisation and resource servers are known to each other and their identities are also known by the PSU. Knowledge: PSU : PSU, AISP, aspspA, aspspR, fPSUSecret(PSU); AISP: AISP, PSU, aspspA, aspspR, fAISPSecret(AISP); aspspA: aspspA, aspspR, fPSUSecret, fAISPSecret, fAuthCode, fClientCredToken, fAuthCodeToken; aspspR: aspspR, aspspA, fGetIntent, fCreateIntent, fFetchAccounts,fAuthoriseIntent,fAccountsEndpoint; Security Analysis of the Open Banking ATP 7 where PSU!=AISP,PSU!=aspspA,PSU!=aspspR PSU/AISP. Authentication requires the PSU and AISP to share a secret with the authorisation server. This secret is known a priori as represented by trans- parent function calls fPSUSecret(PSU) and fAISPSecret(AISP), which allows us to abstract from the secret agreement mechanism. Authorisation and Resource Servers. The authorisation server performs numerous state-changing operations over the protocol execution through trans- parent functions: fClientCredToken generates a token acquired through a client credential grant; fAuthCode generates an authorisation code; and fAuthCodeToken generates a token acquired through the authorisation code. The authorisation server is also aware of its PSU and AISP secrets in order to authenticate them. The resource server performs state-changing operations through transparent functions: fCreateIntent and fGetIntent to create and retrieve a consent resource, respectively; fFetchAccounts retrieves a list of all PSU accounts; fAuthoriseIntent updates consent authorisation; and fAccountsEndpoint returns PSU account data. Roles Restriction. To make our model more realistic, we impose restrictions about the role performed by di erent agents. To declare which agent is not allowed to act as another agent, we can use the where keyword at the end of the Knowledge section. For example, the PSU cannot act as the AISP, which is unrealist
展开阅读全文