基于计算模型的 OpenID Connect协议认证性的自动化分析

分析了OpenID Connect协议的消息结构，基于计算模型应用Blanchet演算对 OpenID Connect 协议进行了形式化建模，应用自动化验证工具CryptoVerif 验证了其认证性．结果表明: 在 OpenID Connect 协议中，客户端能够认证终端用户，但是终端用户与授权服务器之间不能相互认证、 令牌终端不能认证客户端．为此，给出了OpenID Connect 协议中不具有认证性问题的解决方法