运用SPIN对开放授权协议OAuth 2.0的分析与验证

OAuth 2.0协议是一种开放授权协议,主要用于解决用户账号关联与资源共享问题。但是,其弱安全性导致各网络公司海量用户信息泄露,且OAuth 2.0传输数据采用的https通道效率低下,成为黑客攻击对象。提出采用http通道传输OAuth 2.0协议数据,基于Promale语言及Dolev-Yao攻击者模型对OAuth 2.0协议建模,运用SPIN进行模型检测。形式化分析结果表明,采用公钥加密体系对OAuth 2.0协议进行加密不安全。上述建模方法对类似的授权协议形式化分析有重要借鉴意义。

Analyzing and verifying an open authorization protocol OAuth 2.0 with SPIN

The OAuth 2.0 is an open authorization protocol which solves the problem of user accounts associating and resources sharing. However, due to its weak security, massive user information of network companies is leaking. Besides, the https channel used by OAuth 2.0 to transmit data is inefficient, making the OAuth 2.0 an attack object of hackers. We propose an open authorization protocol, which transmits the data of the OAuth 2.0 protocol in http channels, model the protocol based on the Promale language and Dolev Yao attacker model, and employ the SPIN for model checking. The results of formal analysis show that the OAuth2.0 protocol encrypted by the public key encryption system is unsafe. The proposed modeling method has great significance in formal analysis of similar license agreement.