Security analysis of openid connect protocol with cryptoverif in the computational model

Abstract

OpenID Connect protocol is widely used today, and it is one of the newest Single Sign-On protocols in authentication. At present, a lot of people are deeply focused on the researches of the security analysis of it. In this paper, we aimed at analyzing the authentication of OpenID Connect protocol by getting the message term of it through its authentication message flow, then formalizing it with Blanchet calculus in computational model, and finally transforming the model into the syntax of CryptoVerif, generate the CryptoVerif inputs in the form of channels Front-end, and import the syntax into the mechanized tool CryptoVerif to analyze its authentication. The result shows that OpenID Connect protocol has no authentication between the End-User and Authorization Server, Token Endpoint can’t authenticate Client, while Client can authenticate Token Endpoint.