Online citations, reference lists, and bibliographies.

Discovering Concrete Attacks On Website Authorization By Formal Analysis

Chetan Bansal, K. Bhargavan, Sergio Maffeis
Published 2012 · Computer Science

Cite This
Download PDF
Analyze on Scholarcy
Share
Social sign-on and social sharing are becoming an ever more popular feature of web applications. This success is largely due to the APIs and support offered by prominent social networks, such as Facebook, Twitter, and Google, on the basis of new open standards such as the OAuth 2.0 authorization protocol. A formal analysis of these protocols must account for malicious websites and common web application vulnerabilities, such as cross-site request forgery and open redirectors. We model several configurations of the OAuth 2.0 protocol in the applied pi-calculus and verify them using ProVerif. Our models rely on WebSpi, a new library for modeling web applications and web-based attackers that is designed to help discover concrete website attacks. Our approach is validated by finding dozens of previously unknown vulnerabilities in popular websites such as Yahoo and Word Press, when they connect to social networks such as Twitter and Facebook.
This paper references
Formal analysis of Facebook Connect Single Sign-On authentication protocol
Caterina Urban (2010)
10.3233/JCS-2009-0339
Automatic verification of correspondences for security protocols
B. Blanchet (2009)
Functions as processes. In Automata, Languages and Programming, volume 443 of Lecture Notes in Computer Science, pages 167–180
R. Milner (1990)
On Breaking SAML: Be Whoever You Want to Be
Juraj Somorovsky (2012)
10.1145/360204.360213
Mobile values, new names, and secure communication
M. Abadi (2001)
Busting frame busting: a study of clickjacking vulnerabilities at popular sites, in: Web 2.0
G. Rydstedt (2010)
10.1007/11555827_28
Browser Model for Security Analysis of Browser-Based Protocols
T. Groß (2005)
10.1006/inco.1998.2740
A Calculus for Cryptographic Protocols: The spi Calculus
M. Abadi (1999)
Universally Composable Security Analysis of OAuth v2.0
S. Chari (2011)
10.17487/RFC6797
HTTP Strict Transport Security (HSTS)
J. Hodges (2012)
10.1109/SP.2012.30
Signing Me onto Your Accounts through Facebook and Google: A Traffic-Guided Security Study of Commercially Deployed Single-Sign-On Web Services
R. Wang (2012)
10.4018/jsse.2011100103
JavaSPI: A Framework for Security Protocol Implementation
Matteo Avalle (2011)
10.1109/MSP.2010.203
On Adversary Models and Compositional Security
A. Datta (2011)
10.1109/MIC.2003.1250582
Analysis of Liberty Single-Sign-on with Enabled Clients
B. Pfitzmann (2003)
10.1145/1368310.1368330
Verified implementations of the information card federated identity-management protocol
K. Bhargavan (2008)
10.1007/3-540-44880-2_1
Alloy: A Logical Modelling Language
Daniel Jackson (2003)
10.1109/CSF.2010.27
Towards a Formal Foundation of Web Security
Devdatta Akhawe (2010)
OpenID OAuth Extension
D. Balfanz (2009)
10.1007/978-3-642-36830-1_7
Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage
Chetan Bansal (2013)
10.1016/j.tcs.2003.12.023
Private authentication
M. Abadi (2004)
10.1109/SFCS.2001.959888
Universally composable security: a new paradigm for cryptographic protocols
R. Canetti (2001)
10.1007/11542322_20
Federated Identity-Management Protocols
B. Pfitzmann (2003)
Assertions and Protocol for the OASIS Security Assertion Markup Language (SAML) V2. 0
Carslile Adams (2001)
10.1109/CSF.2007.7
A Type Discipline for Authorization in Distributed Systems
C. Fournet (2007)
10.1109/RISP.1993.287633
A semantic model for authentication protocols
T. Woo (1993)
10.17487/RFC6819
OAuth 2.0 Threat Model and Security Considerations
T. Lodderstedt (2013)
10.17487/RFC6749
The OAuth 2.0 Authorization Framework
D. Hardt (2012)
10.1016/j.cose.2012.08.007
An authentication flaw in browser-based Single Sign-On protocols: Impact and remediations
Alessandro Armando (2013)
10.1007/978-3-642-36563-8_4
Towards Unified Authorization for Android
Michael J. May (2013)
WebSpi and web application models
K. Bhargavan C. Bansal (2005)
10.1109/CSFW.2001.930138
An efficient cryptographic protocol verifier based on prolog rules
B. Blanchet (2001)
Busting frame busting a study of clickjacking vulnerabilities on popular sites
Gustav Rydstedt (2010)
10.1109/TIT.1983.1056650
On the security of public key protocols
D. Dolev (1981)
10.3233/JCS-2007-15603
Timed analysis of security protocols
R. Corin (2007)
The OAuth 2.0 Authorization Protocol: Bearer Tokens draft-ietf-oauth-v2-bearer-10
D. Recordon (2012)
Functions as processes, Mathematical Structures in Computer Science
R. Milner (1992)
Cross-origin resource sharing, 2013, available at: http://www.w3.org/TR/cors
A. van Kesteren (2013)
10.1007/11513988_27
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications
A. Armando (2005)
10.17487/RFC5849
The OAuth 1.0 Protocol
E. Hammer-Lahav (2010)
10.3233/JCS-140503
Discovering concrete attacks on website authorization by formal analysis
Chetan Bansal (2014)
Zălinescu, Verified cryptographic implementations for TLS
K. Bhargavan (2012)
10.1109/CSNT.2011.141
Formal Verification of OAuth 2.0 Using Alloy Framework
Suhas A. Pai (2011)
Knowledge Flow Analysis for Security Protocols
Emina Torlak (2006)
WebSpi and web application models. http://prosecco
C. Bansal (2011)
10.1007/978-3-540-31987-0_11
A Type Discipline for Authorization Policies
C. Fournet (2005)
10.1145/266420.266432
A calculus for cryptographic protocols: the spi calculus
M. Abadi (1997)
10.1145/2382196.2382238
The devil is in the (implementation) details: an empirical analysis of OAuth SSO systems
San-Tsai Sun (2012)
10.1145/1179529.1179532
OpenID 2.0: a platform for user-centric identity management
D. Recordon (2006)
Security Analysis of Double Redirection Protocols
F. Corella (2011)
10.1145/1455770.1455782
Robust defenses for cross-site request forgery
A. Barth (2008)
Featherweight Firefox: Formalizing the Core of a Web Browser
A. Bohannon (2010)
Towards a Declarative Language and System for Secure Networking
M. Abadi (2007)
WebSpi and web application models. http://prosecco.gforge.inria
C.Bansal (2011)
OAuth Security Advisory: 2009.1 - Session Fixation Attack
E. Hammer-Lahav (2009)
10.1145/1045405.1045409
Using static analysis to validate the SAML single sign-on protocol
Steffen M. Hansen (2005)
AUTHSCAN: Automatic Extraction of Web Authentication Protocols from Implementations
Guangdong Bai (2013)
10.1587/transinf.E92.D.836
Information-Flow-Based Access Control for Web Browsers
Sachiko Yoshihama (2009)
10.1145/2133375.2133378
Verified Cryptographic Implementations for TLS
Karthikeyan Bhargavan (2012)
10.1017/S0960129500001407
Functions as Processes
R. Milner (1992)
10.1145/1456396.1456397
Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for google apps
A. Armando (2008)
10.1109/SECPRI.2002.1004365
Binder, a logic-based security language
J. DeTreville (2002)
10.1109/CSFW.2006.32
Verified Interoperable Implementations of Security Protocols
K. Bhargavan (2006)
ProVerif 1.85: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial
B. Blanchet (2011)



This paper is referenced by
10.1145/3321705.3329801
MoSSOT: An Automated Blackbox Tester for Single Sign-On Vulnerabilities in Mobile Applications
Shangcheng Shi (2019)
10.1007/978-3-319-12226-7_6
Attacks on the Browser’s Requests
Philippe De Ryck (2014)
10.1145/2976749.2978385
A Comprehensive Formal Security Analysis of OAuth 2.0
Daniel Fett (2016)
Towards High Assurance HTML5 Applications
Devdatta Akhawe (2014)
10.1007/978-3-642-54568-9_15
Reference Monitors for Security and Interoperability in OAuth 2.0
Ronan-Alexandre Cherrueau (2013)
Abstract Semantics for Software Security Analysis
Zhijie Chen (2015)
10.1145/3127586
The Applied Pi Calculus
M. Abadi (2018)
10.1145/2897845.2897874
Model-based Security Testing: An Empirical Study on OAuth 2.0 Implementations
R. Yang (2016)
10.3233/JCS-140503
Discovering concrete attacks on website authorization by formal analysis
Chetan Bansal (2014)
10.1007/978-3-030-03251-7_3
Your Code Is My Code: Exploiting a Common Weakness in OAuth 2.0 Implementations
Wanpeng Li (2018)
10.1145/2810103.2813726
SPRESSO: A Secure, Privacy-Respecting Single Sign-On System for the Web
Daniel Fett (2015)
Modeling and Assessing OAuth 2.0 under PoP (Proof of Possession) for Secrecy
nbspBharatkumar K. Talaviya (2015)
My City Guide Mobile Application
Aniket Patil (2019)
10.1007/978-3-319-78813-5_41
A Framework for Formal Analysis of Privacy on SSO Protocols
Kailong Wang (2017)
The Devil Is Phishing: Rethinking Web Single Sign-On Systems Security
Chuan Yue (2013)
10.1007/978-3-319-24174-6_3
Analyzing the BrowserID SSO System with Primary Identity Providers Using an Expressive Model of the Web
Daniel Fett (2015)
10.1145/3386723.3387888
Web OAuth-based SSO Systems Security
Yassine Sadqi (2020)
10.1109/ICRTIT.2014.6996166
Detecting cloning attack in Social Networks using classification and clustering techniques
S. Kiruthiga (2014)
Development and quality assessment of cookies prepared by using “Wheat flour & Sattu”
Narendra Nath (2017)
ASPIRE: Iterative Specification Synthesis for Security
K. Chen (2015)
10.1007/s10009-015-0385-y
SATMC: a SAT-based model checker for security protocols, business processes, and security APIs
Alessandro Armando (2015)
10.1007/978-981-10-8890-2_11
Achieving Communication Effectiveness of Web Authentication Protocol with Key Update
Zijian Zhang (2017)
10.1007/978-3-030-25540-4_12
Automated Synthesis of Secure Platform Mappings
Eunsuk Kang (2019)
10.1007/978-3-030-02450-5_31
Analyzing Security and Privacy in Design and Implementation of Web Authentication Protocols
Kailong Wang (2018)
Web-based Attacks on Host-Proof Encrypted Storage
K. Bhargavan (2012)
10.1109/SP.2014.49
An Expressive Model for the Web Infrastructure: Definition and Application to the Browser ID SSO System
Daniel Fett (2014)
10.3929/ethz-b-000372337
Modelling and Analysis of Web Applications in Tamarin
Sandra Dünki (2019)
10.1145/2660460.2660463
Application impersonation: problems of OAuth and API design in online social networks
Pili Hu (2014)
10.1109/ICECCS.2015.39
Analyzing Security Property of Android Application Implementation Using Formal Method
Quanqi Ye (2015)
Analysis of privacy in mobile telephony systems
ArapinisMyrto (2017)
10.1007/978-3-319-10082-1
Foundations of Security Analysis and Design VII
A. Aldini (2014)
MODELING AND ANALYZING WEB PROTOCOLS FOR TRUST AND SECRECY
A. Kumar (2012)
See more
Semantic Scholar Logo Some data provided by SemanticScholar