Formally-verified Security against Forgery of Remote Attestation using SSProve

• URL: http://arxiv.org/abs/2502.17653v2
• Date: Mon, 14 Jul 2025 07:36:02 GMT
• Title: Formally-verified Security against Forgery of Remote Attestation using SSProve
• Abstract summary: This paper presents the first mechanized formalization of the fundamental security properties of RA.<n>We first define digital signatures and formally verify security against forgery in the strong existential attack model.<n>Our development provides evidence that the RA protocol is secure against forgery.
• Score: 0.21427777919040417
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Remote attestation (RA) is the foundation for trusted execution environments in the cloud and trusted device driver onboarding in operating systems. However, RA misses a rigorous mechanized definition of its security properties in one of the strongest models, i.e., the semantic model. Such a mechanization requires the concept of StateSeparating Proofs (SSP). However, SSP was only recently implemented as a foundational framework in the Rocq Prover. Based on this framework, this paper presents the first mechanized formalization of the fundamental security properties of RA. Our Rocq Prover development first defines digital signatures and formally verifies security against forgery in the strong existential attack model. Based on these results, we define RA and reduce the security of RA to the security of digital signatures. Our development provides evidence that the RA protocol is secure against forgery. Additionally, we extend our reasoning to the primitives of RA and reduce their security to the security of the primitives of the digital signatures.

Related papers

• Provably Secure Agent Guardrail [89.79561918065122]
  Existing defense architectures rely on empirical semantic guardrails and probabilistic large model adjudicators.<n>This paper proposes a new security paradigm for agents based on the fundamental limitations of logical reasoning.
  arXiv  Detail & Related papers  (2026-05-28T02:12:41Z)
• ACIArena: Toward Unified Evaluation for Agent Cascading Injection [47.48169234218755]
  ACIArena is a framework for evaluating the robustness of Multi-Agent Systems.<n>It offers evaluation suites spanning multiple attack surfaces and attack objectives.<n>It covers six widely used MAS implementations and provides a benchmark of 1,356 test cases.
  arXiv  Detail & Related papers  (2026-04-09T04:03:13Z)
• Mitigating Safety Tax via Distribution-Grounded Refinement in Large Reasoning Models [63.368505631152594]
  Safety alignment incurs safety tax that perturbs a large reasoning model's (LRM) general reasoning ability.<n>Existing datasets used for safety alignment for an LRM are usually constructed by distilling safety reasoning traces and answers from an external LRM or human labeler.<n>We propose a safety alignment dataset construction method, dubbed DGR. DGR transforms and refines an existing out-of-distributional safety reasoning dataset to be aligned with the target's LLM inner distribution.
  arXiv  Detail & Related papers  (2026-02-02T14:18:48Z)
• Robustness Certificates for Neural Networks against Adversarial Attacks [9.365069861121944]
  This paper introduces a principled formal robustness certification framework that models gradient-based training as a discrete-time dynamical system.<n>Our framework also extends to certification against test-time attacks, making it the first unified framework to provide formal guarantees in both training and test-time attack settings.
  arXiv  Detail & Related papers  (2025-12-24T00:49:47Z)
• Signing Right Away [0.0]
  Signing Right Away (SRA) is a comprehensive security architecture that guarantees the provenance of digital media.<n>SRA ensures that every captured image and video carries an immutable, verifiable proof of origin.
  arXiv  Detail & Related papers  (2025-10-07T11:56:56Z)
• ReliabilityRAG: Effective and Provably Robust Defense for RAG-based Web-Search [69.60882125603133]
  We present ReliabilityRAG, a framework for adversarial robustness that explicitly leverages reliability information of retrieved documents.<n>Our work is a significant step towards more effective, provably robust defenses against retrieved corpus corruption in RAG.
  arXiv  Detail & Related papers  (2025-09-27T22:36:42Z)
• Fortifying the Agentic Web: A Unified Zero-Trust Architecture Against Logic-layer Threats [1.3029461861316425]
  This paper presents a Unified Security Architecture that fortifies the Agentic Web through a Zero-Trust IAM framework.<n>This architecture is built on a foundation of rich, verifiable agent identities using Decentralized IDs (DIDs) and Verifiable Credentials (VCs)<n>Security is operationalized through a multi-layered Trust Fabric.
  arXiv  Detail & Related papers  (2025-08-17T06:52:39Z)
• Provably Secure Retrieval-Augmented Generation [7.412110686946628]
  This paper proposes the first provably secure framework for Retrieval-Augmented Generation (RAG) systems.<n>Our framework employs a pre-storage full-encryption scheme to ensure dual protection of both retrieved content and vector embeddings.
  arXiv  Detail & Related papers  (2025-08-01T21:37:16Z)
• ARMOR: Aligning Secure and Safe Large Language Models via Meticulous Reasoning [49.47193675702453]
  Large Language Models (LLMs) have demonstrated remarkable generative capabilities.<n>LLMs remain vulnerable to malicious instructions that can bypass safety constraints.<n>We propose a reasoning-based safety alignment framework, ARMOR, that replaces the ad-hoc chains of thought reasoning process with human-aligned, structured one.
  arXiv  Detail & Related papers  (2025-07-14T09:05:54Z)
• Towards Provable (In)Secure Model Weight Release Schemes [5.177249919642388]
  Recent secure weight release schemes claim to enable open-source model distribution while protecting model ownership and preventing misuse.<n>These approaches lack rigorous security foundations and provide only informal security guarantees.<n>Inspired by established works in cryptography, we formalize the security of weight release schemes by introducing several concrete security definitions.
  arXiv  Detail & Related papers  (2025-06-23T11:57:41Z)
• LLM Agents Should Employ Security Principles [60.03651084139836]
  This paper argues that the well-established design principles in information security should be employed when deploying Large Language Model (LLM) agents at scale.<n>We introduce AgentSandbox, a conceptual framework embedding these security principles to provide safeguards throughout an agent's life-cycle.
  arXiv  Detail & Related papers  (2025-05-29T21:39:08Z)
• SVAFD: A Secure and Verifiable Co-Aggregation Protocol for Federated Distillation [10.234754822281774]
  We propose SVAFD, the first protocol specifically designed for Federated Distillation (FD)<n>A multilateral co-aggregation method redefines the responsibilities of clients and server.<n> SVAFD is resilient to stragglers and colluding clients, making it well-suited for dynamic networks in real-world applications.
  arXiv  Detail & Related papers  (2025-05-19T16:30:27Z)
• Privacy-Aware RAG: Secure and Isolated Knowledge Retrieval [7.412110686946628]
  This paper proposes an advanced encryption methodology designed to protect RAG systems from unauthorized access and data leakage. Our approach encrypts both textual content and its corresponding embeddings prior to storage, ensuring that all data remains securely encrypted. Our findings suggest that integrating advanced encryption techniques into the design and deployment of RAG systems can effectively enhance privacy safeguards.
  arXiv  Detail & Related papers  (2025-03-17T07:45:05Z)
• Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
  We propose Authenticated Cyclic Redundancy Integrity Check (ACRIC) ACRIC preserves backward compatibility without requiring additional hardware and is protocol agnostic. We show that ACRIC offers robust security with minimal transmission overhead ( 1 ms)
  arXiv  Detail & Related papers  (2024-11-21T18:26:05Z)
• VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL [4.652188875442064]
  CHERI provides and enforces fine-grained memory protection directly in the hardware. VeriCHERI is conceptionally different from previous works in that it does not require any ISA specification. We demonstrate the effectiveness and scalability of VeriCHERI on a RISC-V based processor implementing a CHERI variant.
  arXiv  Detail & Related papers  (2024-07-26T11:48:55Z)
• On the Design and Security of Collective Remote Attestation Protocols [5.01030444913319]
  Collective remote attestation (CRA) is a security service that aims to efficiently identify compromised devices in a (heterogeneous) network. The last few years have seen an extensive growth in CRA protocol proposals, showing a variety of designs guided by different network topologies. We present Catt, a unifying framework for CRA protocols that enables them to be compared systematically.
  arXiv  Detail & Related papers  (2024-07-12T12:06:49Z)
• Generalized Quantum-assisted Digital Signature [2.187441808562386]
  This paper introduces an improved version of a recently proposed scheme whose information theoretic security is inherited by adopting QKD keys for digital signature purposes. Its security against forging is computed considering a trial-and-error approach taken by the malicious forger and GQaDS parameters are optimized via an analytical approach balancing between forgery and repudiation probabilities.
  arXiv  Detail & Related papers  (2024-06-28T15:04:38Z)
• Towards Credential-based Device Registration in DApps for DePINs with ZKPs [46.08150780379237]
  We propose a credential-based device registration (CDR) mechanism that verifies device credentials on the blockchain. We present a general system model, and technically evaluate CDR using zkSNARKs with Groth16 and Marlin.
  arXiv  Detail & Related papers  (2024-06-27T09:50:10Z)
• Poisoning Prevention in Federated Learning and Differential Privacy via Stateful Proofs of Execution [8.92716309877259]
  Federated Learning (FL) and Local Differential Privacy (LDP) have attracted much attention over the past few years.<n>They share the common limitation of being vulnerable to poisoning attacks.<n>We propose a system-level approach to remedy this issue based on a novel security notion of Proofs of Stateful Execution.
  arXiv  Detail & Related papers  (2024-04-10T04:18:26Z)
• A Zero Trust Framework for Realization and Defense Against Generative AI Attacks in Power Grid [62.91192307098067]
  This paper proposes a novel zero trust framework for a power grid supply chain (PGSC) It facilitates early detection of potential GenAI-driven attack vectors, assessment of tail risk-based stability measures, and mitigation of such threats. Experimental results show that the proposed zero trust framework achieves an accuracy of 95.7% on attack vector generation, a risk measure of 9.61% for a 95% stable PGSC, and a 99% confidence in defense against GenAI-driven attack.
  arXiv  Detail & Related papers  (2024-03-11T02:47:21Z)
• 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)
• Tamper-Evident Pairing [55.2480439325792]
  Tamper-Evident Pairing (TEP) is an improvement of the Push-Button configuration (PBC) standard. TEP relies on the Tamper-Evident Announcement (TEA), which guarantees that an adversary can neither tamper a transmitted message without being detected, nor hide the fact that the message has been sent. This paper provides a comprehensive overview of the TEP protocol, including all information needed to understand how it works.
  arXiv  Detail & Related papers  (2023-11-24T18:54:00Z)
• Ring-A-Bell! How Reliable are Concept Removal Methods for Diffusion Models? [52.238883592674696]
  Ring-A-Bell is a model-agnostic red-teaming tool for T2I diffusion models. It identifies problematic prompts for diffusion models with the corresponding generation of inappropriate content. Our results show that Ring-A-Bell, by manipulating safe prompting benchmarks, can transform prompts that were originally regarded as safe to evade existing safety mechanisms.
  arXiv  Detail & Related papers  (2023-10-16T02:11:20Z)

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.