Unveiling Authentication Forgery in OpenID Connect under Web Frameworks: A Formal Analysis of CSRF-Based Attack Paths

With the widespread adoption of web applications and cloud services, the OAuth 2.0-based OpenID Connect (OIDC) Single Sign-on (SSO) protocol has become the core of modern digital identity authentication. Although the OIDC protocol itself has strict security specifications, its implementation in real-world web frameworks can introduce critical vulnerabilities, particularly the improper omission of the state parameter, which leads to severe authentication forgery risks. Existing research often overlooks these implementation-level flaws, especially from a formal analysis perspective. This paper addresses this gap by formally analyzing the authentication forgery attack resulting from the missing state parameter. We construct a high-fidelity web framework model and, using the Tamarin formal analysis tool, systematically analyze the flawed OIDC implementation. Specifically, we demonstrate an attack path where cross-site request forgery is leveraged as a vector to deceive the relying party, ultimately achieving identity binding forgery—linking the attacker’s identity to the victim’s session. In response to this forgery vulnerability, this article proposes and formally verifies corresponding patches to successfully defend against such attacks. Finally, this paper provides concrete guidance for developers. This research, through formal methods, characterizes a replicable authentication forgery pattern within modern web architectures, providing a robust theoretical and practical foundation for hardening SSO systems against such advanced forgery threats.