Ante Đerek | Searcharxiv

arXiv2026

Towards automated formal security analysis of SAML V2.0 Web Browser SSO standard -- the POST/Artifact use case

Single Sign-On (SSO) protocols streamline user authentication with a unified login for multiple online services, improving usability and security. One of the most common SSO protocol frameworks - the Security Assertion Markup Language V2.0 (SAML) Web SSO Profile - has been in use for more than two decades, primarily in government, education and enterprise environments. Despite its mission-critical nature, only certain deployments and configurations of the Web SSO Profile have been formally analyzed. This paper attempts to bridge this gap by performing a comprehensive formal security analysis of the SAML V2.0 SP-initiated SSO with POST/Artifact Bindings use case. Rather than focusing on a specific deployment and configuration, we closely follow the specification with the goal of capturing many different deployments allowed by the standard. Modeling and analysis is performed using Tamarin prover - state-of-the-art tool for automated verification of security protocols in the symbolic model of cryptography. Technically, we build a meta-model of the use case that we instantiate to eight different protocol variants. Using the Tamarin prover, we formally verify a number of critical security properties for those protocol variants, while identifying certain drawbacks and potential vulnerabilities.

cs.CR↗

arXiv2022

Automatically generating models of IT systems

Information technology system (ITS), informally, consists of hardware and software infrastructure (e.g., workstations, servers, laptops, installed software packages, databases, LANs, firewalls, etc.), along with physical and logical connections and inter-dependencies between various items. Nowadays, every company owns and operates an ITS, but detailed information about the system is rarely publicly available. However, there are many situations where the availability of such data would be beneficial. For example, cyber ranges need descriptions of complex realistic IT systems in order to provide an effective training and education platform. Furthermore, various algorithms in cybersecurity, in particular attack tree generation, need to be validated on realistic models of IT systems. In this paper, we describe a system we call the Generator that, based on the high-level requirements such as the number of employees and the business area the target company belongs to, generates a model of an ITS that satisfies the given requirements. We put special emphasis on the following two criteria: the generated ITS models a large amount of details, and ideally resembles a real system. Our survey of related literature found no sufficiently similar prior works, so we believe that this is the first attempt of building something like this. We created a proof-of-concept implementation of the Generator, validated it by generating ITS models for a simplified fictional financial institution, and analyzed the Generators performance with respect to the problem size. The research was done in an iterative manner, with coauthors continuously providing feedback on intermediate results. (...) We intend to extend this prototype to allow probabilistic generation of IT systems when only a subset of parameters is explicitly defined, and further develop and validate our approach with the help of domain experts.

cs.CR↗