基于ASLan++的OAuth2.0协议授权码模型形式化建模与分析

doi:10.3778/j.issn.1002-8331.2408-0365

摘要/Abstract

摘要： OAuth2.0协议被广泛应用的同时，其安全性备受争议。针对授权码泄露和跨站请求伪造问题，对OAuth2.0协议中的授权码模型进行安全性研究。根据OAuth2.0协议标准，采用形式化建模语言ASLan++对授权码模型中的用户浏览器、第三方应用服务器和授权服务器进行形式化建模，分析模型的安全目标，并采用线性时态逻辑描述授权码模型的安全性质。使用基于SAT的模型检查器对授权码形式化模型进行模型检测，实验结果发现了8条被攻击的反例，其中7条反例证明了授权码模型存在授权码等重要参数泄露的问题，另外1条反例证明了授权码模型存在跨站请求伪造攻击的风险。在研究这些检测结果时，还发现了一种新的攻击——中间人攻击。它在用户浏览器和第三方应用服务器中充当第三者，在双方通信过程中窃取重要数据。分析了产生跨站请求伪造问题的原因，提出了一个增强授权码模型安全性的建议。

关键词: OAuth2.0协议, ASLan++, 形式化方法

Abstract: While OAuth2.0 protocol is widely used, its security is highly controversial. To address the problem of authorization code leakage and cross-site request forgery, the authorization code model in OAuth2.0 protocol is studied. Firstly, according to the OAuth2.0 protocol standard, user browsers, third-party application servers and authorization servers in the authorization code model are formally modelled by ASLan++ to analyze the security goals of the model, and linear temporal logic is used to describe the security properties of the authorization code model. Then a SAT-based model checker is used to perform model checking on the formal model of authorization code, and the result shows eight attacked counterexamples, seven of which prove that the authorization code model suffers from the leakage of important parameters such as authorization code, and the other one proves that the authorization code model is at risk of cross-site request forgery attacks. In addition, a new attack which called man-in-the-middle attack is found while studying the results. It acts as a third party between the user’s browsers and the third-party application servers and steals important data during the communication between the two parties. Finally, the causes of the cross-site request forgery problem are analyzed and a proposal is given to enhance the security of the authorization code model.

Key words: OAuth2.0 protocol, ASLan++, formal method

严海星. 基于ASLan++的OAuth2.0协议授权码模型形式化建模与分析[J]. 计算机工程与应用, 2025, 61(18): 309-316.

YAN Haixing. Formal Modelling and Analysis of Authorization Code Model in OAuth 2.0 Protocol Based on ASLan++[J]. Computer Engineering and Applications, 2025, 61(18): 309-316.

参考文献

[1] HARDT D. The OAuth 2.0 authorization framework[EB/OL]. [2024-09-20]. https://auth0.com/docs/authenticate/protocols/oauth.
[2] WANG H, GU D W, ZHANG Y Y, et al. An empirical study of security issues in SSO server-side implementations[J]. Science China Information Sciences, 2021, 65(7): 179104.
[3] YANG F, MANOHARAN S. A security analysis of the OAuth protocol[C]//Proceedings of the 2013 IEEE Pacific Rim Conference on Communications, Computers and Signal Processing. Piscataway: IEEE, 2013: 271-276.
[4] 魏成坤, 刘向东, 石兆军. OAuth2.0协议的安全性形式化分析[J]. 计算机工程与设计, 2016, 37(7): 1746-1751.
WEI C K, LIU X D, SHI Z J. Security formal verification of OAuth2.0 protocol[J]. Computer Engineering and Design, 2016, 37(7): 1746-1751.
[5] LI W P, MITCHELL C J, CHEN T. Your code is my code: exploiting a common weakness in OAuth 2.0 implementations[C]//Proceedings of the 26th International Workshop, Security Protocols XXVI. Cham: Springer, 2018: 24-41.
[6] ARSHAD E, BENOLLI M, CRISPO B. Practical attacks on login CSRF in OAuth[J]. Computers & Security, 2022, 121: 102859.
[7] PHILIPPAERTS P, PREUVENEERS D, JOOSEN W. OAuch: exploring security compliance in the OAuth 2.0 ecosystem[C]//Proceedings of the 25th International Symposium on Research in Attacks, Intrusions and Defenses. New York: ACM, 2022: 460-481.
[8] 王庆德, 吕欣, 王慧钧, 等. 数据安全治理的行业实践研究[J]. 信息安全研究, 2022, 8(4): 333-339.
WANG Q D, LYU X, WANG H J, et al. Research on industry practice of data security governance[J]. Journal of Information Security Research, 2022, 8(4): 333-339.
[9] 苏小红, 郑伟宁, 蒋远, 等. 基于学习的源代码漏洞检测研究与进展[J]. 计算机学报, 2024, 47(2): 337-374.
SU X H, ZHENG W N, JIANG Y, et al. Research and progress on learning-based source code vulnerability detection[J]. Chinese Journal of Computers, 2024, 47(2): 337-374.
[10] 李懿, 田玉玲. 远程医疗信息系统中的三因素匿名认证协议[J]. 计算机工程与应用, 2023, 59(10): 280-287.
LI Y, TIAN Y L. Three-factor anonymous authentication protocol in telecare medicine information system[J]. Computer Engineering and Applications, 2023, 59(10): 280-287.
[11] 陈洪森, 方勇, 郝城凌, 等. 基于小样本学习的源码漏洞检测[J]. 信息安全研究, 2024, 10(5): 440-445.
CHEN H S, FANG Y, HAO C L, et al. Source code vulnerability detection based on few-shot learning[J]. Journal of Information Security Research, 2024, 10(5): 440-445.
[12] 陈传涛, 潘丽敏, 龚俊, 等. 基于抽象语法树压缩编码的漏洞检测方法[J]. 信息安全研究, 2022, 8(1): 35-42.
CHEN C T, PAN L M, GONG J, et al. The vulnerability detection method based on compression coding of abstract syntax tree[J]. Journal of Information Security Research, 2022, 8(1): 35-42.
[13] 师自通, 师智斌, 刘冬明, 等. 多头注意力机制的图同构网络智能合约源码漏洞检测[J]. 计算机工程与应用, 2024, 60(7): 258-265.
SHI Z T, SHI Z B, LIU D M, et al. Smart contract source code vulnerability detection of graph isomorphism network with multi-head attention mechanism[J]. Computer Engineering and Applications, 2024, 60(7): 258-265.
[14] SUMONGKAYOTHIN K, RACHTRACHOO P, YUPUECH A, et al. OVERSCAN: OAuth 2.0 scanner for missing parameters[C]//Proceedings of the International Conference on Network and System Security. Cham: Springer, 2019: 221-233.
[15] LI W P, MITCHELL C J, CHEN T. OAuthGuard: protecting user security and privacy with OAuth 2.0 and OpenID connect[C]//Proceedings of the 5th ACM Workshop on Security Standardisation Research Workshop. New York: ACM, 2019: 35-44.
[16] YANG R H, LI G C, LAU W C, et al. Model-based security testing: an empirical study on OAuth 2.0 implementations[C]//Proceedings of the 11th ACM on Asia Conference on Computer and Communications Security. New York: ACM, 2016: 651-662.
[17] JAYASRI K S, JEVITHA K P, JAYARAMAN B. Verification of OAuth 2.0 using UPPAAL[M]//Communications in computer and information science. Singapore: Springer, 2018: 58-67.
[18] PAI S, SHARMA Y, KUMAR S, et al. Formal verification of OAuth 2.0 using alloy framework[C]//Proceedings of the 2011 International Conference on Communication Systems and Network Technologies. Piscataway: IEEE, 2011: 655-659.
[19] 程道雷, 肖美华, 刘欣倩, 等. 运用SPIN对开放授权协议OAuth 2.0的分析与验证[J]. 计算机工程与科学, 2015, 37(11): 2121-2127.
CHENG D L, XIAO M H, LIU X Q, et al. Analyzing and verifying an open authorization protocol OAuth 2.0 with SPIN[J]. Computer Engineering & Science, 2015, 37(11): 2121-2127.