Full text
Enhancing Security Testing for Identity Management Implementations: Introducing MIG-L and MIG-T Andrea Bisegna1, Matteo Bitussi1, Roberto Carbone1, and Silvio Ranise1,2 1Center for Cybersecurity, Fondazione Bruno Kessler, Trento, Italy {a.bisegna,carbone,ranise}@fbk.eu, [email protected] 2Department of Mathematics, University of Trento, Italy Abstract. We introduce MIG-L, a declarative language for the specification of security tests, and MIG-T, a testing tool, for Identity Management solutions based on SAML and OAuth/OIDC by verifying compliance with Best Current Practices, detecting known vulnerabilities, and providing suggestions for fixes. Experiments demonstrate the flexibility and effectiveness of our approach. 1 Multi-Party Web Applications play a crucial role in building trust in digital ecosystems by adopting Identity Management (IdM) protocols to secure their implementations. IdM protocols involve three entities: the User (typically interacting through a web browser), the web application (playing the role of a Client), and an Identity Provider (IdP) acting as a trusted third party. Standards for IdM protocols are available—e.g., SAML 2.0 (SAML),3OpenID Connect (OIDC),4and OAuth 2.0 (OAuth)5—that describe how Clients can request and consume assertions from IdPs to authenticate users via Single Sign-On (SSO) procedures. This allows users to access multiple applications or services using a single set of credentials while providing a streamlined user experience and increasing security by reducing password fatigue. Despite the advantages, several vulnerabilities have been and are still being found, exposing potential errors and security risks inherent in design and implementation [1,6,?]. The complexity of protocols and reliance on third-party entities further exacerbate the risks. Privacy and data protection concerns necessitate meticulous consideration during deployment. Fragmentation of information sources and a dearth of comprehensive remediation strategies contribute to the complexity of securing these systems. While security testing tools are available, they often exhibit a narrow focus on specific vulnerabilities, potentially overlooking broader security concerns [8,9,10,11]. Moreover, administrators may lack the expertise required to 3https://docs.oasis-open.org/security/saml/Post2.0/sstc-saml-tech-overview2.0.html 4https://openid.net/connect 5https://tools.ietf.org/html/rfc6749
2 Andrea Bisegna, Matteo Bitussi, Roberto Carbone, and Silvio Ranise address vulnerabilities effectively, particularly for average IT professionals. To alleviate these problems, we propose a declarative language for security testing, providing a straightforward method to define and execute security test cases in the context of IdM deployments by making the following main contributions: –We consider an existing threat model [4] based on security controls, threats, vulnerabilities, and risks, and propose an extended version. The extended version allows us not only to perform security tests to identify known vulnerabilities but also to check compliance with Best Current Practices (BCPs) put forward by standardization efforts (e.g., OIDC) to avoid recurring vulnerabilities with high risk. –We introduce a novel approach for the specification of the test cases leveraging a new declarative language named MIG-L. The language is tailored specifically for IdM protocols and is built upon the extended threat model previously defined. –We automate our approach by integrating MIG-L into MIG-T,6a security testing tool included in Micro-Id-Gym [5]. –For validation, we conducted experiments with MIG-T in three scenarios involving IdM protocols. In an OIDC deployment, we identified three vulnerabilities. In an OAuth implementation for a PSD2 compliant payment service, we detected two vulnerabilities and a misconfiguration in the OAuth protocol. Among 48 pairs of service and identity providers supporting SSO-based Account Linking, we identified 21 pairs vulnerable to CSRF. We make available the security tests specified in MIG-L and the code of MIGT at the following links https://github.com/stfbk/mig/tree/master/testplans/spidcie-oidc/implementations/spid-cie-oidc-django/input/mig-t and https://github.com/stfbk/migt, respectively. Plan of the paper. In Section OUR THREAT MODEL we propose an extended threat model based on an existing one. Then, in Section OUR APPROACH, we present our approach to support security testing. In Section TEST SPECIFICATION, we delve into the specification to define test cases. In Section USE CASES, we describe the experimental analysis on three different scenarios. In Section COMPARISON WITH AVAILABLE TOOLS we collect state-of-the-art tools covering our research. We conclude our work in Section CONCLUSIONS. 2 OUR THREAT MODEL The threat model we propose supports the automation of security tests, specified in a high-level language, for both verifying the proper implementation of BCPs and performing attacks on deployments based on IdM protocols. Additionally, the proposed threat model supports, by automating the use of structured data, security assessments and facilitates informed decision-making for cybersecurity 6https://github.com/stfbk/mig-t
Title Suppressed Due to Excessive Length 3 Fig. 1: Our extended threat model. risk management. By leveraging automation, we can expedite the analysis process and enhance result accuracy, ensuring the delivery of up-to-date and comprehensive assessments. By returning actionable hints for fixing vulnerabilities, we assist IT professionals to increase the security of IdM deployments. In Figure 1, the threat model derived from [4]7is shown in the dashed box whereas outside are the concepts of the extended threat model that are further discussed in Section OUR APPROACH. The threat model in [4] consists in identifying potential threats and vulnerabilities as well as determining the appropriate security controls to mitigate these risks. Security controls encompass a range of countermeasures implemented to secure against intentional and unintentional threats. Vulnerabilities represent implementation and configuration flaws that could be exploited by threats. Understanding the likelihood and impact of these threats is essential for effective risk management. Cyber Threat Intelligence (CTI) plays a crucial role in helping organizations identify and prioritize potential risks. Moreover, CTI aids in the development of targeted risk management strategies tailored to specific vulnerabilities, thus improving overall security posture. We then introduce an extended threat model for IdM implementations, depicted in Figure 1. Our extended threat model incorporates known attacks and BCPs outlined in the IdM standards, ensuring a comprehensive coverage of security issues. From our threat model, we derive two types of test cases. The former assess the proper implementation of security controls outlined in standards like OIDC or OAuth, facilitating automated compliance testing. The latter perform attacks to exploit known vulnerabilities, enabling automated security testing. By leveraging these test cases, it is possible to identify recurring vulnerabilities and evaluate the security posture of the system through targeted, (known) attacks. The purpose of BCPs, implemented through Security Controls, is to identify key vulnerabilities and provide structured mitigations. Security testers design test cases that assess these measures and make sure they are implemented correctly. Let us consider the test T1 aiming at checking whether the adoption of Proof Key for Code Exchange (PKCE) is in place for an OAuth/OIDC deployment. PKCE mitigates the possibility of unauthorized access to protected resources.8 7https://doi.org/10.6028/NIST.SP.800-30 8https://tools.ietf.org/html/rfc7636
4 Andrea Bisegna, Matteo Bitussi, Roberto Carbone, and Silvio Ranise Security Testers also play the role of attackers to assess the impact of vulnerabilities by performing known attacks. Let us consider the test T2, a “Code replay” attack, where the attacker intercepts and reuses the authorization response to gain access to users’ resources without their knowledge [3]. The extended threat model considers the nature of BCPs and attacks, which can change over time, offering the possibility of easily expressing and incorporating new test cases in response to a rapidly changing threat landscape. Security Testers have two options according to the type of test case they execute. The first capability pertains to verifying BCPs, by assuming “network” or “web attacker” capabilities, depending on the specific BCP being tested. For example, BCPs addressing redirect Universal Resource Identifier (URI) attacks in OAuth require the capabilities of a web attacker, while others, like securing the OAuth token exchange process, require the capabilities of a (more powerful) “network attacker.” The second option relates to executing attacks, where Security Testers have the capabilities of a “web attacker.” For instance, in the authorization code interception attack, Security Testers intercept the authorization code exchanged between the OAuth client and authorization server. This attack can be executed through phishing or exploiting vulnerabilities in the OAuth client application, allowing attackers to obtain access tokens and access protected resources. 3 OUR APPROACH According to the threat model in Figure 1, a Security Tester is responsible for creating two types of test cases: one to verify the compliance with the BCPs, and the other to perform attacks. For each test case, a Security Tester defines both a Session and a Test as reported in Figure 2, which provides an overview of our approach. The Session is similar to a UI integration test typically employed by testers of web applications.9Indeed, Session encompasses a series of user actions executed by a browser to trigger the HTTP messages required for a Test, enabling our approach to simulate user interactions and gather information on the web application’s response. The Test, written in MIG-L, a formal and concise declarative language for security testing, consists of a sequence of operations aimed at managing and manipulating HTTP messages and Session, as well as integrating an oracle automating the criterion against which the outcome of a test can be evaluated. MIG-L is designed to be versatile and adaptable across all web digital identity protocols, as its underlying principles and structure are sufficiently generic to support them. To ensure this flexibility, MIG-L enables security testers to define tests for any web digital identity protocol by specifying relevant parameters and interactions. A Test can be passive or active. The former involves analyzing the intercepted HTTP messages statically, without any interaction (saving a value of a parameter) or modification of the HTTP messages during the execution of the Session. An active test allows for interactions during the execution of the Session. By automating the execution of the test 9https://www.divami.com/blog/selenium-guide-to-automated-ui-testing/
Title Suppressed Due to Excessive Length 5 Fig. 2: High level view of our approach. case, a Security Tester can rapidly and precisely evaluate the security of the IdM implementation. As depicted in Figure 2, the Test Handler is responsible for interpreting and executing the test specified in MIG-L, and it triggers, when needed, the Session Handler, which processes the Session and replicates the user actions within a browser. All HTTP messages pass through (and may be intercepted by) a Proxy. The Proxy Interaction component manages the communication with the Proxy to enforce the conditions specified in the Test. Finally, the Reporting component provides output detailing identified vulnerabilities and suggestions for appropriate security controls, aiding Security Testers and stakeholders in understanding and addressing the results of the tests, thus paving the way to cybersecurity risk management. To define an architecture for the execution of security tests specified in MIGL, we define three distinct APIs used by components independently of the underlying technology. These APIs—the Browser API, Proxy API, and Session API—support the automated execution of user actions, interception and manipulation of messages, and management of test session executions, respectively. They streamline the testing process and enhance the flexibility and usability of our approach. 4 TEST SPECIFICATION MIG-L is a declarative language for security testing, encompassing many command combinations for manipulating HTTP messages or interacting with the Session. One of the key strengths of MIG-L is its user-friendly nature. The language is designed to be highly expressive yet intuitive, making it accessible to security testers with limited programming experience. The declarative nature of MIG-L allows testers to specify test scenarios in a concise manner without delving into complex scripting or programming. To further simplify the process, we provide a library of pre-defined test templates for common test patterns, which
6 Andrea Bisegna, Matteo Bitussi, Roberto Carbone, and Silvio Ranise can be easily adapted to specific protocols and implementations. Additionally, MIG-L can be used to generate tests for other types of testing, including triggering additional security tests for the implementation, such as fuzzing, though this is not considered in this work. To illustrate the flexibility of this language we present two test cases, T1 and T2. These examples correspond to the BCP and attack cases described in Section OUR THREAT MODEL. Our approach, as defined in Section OUR APPROACH, requires two inputs: the Test specified in MIG-L and the Session. The Session depicted in Listing 1.1 and required for both tests (T1 and T2) is a Selenium script that executes the OIDC flow in the spid-cie-oidc-django10 implementation based on the SPID/CIE OIDC. The commands inherited by the Selenium script are highlighted in red, while comments are in blue. Listing 1.1: Session s1 used both in T1 and T2. 1open | http :// relying - party . org :8001/ oidc / rp / landing | $$ // access SP webpage$$ 2click | xpath =/ html/ body/ div [2]/ div/span [2]/ a | $$ // press login button$$ 3click | xpath =/ html /body /div [2]/ ul/li [2]/a | $$ // choose IdP$$ 4type | id= username | user $$ // insert user$$ 5type | id= password | oidcuser $$ // insert password$$ 6click | xpath =/ html/ body/ div [2]/ div [3]/ button /span [2] | $$ // press login button$$ 7click | id= agree | $$ // provide consent$$ The first test T1 we analyze, specified in Listing 1.2, concerns compliance with the BCP in OAuth, specifically focusing on the adoption of PKCE. This test intercepts the authorization request and verifies the presence of code_challenge and code_verifier in the URL. The commands start_test and end_test mark the beginning (Line 1) and end (Line 11) of the test, respectively. The start_test command requires the test name and description, the test type (either passive or active), the set of (references to) Sessions (only s1 for T1). The command start (at Line 2) indicates that the Session s1 is executed. The commands start_msg_operation and end_msg_operation mark the beginning (Line 3) and the end (Line 10) of the HTTP message operations to be executed within the test, respectively. The commands start_checks and end_checks identify the beginning (Line 4) and end (Line 6) of an operation in charge of verifying the presence of a parameter, respectively. In this case we detect the presence of the code_challenge parameter in the URL of the authorization request. The authorization_request is defined as the HTTP request where the URL contains the response_type and client_id parameters. Similarly to Lines 4-6, the commands in Lines 7-9 verify the presence of the parameter code_verifier in the URL of the token request. The token_request 10 https://github.com/italia/spid-cie-oidc-django/
Title Suppressed Due to Excessive Length 7 is defined as the HTTP request where the URL contains grant_type,code, redirect_uri, and client_id. Listing 1.2: MIG-L test for T1 (passive). 1start_test ( Verify presence of PKCE , The test verify the presence of code_challenge and code_verifier , passive , { s1 }) $$ // passive test$$ 2start ( s1 ) $$ // run s1$$ 3start_msg_operation () $$// start of message operation$$ 4start_checks ( authorization_request ) $$ // start checks in authorization_request$$ 5check ( code_challenge , is present , url) $$ // verify the presence of code_challenge in url$$ 6end_checks () 7start_checks ( token_request ) $$// start checks in token_request$$ 8check ( code_verifier , is present , url) $$ // verify the presence of code_verifier in url$$ 9end_checks () 10 end_msg_operation () $$ // end of message operation$$ 11 end_test () $$ // end of passive test$$ The second test T2 we show, specified in Listing 1.3, performs the code replay attack in [3]. The steps of this attack involve intercepting the code parameter during the execution of the OIDC flow and then reusing it in a new flow. As said above, the Session s1 for T2 is identical to the one used in T1. Another Session (s1_copy) is responsible for reusing the code parameter in a new flow, and T2 automatically generates s1_copy by duplicating s1. The commands at Line 1 and 15 indicate the start and finish of the test, respectively. Unlike the test in Listing 1.2, we have defined an active test and provided two Sessions (s1 and s1_copy). For active tests, another information must be included, namely the expected test result. In this case, it is incorrect flow s1_copy, meaning that the test is passed if the flow of s1_copy is incorrect, i.e. the execution fails. Indeed, if all the user actions in s1_copy are successfully executed, it means that the attack is successful and thus the test is considered failed. The command save (at Line 2) indicates that all the user actions reported from the command track[M0,ML], where M0 represents the first user action and ML represents the last user action reported in Session s1, are saved in s1_copy. The command start (at Line 3) indicates that the Session s1 is executed. The commands start_test_operation and end_test_operation (at Lines 4 and 8, respectively) define which HTTP message to intercept and the action to take once intercepted. All the operations between Lines 5 and 7 will be applied to the HTTP message. In this case, the HTTP message to intercept is the authorization_response in s1, and once intercepted, it must be dropped. This means inducing an error in the execution and thus halting the execution of s1. The authorization_response is defined as the HTTP response with code and state in the URL.
8 Andrea Bisegna, Matteo Bitussi, Roberto Carbone, and Silvio Ranise The commands start_msg_operation and end_msg_operation identify the beginning (Line 5) and end (Line 7) of an operation in charge of saving the value of a parameter, respectively. In this case, we identify the value of the parameter code in the URL and save it to a new variable called saved_code. The command start (at Line 9) indicates that the Session s1_copy is executed. Similarly to Lines 4 and 8, with the command start_test_operation and end_test_operation (at Lines 10 and 14, respectively), we want to intercept the authorization_response message from s1_copy without dropping the HTTP message, allowing the execution of the remaining user actions specified in s1_copy. The commands start_msg_operation and end_msg_operation (at Lines 11 and 13, respectively) replace the value of the code parameter in the URL with that in saved_code. Listing 1.3: MIG-L test for T2 (active). 1start_test (Code replay attack , The test intercepts the code in the authorization response and replay it in another authorization response , active , {s1 , s1_copy }, incorrect flow s1_copy ) $$ // active test$$ 2save ( s1_copy , track [M0 , ML ], s1) $$ // copy all the user actions from s1 to s1_copy$$ 3start ( s1 ) $$ // run s1$$ 4start_test_operation ( authorization_response , s1 , drop ) $$ // drop authorization_response message generated in s1 $$ 5start_msg_operation () $$ // begin message operation$$ 6save_parameter ( code , saved_code , url ) $$ // save parameter code from url and store it as saved_code$$ 7end_msg_operation () $$ // end message operation$$ 8end_test_operation () $$ // end test operation$$ 9start ( s1_copy ) $$ // run s1_copy$$ 10 start_test_operation ( authorization_response , s1_copy , intercept ) $$ // intercept authorization_response message from s1_copy $$ 11 start_msg_operation () $$ // begin message operation$$ 12 edit_parameter ( code , saved_code , url ) $$ // edit code parameter from url with saved_code$$ 13 end_msg_operation () $$ // end message operation$$ 14 end_test_operation () $$ // end test operation$$ 15 end_test () $$ // end of active test$$ With our language, it is also possible to execute multiple tests simultaneously using the same Session. For this, we have introduced the ability to define a test suite, which consists of an object comprising a collection of tests, using the command define_suite. This command specifies (i) name - the label assigned to the suite, and (ii) description - the descriptive annotation allocated to it. Once the test suite is defined, tests can be defined. Additionally, MIG-L can be used to generate tests for detecting other types of vulnerabilities (e.g., those detectable by fuzzing). Although we do not further elaborate on this point, we mention that it is not difficult to specify a test case
Title Suppressed Due to Excessive Length 9 in MIG-L to detect a recently disclosed vulnerability in a largely used OAuth deployment that, paired with cross-site scripting (XSS) flaws, enables account takeovers in more than a million websites.11 5 IMPLEMENTATION We have implemented our approach in Micro-Id-Gym [5] by extending MIG-T, a plugin to support pentesting activities in IdM implementations. Based on the Burp web proxy,12 MIG-T offers a comprehensive set of APIs to interact with, including those defined in Section OUR APPROACH. The three APIs available in MIG-T are the Browser API, Proxy API, and Session API and are instances of those depicted in Figure 2. The Browser API allows for the automated execution of user actions defined in a Session. For example, it provides the driver.get(URL)method to open a specific URL in the browser. The Proxy API is used to intercept and manipulate an HTTP Message. For instance, the HttpRequestResponse.getRequest() method can retrieve intercepted messages. Finally, the Session API manages Session executions. For example, the start(Session)method creates a new thread object to run a specified Session. 6 USE CASES We illustrate three applications of MIG-T that highlight its versatility and effectiveness by conducting the security analysis in (S1) the SPID/CIE OIDC deployment in Developers Italia, (S2) an OAuth deployment for a PSD2 service, and (S3) 48 pairs of SP-IdP supporting SSO-based Account Linking. For all the experiments reported in the following, we use JSON as a concrete syntax of MIG-L as described in Section TEST SPECIFICATION. The reasons underlying this choice are practical, namely to simplify the development of the parser and interpreter of the language. We will soon implement a parser from the syntax presented in this work to the JSON syntax. 6.1 S1. SPID/CIE OIDC Deployment in Developers Italia In the context of a long term collaboration with the Italian Government Printing Office and Mint (Istituto Poligrafico e Zecca dello Stato, IPZS), we contributed to the development of an extensive corpus of compliance and security tests for deployments of the SPID/CIE OIDC,13 the national digital identity solution based on the OIDC standard and leveraging the Italian electronic identity card (Carta d’Identità Elettronica, CIE). The collection of the test cases has been made available on the Github web site (at https://github.com/stfbk/mig/tree/master/testplans/spidcie-oidc/implementations/spid-cie-oidc-django/input/mig-t) which offers resources 11 https://salt.security/blog/over-1-million-websites-are-at-risk-of-sensitiveinformation-leakage—xss-is-dead-long-live-xss 12 https://portswigger.net/burp/documentation/desktop/tools/proxy 13 https://docs.italia.it/italia/spid/spid-cie-oidc-docs
16 Andrea Bisegna, Matteo Bitussi, Roberto Carbone, and Silvio Ranise another distinctive feature of MIG-T. The column IdM is not very relevant to general purpose tools and becomes crucial for all those in the remaining categories. By contrasting columns IdM with column Compl, it becomes clear that only 3 out of 20 tools (i.e. not considering the 5 in General purpose) can verify compliance and checks for IdM vulnerabilities (the OauthTester [14] cannot perform either activities as it is only able to flag protocol executions that deviate from those specified in the OAuth RFC document). This means that most tools are focused on just one activity between vulnerability detection and compliance checking, contrary to MIG-T which naturally supports both again because of its extended threat model. The columns Active and Passive clearly show that almost all tools support just one type of tests with two notable exceptions, namely the BRM Analyzer [15] (classified as OAuth/OIDC and SAML) that supports none, as it requires manual inspections of the reports produced from SSO protocol traces to detect vulnerabilities, and OAuch [11] that supports both. As discussed above, MIG-T supports both types of tests not only for OAuth/OIDC as OAuch but also for SAML. 8 CONCLUSIONS We presented a declarative and automated approach to test the security of IdM protocols, which are essential building blocks for securing online services and whose deployments are plagued by a consistent number of vulnerabilities despite various standardization efforts including SAML, OAuth, and OIDC. Experiments on real deployments (including a national digital identity system, a PSD2 payment service, and a number of SSOLinking solutions in web applications) confirm that automation is crucial for scalability and declarativity for considering new vulnerabilities in a rapidly evolving threat landscape. 9 ACKNOWLEDGMENTS This work has been partially funded by (i) the project SERICS (PE00000014) under the MUR National Recovery and Resilience Plan funded by the European Union — NextGenerationEU, and (ii) the joint laboratory between Fondazione Bruno Kessler (FBK) and the Italian Government Printing Office and Mint, Italy (Istituto Poligrafico e Zecca dello Stato, IPZS). The work of Silvio Ranise has also been supported by the Italian Ministry of University’s PRIN 2022 program under the “Post quantum Identification and Encryption Primitives: Design and Realization (POINTER)” (2022M2JLF2) project funded by the European Union — NextGenerationEU. We would like to thank the anonymous reviewers for their valuable comments that help us to improve the quality of the paper, and to Luca Compagna and Alessandro Biasi for their support and insights about MIG-L.
Title Suppressed Due to Excessive Length 17 References 1. A. Bisegna, M. Bitussi, R. Carbone, L. Compagna, A. Sudhodanan, and S. Ranise, “CSRF-ing the SSO waves: security testing of SSO-based account linking process”, 2024 IEEE European symposium on security and privacy (EuroS&P), 2024. 2. A. Bisegna, R. Carbone, G. Pellizzari, and S. Ranise, “Micro-Id-Gym: A Flexible Tool for Pentesting Identity Management Protocols in the Wild and in the Laboratory”, In International Workshop on Emerging Technologies for Authorization and Authentication (pp. 71-89). Cham: Springer International Publishing, 2020. 3. F. Yang, and S. Manoharan, “A security analysis of the OAuth protocol”, 2013 IEEE Pacific Rim Conference on Communications, Computers and Signal Processing (PACRIM), 2013. 4. M.S. Toosarvandani, N. Modiri, and M. Afzali. “The risk assessment and treatment approach in order to provide LAN security based on ISMS standard”, 2012 arXiv preprint arXiv:1301.1578, 2012. 5. A. Bisegna, R. Carbone, I. Martini, V. Odorizzi, G. Pellizzari, and S. Ranise, “MicroId-Gym: Identity Management Workouts with Container-Based Microservices”, International Journal of Information Security and Cybercrime 8, pp. 45–50, 2019. 6. A. Carmel, “Traveling with OAuth - Account Takeover on Booking.com”, 2023, https://salt.security/blog/traveling-with-oauth-account-takeover-on-booking-com. 7. N. Engelbertz, N. Erinola, D. Herring, J. Somorovsky, V. Mladenov, and J. Schwenk, “Security Analysis of eIDAS–the Cross-Country Authentication Scheme in Europe”, 12th USENIX Workshop on Offensive Technologies (WOOT 18), 2018. 8. C. Mainka, J. Somorovsky, and J. Schwenk, “Penetration testing tool for web services security”, 2012 IEEE Eighth World Congress on Services, 2012. 9. V. Prasad, and S. Shukla, “SAML Raider: A Burp Suite Extension for SAML Security Testing”, 2018 17th IEEE International Conference On Trust, Security And Privacy In Computing And Communications/12th IEEE International Conference On Big Data Science And Engineering, 2018. 10. G. Bai, J. Lei, G. Meng, S. Sathyanarayan Venkatraman, P. Saxena, J. Sun, Y. Liu, and J. Song Dong, “AUTHSCAN: Automatic Extraction of Web Authentication Protocols from Implementations”, Proceedings of the 20th Annual Network and Distributed System Security Symposium, 2013. 11. P. Philippaerts, D. Preuveneers, and W. Joosen, “OAuch: Exploring Security Compliance in the OAuth 2.0 Ecosystem”, Proceedings of the 25th International Symposium on Research in Attacks, Intrusions and Defenses, 2022. 12. A. Bisegna, R. Carbone, and S. Ranise, “Micro-Id-Gym: A Flexible Tool for Pentesting Identity Management Protocols in the Wild and in the Laboratory”, In International Workshop on Emerging Technologies for Authorization and Authentication, 2021. 13. A. Sudhodanan, R. Carbone, L. Compagna, N. Dolgin, A. Armando, and U. Morelli, “Large-scale analysis & detection of authentication cross-site request forgeries”, 2017 IEEE European symposium on security and privacy (EuroS&P), 2017. 14. R. Yang, G. Li, W. Cheong Lau, K. Zhang and P. Hu, “Model-based security testing: An empirical study on OAuth 2.0 implementations”, Proceedings of the 11th ACM on Asia Conference on Computer and Communications Security, 2016. 15. R. Wang, S. Chen and X. Wang, “Signing me onto your accounts through Facebook and Google: A traffic-guided security study of commercially deployed Single-SignOn web services”, 2012 IEEE Symposium on Security and Privacy, 2012.