The OpenID Financial-grade API provides a mechanism for accessing data and resources that need a high degree of protection, such as in the context of financial applications. As a profile of the OAuth 2.0 Authorization Framework designed for high-risk scenarios, the Financial-grade API aims at being secure even if the procedure is attacked at several points leading to wrongly configured endpoints, the leakage of tokens and even whole requests and responses. To achieve this degree of security, several additional mechanisms are used, which protect against the usage of leaked tokens and protect messages against modification. We modeled both the Read-Only Profile and the Read-Write Profile of the Financial-grade API in the FKS Web Model, including all underlying assumptions that might affect the security of the flows. Through formal analysis, we discovered several attacks not only on mechanisms specific to the Financial-grade API but also on more general concepts of OAuth, namely, Token Binding and the Proof Key for Code Exchange extension. We provide mitigations against these attack scenarios and show that the modified flows are secure as specified by our security definitions. More precisely, these modified flows prevent an attacker from logging in under the identity of an honest user and accessing protected resources belonging to the honest user.