AUTHSCAN: Automatic extraction of web authentication protocols from implementations

• Main Authors: BAI, Guangdong, LEI, Jike, MENG, Guozhu, VENKATRAMAN, Sai Sathyanarayan, SAXENA, Prateek, SUN, Jun, LIU, Yang, DONG, Jin Song
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2013
• Subjects: Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/5008; https://ink.library.smu.edu.sg/context/sis_research/article/6011/viewcontent/ndss2013authscan.pdf
• Institution: Singapore Management University

Ideally, security protocol implementations should be formally verified before they are deployed. However, this is not true in practice. Numerous high-profile vulnerabilities have been found in web authentication protocol implementations, especially in single-sign on (SSO) protocols implementations recently. Much of the prior work on authentication protocol verification has focused on theoretical foundations and building scalable verification tools for checking manually-crafted specifications [17, 18, 44]. In this paper, we address a complementary problem of automatically extracting specifications from implementations. We propose AUTHSCAN, an end-to-end platform to automatically recover authentication protocol specifications from their implementations. AUTHSCAN finds a total of 7 security vulnerabilities using off-the-shelf verification tools in specifications it recovers, which include SSO protocol implementations and custom web authentication logic of web sites with millions of users.