Open Access

ARTICLE

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

Xingyun Hu^1,2, Siqi Lu^1,2,*, Liujia Cai^1,2, Ye Feng^1,2, Shuhao Gu^1,2, Tao Hu¹, Yongjuan Wang^1,2,*

1 Information Engineering University, Zhengzhou, China
2 Henan Key Laboratory of Network Cryptography Technology, Zhengzhou, China

* Corresponding Authors: Siqi Lu. Email: ; Yongjuan Wang. Email:

(This article belongs to the Special Issue: Cyberspace Mapping and Anti-Mapping Techniques)

Computers, Materials & Continua 2026, 88(1), 24 https://doi.org/10.32604/cmc.2026.079484

Received 22 January 2026; Accepted 23 February 2026; Issue published 08 May 2026

Abstract

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.

---

Keywords

---