Verification for OAuth Using ASLan

Over the past few years, OAuth has become an open authorization standard that is being adopted by a growing number of sites such as Twitter, Facebook and Google. It allows users to grant a third-party application access to restricted resources without providing their credentials. However, ensuring the correctness of implementations of OAuth in applications brings multiple concerns. Therefore, it is crucial to verify OAuth with an exhaustive examination by utilizing formal methods. In this paper, we first formalize OAuth with ASLan++ on the AVANTSSAR platform and propose several fundamental security properties on it which are specified using extended Linear Temporal Logic (LTL) formulas. In a second step, we use a SAT-based Model-Checker (SATMC) to verify whether OAuth violates these properties. As a result, we reveal three attacks which steal and falsify users' critical information.