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

来源：计算机工程与应用杂志2025年第18期北京时间：

作者：严海星

单位：福建医科大学 文理艺术学院，福州 350000

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

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