Formal Analysis of Facebook Connect Single Sign-On Authentication Protocol

Abstract

We present a formal analysis of the authentication protocol of Facebook Connect, the Single Sign-On service offered by the Facebook Platform which allows Facebook users to login to affiliated sites.

Formal specification and verification have been carried out using the specification language HLPSL and AVISPA, a state-of-the-art verification tool for security protocols. AVISPA has revealed two security flaws, one of which (previously unheard of, up to our knowledge) allows an intruder to impersonate a user at a service provider affiliated with Facebook. To address this problem, we propose a modification of the protocol, by adding a message authentication mechanism; this protocol has been verified with AVISPA to be safe from the masquerade attack. Finally, we sketch a JavaScript implementation of the modified protocol.

Publication
In Proc. Student Research Forum of 37th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2011)
Best Poster Award
Date