Formal Verification of OAuth 2.0 Using Alloy Framework

Suhas Pai, Yash Sharma, Sunil Kumar, Radhika M. Pai, Sanjay Singh
  • June 2011, Institute of Electrical & Electronics Engineers (IEEE)
  • DOI: 10.1109/csnt.2011.141

Is OAuth flawless?

What is it about?

While using any social network be it facebook, twitter or linkedin OAauth is the underlying authentical protocol. We have used alloy to formally verify the various functionality of OAuth.

Why is it important?

We have used alloy tool to model and verify various functionality of OAuth protocol and could find a major limitation of OAuth.


Sanjay Singh
Manipal Institute of Technology, Manipal

Online social networks have increasingly become important now a days. Lot of privacy issues are associated with those services, if the there is any problem with the authentication modules of those services then it may casue abuse of users privacy data. Our work has tried to formally model and verify the various functionality to check if there is any problem with OAuth and it has found a limitation with the said protocol.

Read Publication

The following have contributed to this page: Sanjay Singh