| 摘 要: 本文在OAuth2.0授权码模型的基础上做出改进，采用HLPSL语言对授权码模型进行形式化建模，建立 OAuth2.0协议授权码模型形式化模型，找到授权码模型出现安全漏洞的根本原因是客户端凭证可以被攻击者窃取。结 合惰性无限状态方法和惰性攻击者优化方法对形式化模型分析和验证。提出OAuth2.0安全授权码模型，并分析和验证 其在理论上无安全漏洞。通过的研究，本文可以提供一套安全的OAuth2.0授权协议模型，对目前安全要求高的开放平 台的授权是有指导意义的。 |
| 关键词: OAuth2.0；安全；授权码模型；形式化 |
|
中图分类号: TP309
文献标识码: A
|
|
| The Research of the Security Authorization Model Based on OAuth2.0 Protocol |
|
WANG Tingting，ZHAO Songze1,2
|
1.( 1.Beijing Ziru Information Technology Co .Ltd ., Beijing 100873, China;2.
2.The Experimental High School Attached to Beijing Normal University, Beijing 100032, China )
|
| Abstract: Based on the OAuth2.0 protocol authorization code model,the paper adopts HLPSL to create a formal model
on the authentication code model.The root cause of the security vulnerability on the authorization code model is that attackers
can steal the client certificate.Through the analysis and verification of formal model by using the method of infinite state of
inertia and the optimization method of inert attackers,the paper proposes the OAuth2.0 security authorization code model,and
analyzes and verifies its zero security vulnerability in theory.Through the research,this paper provides a secure OAuth2.0
authorization protocol model,which is a guide for the authorization of the open platform with high security requirements. |
| Keywords: OAuth2.0;security;the authorization code model;formal |
