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

• URL: http://arxiv.org/abs/2403.11859v1
• Date: Mon, 18 Mar 2024 15:11:29 GMT
• Title: Towards automated formal security analysis of SAML V2.0 Web Browser SSO standard - the POST/Artifact use case
• Authors: Zvonimir Hartl, Ante Đerek,
• Abstract summary: 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. Single Sign-On (SSO) protocols streamline user authentication with a unified login for multiple online services, improving. usability and security.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: 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.

Related papers

• DoomArena: A framework for Testing AI Agents Against Evolving Security Threats [84.94654617852322]
  We present DoomArena, a security evaluation framework for AI agents. It is a plug-in framework and integrates easily into realistic agentic frameworks. It is modular and decouples the development of attacks from details of the environment in which the agent is deployed.
  arXiv  Detail & Related papers  (2025-04-18T20:36:10Z)
• OmniParser V2: Structured-Points-of-Thought for Unified Visual Text Parsing and Its Generality to Multimodal Large Language Models [58.45517851437422]
  Visually-situated text parsing (VsTP) has recently seen notable advancements, driven by the growing demand for automated document understanding. Existing solutions often rely on task-specific architectures and objectives for individual tasks. In this paper, we introduce Omni V2, a universal model that unifies VsTP typical tasks, including text spotting, key information extraction, table recognition, and layout analysis.
  arXiv  Detail & Related papers  (2025-02-22T09:32:01Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  We introduce a benchmark to assess the ability of Large Language Models to autonomously identify vulnerabilities in new cryptographic protocols. We created a dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents.
  arXiv  Detail & Related papers  (2024-11-20T14:16:55Z)
• Misbinding Raw Public Keys to Identities in TLS [1.821556502071398]
  This paper examines the security of TLS when using Raw Public Key (RPK) authentication. This mode has not been as extensively studied as X.509 certificates and Pre-Shared Keys (PSK) We develop a formal model of TLS RPK using applied pi calculus and the ProVerif verification tool, revealing that the RPK mode is susceptible to identity misbinding attacks.
  arXiv  Detail & Related papers  (2024-11-14T19:28:09Z)
• SecCodePLT: A Unified Platform for Evaluating the Security of Code GenAI [47.11178028457252]
  We develop SecCodePLT, a unified and comprehensive evaluation platform for code GenAIs' risks. For insecure code, we introduce a new methodology for data creation that combines experts with automatic generation. For cyberattack helpfulness, we construct samples to prompt a model to generate actual attacks, along with dynamic metrics in our environment.
  arXiv  Detail & Related papers  (2024-10-14T21:17:22Z)
• Excavating Vulnerabilities Lurking in Multi-Factor Authentication Protocols: A Systematic Security Analysis [2.729532849571912]
  Single-factor authentication (SFA) protocols are often bypassed by side-channel and other attack techniques. To alleviate this problem, multi-factor authentication (MFA) protocols have been widely adopted recently.
  arXiv  Detail & Related papers  (2024-07-29T23:37:38Z)
• SAM-CP: Marrying SAM with Composable Prompts for Versatile Segmentation [88.80792308991867]
  Segment Anything model (SAM) has shown ability to group image pixels into patches, but applying it to semantic-aware segmentation still faces major challenges. This paper presents SAM-CP, a simple approach that establishes two types of composable prompts beyond SAM and composes them for versatile segmentation. Experiments show that SAM-CP achieves semantic, instance, and panoptic segmentation in both open and closed domains.
  arXiv  Detail & Related papers  (2024-07-23T17:47:25Z)
• EmInspector: Combating Backdoor Attacks in Federated Self-Supervised Learning Through Embedding Inspection [53.25863925815954]
  Federated self-supervised learning (FSSL) has emerged as a promising paradigm that enables the exploitation of clients' vast amounts of unlabeled data. While FSSL offers advantages, its susceptibility to backdoor attacks has not been investigated. We propose the Embedding Inspector (EmInspector) that detects malicious clients by inspecting the embedding space of local models.
  arXiv  Detail & Related papers  (2024-05-21T06:14:49Z)
• Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
  SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems.
  arXiv  Detail & Related papers  (2024-05-09T19:57:59Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• A Novel Approach To User Agent String Parsing For Vulnerability Analysis Using Mutli-Headed Attention [3.3029515721630855]
  A novel methodology for parsing UASs using Multi-Headed Attention Based transformers is proposed. The proposed methodology exhibits strong performance in parsing a variety of UASs with differing formats. A framework to utilize parsed UASs to estimate the vulnerability scores for large sections of publicly visible IT networks or regions is also discussed.
  arXiv  Detail & Related papers  (2023-06-06T14:49:25Z)
• FedSOV: Federated Model Secure Ownership Verification with Unforgeable Signature [60.99054146321459]
  Federated learning allows multiple parties to collaborate in learning a global model without revealing private data. We propose a cryptographic signature-based federated learning model ownership verification scheme named FedSOV.
  arXiv  Detail & Related papers  (2023-05-10T12:10:02Z)
• Secure access system using signature verification over tablet PC [62.21072852729544]
  We describe a highly versatile and scalable prototype for Web-based secure access using signature verification. The proposed architecture can be easily extended to work with different kinds of sensors and large-scale databases.
  arXiv  Detail & Related papers  (2023-01-11T11:05:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.