An Extensive Formal Security Analysis of the OpenID Financial Grade API

Explore an extensive formal security analysis of the OpenID Financial-grade API (FAPI) in this IEEE Symposium on Security & Privacy conference talk. Delve into the complexities of Open Banking APIs and their critical role in allowing third-party services access to customers' online banking accounts. Examine the FAPI's design as a high-security OAuth 2.0 profile, incorporating advanced mechanisms like Code and Token Binding, JWS Client Assertions, and Proof Key for Code Exchange. Follow the rigorous analysis using the Web Infrastructure Model (WIM) to uncover potential security vulnerabilities in authentication, authorization, and session integrity. Learn about the development of mitigations for identified attacks and the subsequent formal proof of security for a revised FAPI version. Gain insights into the challenges of securing financial applications and the importance of formal analysis in defining security properties and attacker models before implementation.

Introduction
Financial grade API
Overview
OAuth
Attacker Model
Roth Mutual TLS
Web Infrastructure Model
Browser Model
Overall Approach
Model
Security Properties
Authorization
Token Binding