OAuth2.0协议形式化验证：使用AVISPA

摘要

OAuth is an protocol used to identify the client, and control resource access. Because it concerns about the privacy of the private resource owner, the security of OAuth protocol is fairly important. This paper mainly research on the OAuth2.0 protocol text, and make an abstraction on it, build an model in AVISPA, an formal verification tool for security protocols , and then verify the model in AVISPA. Finally, we find there is an attack mode that may result in leaking the private resource to attackers. We suggest a way to model the message to be authenticated as a symmetric key, which is innovative. This modelling and verification method we used on analyzing OAuth2.0 can be used in the verification of other security protocols, like the online payment protocol.%OAuth协议是一套用于在不同的服务中进行身份认证并且实现资源互访一套协议.由于关系到用户隐私，所以OAuth协议的安全性非常重要.这篇文章的主要贡献是研究OAuth2.0协议文本，对协议进行抽象，并且使用验证工具AVISPA对抽象后的协议进行建模与验证，找到协议中会导致隐私泄露的一种攻击模式.我们在建模过程中提出需将要验证的消息作为双方的对称密码这样一种创新思路.这种对协议的抽象和验证的方法可以推广到其他安全协议上，例如在线支付协议等等.