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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Mouli, V.R., Jevitha, K.: Web services attacks and security-a systematic literature review. Procedia Comput. Sci. 93, 870–877 (2016)
Poornachandran, P., Nithun, M., Pal, S., Ashok, A., Ajayan, A.: Password reuse behavior: how massive online data breaches impacts personal data in web. In: Saini, H.S., Sayal, R., Rawat, S.S. (eds.) Innovations in Computer Science and Engineering. AISC, vol. 413, pp. 199–210. Springer, Singapore (2016). https://doi.org/10.1007/978-981-10-0419-3_24
Franks, J., et al.: HTTP authentication: basic and digest access authentication. Technical report (1999)
Luo, X., Chen, Y., Gu, M., Wu, L.: Model checking needham-schroeder security protocol based on temporal logic of knowledge. In: 2009 International Conference on Networks Security, Wireless Communications and Trusted Computing. NSWCTC 2009, vol. 2, pp. 551–554. IEEE (2009)
Díaz, G., Cuartero, F., Valero, V., Pelayo, F.: Automatic verification of the TLS handshake protocol. In: Proceedings of the 2004 ACM Symposium on Applied Computing, pp. 789–794. ACM (2004)
Yuan, T., et al.: Formalization and verification of REST on HTTP using CSP. Electron. Notes Theor. Comput. Sci. 309, 75–93 (2014)
Yan, H., Fang, H., Kuka, C., Zhu, H.: Verification for OAuth using ASLan++. In: 2015 IEEE 16th International Symposium on High Assurance Systems Engineering (HASE), pp. 76–84. IEEE (2015)
Fett, D., Küsters, R., Schmitz, G.: A comprehensive formal security analysis of OAuth 2.0. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 1204–1215. ACM (2016)
Pai, S., Sharma, Y., Kumar, S., Pai, R.M., Singh, S.: Formal verification of OAuth 2.0 using alloy framework. In: 2011 International Conference on Communication Systems and Network Technologies (CSNT), pp. 655–659. IEEE (2011)
Richer, J., Sanso, A.: OAuth 2 in Action. Manning Publications, Shelter Island (2017)
Hardt, D.: The OAuth 2.0 authorization framework (2012)
Lodderstedt, T., McGloin, M., Hunt, P.: OAuth 2.0 threat model and security considerations (2013)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL 4.0 (2006, 2014). URL http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. (STTT) 1(1), 134–152 (1997)
Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)
Sabnani, K.: An algorithmic technique for protocol verification. IEEE Trans. Commun. 36(8), 924–931 (1988)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Jayasri, K.S., Jevitha, K.P., Jayaraman, B. (2018). Verification of OAuth 2.0 Using UPPAAL. In: Mandal, J., Sinha, D. (eds) Social Transformation – Digital Way. CSI 2018. Communications in Computer and Information Science, vol 836. Springer, Singapore. https://doi.org/10.1007/978-981-13-1343-1_7
Download citation
DOI: https://doi.org/10.1007/978-981-13-1343-1_7
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-13-1342-4
Online ISBN: 978-981-13-1343-1
eBook Packages: Computer ScienceComputer Science (R0)