key: cord-0043696-b9xdsy6z authors: Almehrej, Abdulaziz; Freitas, Leo; Modesti, Paolo title: Account and Transaction Protocol of the Open Banking Standard date: 2020-04-22 journal: Rigorous State-Based Methods DOI: 10.1007/978-3-030-48077-6_16 sha: 797704bfadebfea8255348ac63b829ecc4c07e11 doc_id: 43696 cord_uid: b9xdsy6z To counteract the lack of competition and innovation in the financial services industry, the EU has issued the Second Payment Services 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 Standard. We present an overview of the results of a formal security analysis of the Account and Transaction API protocol. The lack of competition in the financial 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) [14] , which aims to improve competition by enabling and encouraging bank account holders to share, in a controlled and secure way, their account data. To provide a standard API for the sharing of customer data across different banks, the UK, similarly to other European countries, introduced the Open Banking Standard [13] . The regulation encompasses several API specifications suitable for different Third Party Providers (TPPs) who aim to service consumers that consent to sharing their data. The adoption of a standardised interface allows interoperability and simplifies the implementation of systems for sharing data between banks and TPPs. Contribution. In this paper, we present an overview of a formal security analysis of the Open Banking Standard APIs, focusing on the verification of the correctness of the Account and Transaction API protocol. The work relies on a previously proposed methodology [5] which provided a practical approach to protocol modelling and verification. The methodology utilises the Alice and Bob notation (AnB) [9] to specify a formal model of the protocol that can be formally verified with the OFMC model checker [2] . We formalised and verified a number of security goals that are implicit in the requirements. Although most goals were satisfied in our analysis, the lack of rigourous definition of security properties in the standard can be a source of ambiguity, potentially leading to different interpretations of the security requirements in the implementation. To the best of our knowledge, our model, fully presented in [1] , is the first attempt to formally analyse Open Banking protocols. Recently, other authors [7] made an evaluation of the integration of a web application with the Danish Nordea's Open Banking APIs considering the security threats of the underlying 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 this formal analysis can be valuable for stakeholders considering the adoption of a standard that can have a significant and long impact on the efficiency and security of the financial sector. The Open Banking Standard [13] aims at two key outcomes. The first one is an open API for sharing data regarding the services offered by Account Servicing Payment Service Providers (ASPSPs), e.g. banks. The other one is an open API for sharing the account data of Payment Service Users (PSUs) provided by ASPSPs. 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 financial applications), but also about data and security standards. The data standard provides data models to the API data format. The API standard covers the API's operational requirements. The security standard covers API security requirements. An Account Information Service Provider (AISP) is a regulated entity allowed by ASPSPs to access a PSU's account data if the PSU provides their consent. This type of access is read-only as the AISPs are not expected to directly affect the payment accounts they are allowed access to. An AISP can then provide different services having the PSU's account and transaction data, including applications that provide a user-friendly view of the states of the different payment accounts held by the PSU, budgeting advice, price comparisons and product recommendations. Account and Transaction Protocol. 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 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 PSU's account data. This requires the PSUs to authenticate themselves to the ASPSP, followed by authorising the consent. During this phase, the PSU has to select the payment account(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 first retrieve the accessible accounts, including their unique IDs, through the accounts endpoint. The IDs can later be used to request the data of specific accounts (Step 4). To retrieve specific PSU account data (e.g. balances, transactions, direct debits, beneficiaries, etc.) the AISP will have to request the data via the appropriate link using the correct endpoint and method from the ASPSP. The formal verification of Open Banking API presented in this work is based on a protocol verification methodology proposed in [5] . The methodology utilises the Alice and Bob notation (AnB) [9] to specify a formal model of the protocol that can be formally verified through information flow (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 specification comprises of several sections. The Types section declares the different identifiers used in the protocol. This includes the agents, constant and variable (random) numbers and transparent functions. Transparent functions are user-defined through their signature, thereby abstracting from their implementation details (i.e. they are uninterpreted). The Knowledge section describes the initial data each agent has before running the protocol. Fresh values are initialised at runtime. The information flow is described in the Actions section, where details about messages exchanged by agents are specified. Furthermore, the model can be used to verify specific security properties, such as (weak and strong) authentication and secrecy goals: The formal model captures the protocol requirements [12] . While the Open Banking API describes in details the information-flow, it lacks definitions 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. For the verification, we used the Open-Source Fixed-Point Model-Checker (OFMC) [10] , a symbolic model-checker supporting the AnB notation. Moreover, the AnBx Compiler and Code Generator [11] was used to pre-process the model to benefit from a stricter type system and support the extension to AnB that allows named expression abstractions (Definitions section). The goals we identified (and verified) are based on our understanding of the protocol and on its dependencies. For example, OAuth 2.0 security considerations [6, pp. 52-60], protocol use cases in [13, pp. 20-23] and our expectations of the protocol. We identified eight goals: four on message secrecy, and four on authentication. Two goals (G1 and G2) are obvious: the exchanged secrets/credentials between the AISP and PSU and the authorisation server remain secret whilst requesting for a client token (Action 2.1 in the specification) and acquiring consent authorisation (A3. The authentication goals relate to the PSU authenticating the consent resource to authorise (G4), the resource server authenticating the PSU's selected accounts information (G5) and the AISP authenticating the PSU's account information from the resource server (G8). This last goal between the AISP and the resource server is crucial in verifying the integrity of the account data sent to the AISP by the resource server. In addition to direct data modification, it is important to verify that old data cannot be replayed. For instance, in the case of affordability check, if the PSU was an intruder and modified the data, they could trick an AISP into providing a product they are not eligible for. This goal also enforces fraud detection: if the transactional data can be modified by an intruder to hide fraudulent activity. Given the redirections from the PSU to the authorisation server and AISP (A3. 1.1 and A3.3.1-A3.3.2) , we weakly authenticate that those endpoints cannot be modified by an intruder to help avoid redirected URI manipulation [6, Sect. 10.6] and phishing attacks [6, Sect. 10.11] (G6). Model Development. The Open Banking ATP is complex and with multiple dependencies. The AnB model aims to provide an abstract and accurate view of its essential aspects and to verify key properties. The initial AnB model was overly detailed with unnecessary data exchanges. To reach the right level of abstraction, we then decided to first determine the protocol goals prior to abstracting. Even after such endevour, verification was unwieldy: it ran for over two days without response. As is common within model checking problems, state explosion must be tackled beyond abstracting details, abstract on irrelevant data. Restricting the role of the PSU, where it had to be different from the AISP and servers, considerably reduced the state space. This led to termination with goal verification to be reduced to about seven hours. This enabled us to identify further steps to abstract related to data, which reduced the verification time to about six minutes. A final abstraction, related to the various TLS-related steps, was to abstract them using AnB bullet channels, used to model channels providing authentication and/or secrecy properties at the end-points. The internal efficiency of OFMC dealing with such channels led the final version to verify within eight seconds. This exponential efficiency (up to 5 orders of magnitude) increase is not uncommon in model checking problems, so long the right abstractions are taken alongside expert knowledge of the tool's implementation. We used the OFMC model checker [2] to verify the eight goals described above. At first, three goals (G4,G7,G8 ) about PSU intent authentication and account information secrecy and integrity failed. This led us to check these goals independently in order to study their reason for failure quickly. The witness for the PSU authentication failure (G4 ) relates to the resource server authenticating with an unknown agent rather than the PSU. This was fixed by having the resource server being aware of the PSU's identity early on when setting up the access consent with the AISP (A3.2). Thus, this failure identifies a previously undocumented vulnerability, which our modification fixes. The account information goals fail due to a limitation of bullet channels: they do not protect against replay attacks, hence their use here allowed breaking both secrecy (G7 ) and integrity (G8 ). The intruder could respond to the AISP's request for account data by replaying a previous message. This breaks integrity as the response received by the AISP, and perceived to be the account data, has been modified. As the data replayed is known to the intruder, it also breaks secrecy of the account data. However, the TLS protocol does protect against message replay [4, pp. 93-94] . To deal with this limitation and ensure that freshness would resolve the issue, we modified the model to include a nonce generated and sent by the AISP when requesting for the PSU account data and is expected to be part of the response. These modifications enable checking all goals for one session. Multiple sessions verification is important as there could be attacks relying on multiple concurrent protocol runs. Due to increased state space and limited hardware, we were unable to fully verify the model for two parallel sessions. As customary in under such conditions (e.g. [3] for iKP and SET), we were able to obtain partial results by increasing the search space up to the available resource limits (search space depth: 15 plies, 14.5 GB RAM, 50 h to run) without being able to reach any attack state. The novel Open Banking Account and Transaction protocol is a security-critical protocol, which is being enforced on the largest banks in Europe. Given the protocol's significance and expected wider use, verifying its correctness is crucial. Our findings were disseminated as part of a presentation on PSD2 at a UK Finance event, with representatives from Visa and MasterCard, as well as several banks. Some of the identified goals were known, others not. The audience was particularly keen on the time/cost analysis. Our future work will focus on the modelling of the protocol's state and transparent functions specification in VDM-SL: this is aimed at discovering underlying vulnerabilities related to the myriad of dependant technologies (e.g. OAuth2, TLS, etc.). Security analysis of the Open Banking Account and Transaction API Protocol OFMC: a symbolic model checker for security protocols Security protocol specification and verification with AnBx The Transport Layer Security (TLS) Protocol Version 1.2 A methodology for protocol verification applied to EMV R 1 The OAuth 2.0 Authorization Framework Towards secure open banking architecture: an evaluation with OWASP A hierarchy of authentication specifications Algebraic properties in Alice and Bob notation The open-source fixed-point model checker for symbolic analysis of security protocols AnBx: automatic generation and verification of security protocols implementations Open Banking Limited: Account and Transaction API Specification -v3 Open Banking Working Group: The Open Banking Standard The European Parliament and the Council of the European Union: DIRECTIVE (EU) 2015/2366