An Extensive Formal Security Analysis of the OpenID Financial Grade API

This course provides an extensive formal security analysis of the OpenID Financial-grade API, focusing on the security requirements for open banking APIs. The learning outcomes include understanding the security mechanisms of the FAPI, such as Code and Token Binding, JWS Client Assertions, and Proof Key for Code Exchange. The course teaches how to develop a precise model of the FAPI in the Web Infrastructure Model and define central security properties. The teaching method involves a rigorous, systematic formal analysis to uncover and mitigate severe attacks, ensuring the security of the FAPI. The intended audience for this course includes security professionals, developers, and individuals involved in the implementation of financial-grade APIs.