Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Security Analysis of the Open Banking Account and Transaction API Protocol

Paolo Modesti, Leo Freitas, Qudus Shotomiwa, Abdulaziz Almehrej

TL;DR

The paper tackles the problem of ensuring correctness and security of the Open Banking Account and Transaction API protocol through formal modelling with AnBx and automated verification using OFMC (single-session) and ProVerif (unbounded sessions). It contributes by delivering a typed, automatically verifiable AnBx model that captures the ATP flow, token handling, and consent mechanisms, while addressing vertical composition with assumed secure channels. The authors validate the approach both formally and practically by coupling the model with security testing in the NatWest sandbox, confirming key security goals under the model and highlighting the strengths and limitations of the verification tools. The work has practical significance for PSD2/Open Banking security, providing a rigorous foundation that can inform PSD3/PSR and encourage broader adoption of formal methods in banking API compliance. Limitations include abstractions of TLS/OAuth/OIDC and the challenge of scaling OFMC to fully explore multi-session interleavings, underscoring the value of complementary tools and future work to extend the model to timing properties and additional protocol components.

Abstract

The Second Payment Services Directive (PSD2) of the European Union aims to create a consumer-friendly financial market by mandating secure and standardised data sharing between banking operators and third parties. Consequently, EU countries and the United Kingdom have adopted Open Banking, a standardised data-sharing API. This paper presents a formal modelling and security analysis of the UK Open Banking Standard's APIs, with a specific focus on the Account and Transaction API protocol. Our methodology employs the extended Alice and Bob notation (AnBx) to create a formal model of the protocol, which is then verified using the OFMC symbolic model checker and the Proverif cryptographic protocol verifier. We extend previous work by enabling verification for unlimited sessions with a strongly typed model. Additionally, we integrate our formal analysis with practical security testing of some necessary conditions to demonstrate verified security-goals in the NatWest Open Banking sandbox, evaluating mechanisms such as authorisation and authentication procedures.

Security Analysis of the Open Banking Account and Transaction API Protocol

TL;DR

The paper tackles the problem of ensuring correctness and security of the Open Banking Account and Transaction API protocol through formal modelling with AnBx and automated verification using OFMC (single-session) and ProVerif (unbounded sessions). It contributes by delivering a typed, automatically verifiable AnBx model that captures the ATP flow, token handling, and consent mechanisms, while addressing vertical composition with assumed secure channels. The authors validate the approach both formally and practically by coupling the model with security testing in the NatWest sandbox, confirming key security goals under the model and highlighting the strengths and limitations of the verification tools. The work has practical significance for PSD2/Open Banking security, providing a rigorous foundation that can inform PSD3/PSR and encourage broader adoption of formal methods in banking API compliance. Limitations include abstractions of TLS/OAuth/OIDC and the challenge of scaling OFMC to fully explore multi-session interleavings, underscoring the value of complementary tools and future work to extend the model to timing properties and additional protocol components.

Abstract

The Second Payment Services Directive (PSD2) of the European Union aims to create a consumer-friendly financial market by mandating secure and standardised data sharing between banking operators and third parties. Consequently, EU countries and the United Kingdom have adopted Open Banking, a standardised data-sharing API. This paper presents a formal modelling and security analysis of the UK Open Banking Standard's APIs, with a specific focus on the Account and Transaction API protocol. Our methodology employs the extended Alice and Bob notation (AnBx) to create a formal model of the protocol, which is then verified using the OFMC symbolic model checker and the Proverif cryptographic protocol verifier. We extend previous work by enabling verification for unlimited sessions with a strongly typed model. Additionally, we integrate our formal analysis with practical security testing of some necessary conditions to demonstrate verified security-goals in the NatWest Open Banking sandbox, evaluating mechanisms such as authorisation and authentication procedures.

Paper Structure

This paper contains 37 sections, 2 equations, 19 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Contribution
  3. Background
  4. The Open Banking Standard Overview
  5. Account and Transaction API Protocol
  6. Account and Transaction API Use Case Example
  7. Methodology and Specification Language
  8. Formal Model
  9. Roles and Responsibilities
  10. Initial Knowledge
  11. Actions
  12. Messages Definitions
  13. Automated Verification
  14. Security Goals
  15. Verification
  16. ...and 22 more sections

Figures (19)

  • Figure 1: The Account and Transaction API protocol high-level flow
  • Figure 2: Account and Transaction API Use Case Example
  • Figure 3: Modelling and Verification Methodology (manual automatic)
  • Figure 4: Account and Transaction API Protocol -- Model Sequence Diagram
  • Figure 5: Account and Transaction API Protocol -- Model Sequence Diagram -- Step 1
  • ...and 14 more figures