{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T13:37:21Z","timestamp":1787060241334,"version":"build-2736575974"},"publisher-location":"New York, NY, USA","reference-count":54,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,12,2]],"date-time":"2024-12-02T00:00:00Z","timestamp":1733097600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100006374","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1908494,2320903, 2323105, 2325369, 2317184"],"award-info":[{"award-number":["1908494,2320903, 2323105, 2325369, 2317184"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"Google","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["N66001-22-2-4037"],"award-info":[{"award-number":["N66001-22-2-4037"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"Ethereum Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,12,2]]},"DOI":"10.1145\/3658644.3670318","type":"proceedings-article","created":{"date-parts":[[2024,12,9]],"date-time":"2024-12-09T12:19:20Z","timestamp":1733746760000},"page":"2949-2962","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["<i>AuthSaber<\/i>\n                    : Automated Safety Verification of OpenID Connect Programs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2599-3825","authenticated-orcid":false,"given":"Tamjid","family":"Al Rahat","sequence":"first","affiliation":[{"name":"University of California, Los Angeles, Los Angeles, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1000-1229","authenticated-orcid":false,"given":"Yu","family":"Feng","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6435-564X","authenticated-orcid":false,"given":"Yuan","family":"Tian","sequence":"additional","affiliation":[{"name":"University of California, Los Angeles, Los Angeles, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,12,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"1986","unstructured":"Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. 1986. Compilers: Principles, Techniques, and Tools. Addison-Wesley. https:\/\/www.worldcat.org\/oclc\/12285707"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2019.2928541"},{"key":"e_1_3_2_1_3_1","unstructured":"AppAuth. 2023. AppAuth-Android. https:\/\/openid.github.io\/AppAuth-Android\/."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179325"},{"key":"e_1_3_2_1_5_1","volume-title":"Prateek Saxena, Jun Sun, Yang Liu, and Jin Song Dong.","author":"Bai Guangdong","year":"2013","unstructured":"Guangdong Bai, Jike Lei, Guozhu Meng, Sai Sathyanarayan Venkatraman, Prateek Saxena, Jun Sun, Yang Liu, and Jin Song Dong. 2013. Authscan: Automatic extraction of web authentication protocols from implementations. (2013)."},{"key":"e_1_3_2_1_6_1","volume-title":"Principles of model checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT press."},{"key":"e_1_3_2_1_7_1","volume-title":"Robert DeLine, Bart Jacobs, and K Rustan M Leino.","author":"Barnett Mike","year":"2006","unstructured":"Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K Rustan M Leino. 2006. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1--4, 2005, Revised Lectures 4. Springer, 364--387."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243846"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_3"},{"key":"e_1_3_2_1_10_1","volume-title":"27th USENIX Security Symposium. 1493--1510","author":"Calzavara Stefano","year":"2018","unstructured":"Stefano Calzavara, Riccardo Focardi, Matteo Maffei, Clara Schneidewind, Marco Squarcina, and Mauro Tempesta. 2018. WPSE: fortifying web protocols via browser-side security monitoring. In 27th USENIX Security Symposium. 1493--1510."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23394"},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. 1773--1788","author":"Cremers Cas","unstructured":"Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017. A comprehensive symbolic analysis of TLS 1.3. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. 1773--1788."},{"key":"e_1_3_2_1_14_1","volume-title":"2016 IEEE Symposium on Security and Privacy (SP). IEEE, 470--485","author":"Cremers Cas","unstructured":"Cas Cremers, Marko Horvat, Sam Scott, and Thyla van der Merwe. 2016. Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication. In 2016 IEEE Symposium on Security and Privacy (SP). IEEE, 470--485."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_3"},{"key":"e_1_3_2_1_17_1","volume-title":"Critical OAuth Vulnerability in Expo Framework Allows Account Hijacking. https:\/\/thehackernews.com\/2023\/05\/critical-oauth-vulnerability-in-expo. html.","year":"2023","unstructured":"Expo. 2023. Critical OAuth Vulnerability in Expo Framework Allows Account Hijacking. https:\/\/thehackernews.com\/2023\/05\/critical-oauth-vulnerability-in-expo. html."},{"key":"e_1_3_2_1_18_1","unstructured":"Facebook. 2018. Facebook Security Update. https:\/\/about.fb.com\/news\/2018\/09\/security-update."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Haonan Feng Hui Li Xuesong Pan Ziming Zhao and T Cactilab. 2021. A Formal Analysis of the FIDO UAF Protocol.. In NDSS.","DOI":"10.14722\/ndss.2021.24363"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00067"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978385"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.20"},{"key":"e_1_3_2_1_23_1","unstructured":"Google. 2023. Google Oauth Client. https:\/\/cloud.google.com\/java\/docs\/reference\/google-oauth-client\/latest\/overview."},{"key":"e_1_3_2_1_24_1","unstructured":"Grammarly. 2023. Critical OAuth Flaws Uncovered in Grammarly Vidio and Bukalapak Platforms. https:\/\/thehackernews.com\/2023\/10\/critical-oauth-flaws-uncovered-in.html."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3320269.3384724"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.38"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/MITP.2020.2973852"},{"key":"e_1_3_2_1_28_1","unstructured":"IETF. 2021. OAuth 2.0 Security Best Current Practice. https:\/\/datatracker.ietf.org\/doc\/html\/draft-ietf-oauth-security-topics."},{"key":"e_1_3_2_1_29_1","volume-title":"Software Abstractions: logic, language, and analysis","author":"Jackson Daniel","unstructured":"Daniel Jackson. 2012. Software Abstractions: logic, language, and analysis. MIT press."},{"key":"e_1_3_2_1_30_1","unstructured":"Charlie Jacomme Elise Klein Steve Kremer and Ma\u00efwenn Racouchot. 2023. A comprehensive formal and automated analysis of the EDHOC protocol. In USENIX Security'23--32nd USENIX Security Symposium."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_10"},{"key":"e_1_3_2_1_32_1","unstructured":"JWT. 2015. Json Web Token. https:\/\/datatracker.ietf.org\/doc\/html\/rfc7519."},{"key":"e_1_3_2_1_33_1","volume-title":"This is boogie 2. manuscript KRML 178, 131","author":"Leino K Rustan M","year":"2008","unstructured":"K Rustan M Leino. 2008. This is boogie 2. manuscript KRML 178, 131 (2008), 9."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_35_1","volume-title":"Cloud and Internet Computing: Proceedings of the 11th International Conference on P2P, Parallel, Grid, Cloud and Internet Computing (3PGCIC--2016)","author":"Lu Jintian","year":"2017","unstructured":"Jintian Lu, Jinli Zhang, Jing Li, ZhongyuWan, and Bo Meng. 2017. Automatic verification of security of openid connect protocol with proverif. In Advances on P2P, Parallel, Grid, Cloud and Internet Computing: Proceedings of the 11th International Conference on P2P, Parallel, Grid, Cloud and Internet Computing (3PGCIC--2016) November 5--7, 2016, Soonchunhyang University, Asan, Korea. Springer, 209--220."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_3_2_1_37_1","unstructured":"Microsoft. 2023. Azure B2C -- Crypto Misuse and Account Compromise. https:\/\/securityboulevard.com."},{"key":"e_1_3_2_1_38_1","unstructured":"Microsoft. 2023. Microsoft Bug Allowed Hackers to Breach Over Two Dozen Organizations via Forged Azure AD Tokens. https:\/\/thehackernews.com\/2023\/07\/microsoft-bug-allowed-hackers-to-breach.html."},{"key":"e_1_3_2_1_39_1","volume-title":"OAuth and OpenID Connect. In 2017 11th International Conference on Research Challenges in Information Science (RCIS). IEEE, 163--174","author":"Naik Nitin","year":"2017","unstructured":"Nitin Naik and Paul Jenkins. 2017. Securing digital identities in the cloud by selecting an apposite Federated Identity Management from SAML, OAuth and OpenID Connect. In 2017 11th International Conference on Research Challenges in Information Science (RCIS). IEEE, 163--174."},{"key":"e_1_3_2_1_40_1","volume-title":"VSTTE 2017","author":"Nejati Saeed","year":"2017","unstructured":"Saeed Nejati, Jia Hui Liang, Catherine Gebotys, Krzysztof Czarnecki, and Vijay Ganesh. 2017. Adaptive restart and CEGAR-based solver for inverting cryptographic hash functions. In Verified Software. Theories, Tools, and Experiments: 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22--23, 2017, Revised Selected Papers 9. Springer, 120--131."},{"key":"e_1_3_2_1_41_1","unstructured":"OpenID. 2021. OpenID Connect Core 1.0. https:\/\/openid.net\/specs\/openidconnect-core-1_0.html."},{"key":"e_1_3_2_1_42_1","unstructured":"OpenID. 2023. OpenID Certification. https:\/\/openid.net\/certification\/."},{"key":"e_1_3_2_1_43_1","unstructured":"Pac4j. 2023. Pac4J. https:\/\/www.pac4j.org."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00024"},{"key":"e_1_3_2_1_45_1","unstructured":"Portswigger. 2023. Authentication bug that enabled unauthorized access to client applications. https:\/\/portswigger.net."},{"key":"e_1_3_2_1_46_1","volume-title":"OAUTHLINT: An Empirical Study on OAuth Bugs in Android Applications. In 34th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2019","author":"Rahat Tamjid Al","year":"2019","unstructured":"Tamjid Al Rahat, Yu Feng, and Yuan Tian. 2019. OAUTHLINT: An Empirical Study on OAuth Bugs in Android Applications. In 34th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2019, San Diego, CA, USA, November 11--15, 2019. 293--304."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3559381"},{"key":"e_1_3_2_1_48_1","unstructured":"RFC6749. 2021. The OAuth 2.0 Authorization Framework. https:\/\/tools.ietf.org\/html\/rfc6750."},{"key":"e_1_3_2_1_49_1","unstructured":"SAML. 2023. SAML protocol. http:\/\/saml.xml.org\/saml-specifications."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12927-019-0003-8"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00085"},{"key":"e_1_3_2_1_52_1","volume-title":"Bulwark: Holistic and Verified Security Monitoring of Web Protocols. In European Symposium on Research in Computer Security. Springer, 23--41","author":"Veronese Lorenzo","year":"2020","unstructured":"Lorenzo Veronese, Stefano Calzavara, and Luca Compagna. 2020. Bulwark: Holistic and Verified Security Monitoring of Web Protocols. In European Symposium on Research in Computer Security. Springer, 23--41."},{"key":"e_1_3_2_1_53_1","unstructured":"WALA. 2023. T.J. Watson Libraries for Analysis (WALA). https:\/\/sourceforge.net\/projects\/wala."},{"key":"e_1_3_2_1_54_1","volume-title":"27th USENIX Security Symposium. 1459--1474","author":"Yang Ronghai","year":"2018","unstructured":"Ronghai Yang, Wing Cheong Lau, Jiongyi Chen, and Kehuan Zhang. 2018. Vetting Single Sign-On SDK Implementations via Symbolic Reasoning. In 27th USENIX Security Symposium. 1459--1474."}],"event":{"name":"CCS '24: ACM SIGSAC Conference on Computer and Communications Security","location":"Salt Lake City UT USA","acronym":"CCS '24","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3670318","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3658644.3670318","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T06:21:53Z","timestamp":1755843713000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3670318"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,2]]},"references-count":54,"alternative-id":["10.1145\/3658644.3670318","10.1145\/3658644"],"URL":"https:\/\/doi.org\/10.1145\/3658644.3670318","relation":{},"subject":[],"published":{"date-parts":[[2024,12,2]]},"assertion":[{"value":"2024-12-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}