Publication

Abstract : Web services are software services that are accessible over the internet through a set of application program interfaces (APIs). The security of these APIs is a major concern because of their loose coupling, and protection mechanisms are needed to safeguard them from attacks. The simplest of these mechanisms are authentication and authorization. A client that requests access to a web API should be authorized by an end-user who has been authenticated by an authorization server. OAuth 2.0 can be used to achieve this protection. The security properties of a widely used protocol such as OAuth 2.0 should be verified, since many systems depend on this protocol for protection. This paper focuses on verifying three important classes of properties of OAuth 2.0, namely safety, liveness, and absence of deadlock. A model of the OAuth protocol was developed using UPPAAL, a tool used for modeling and verification. This model consists of four finite state machines, one representing each of the roles in OAuth 2.0, and the properties of interest were verified using this model.