Formal Verification of Probing Security via Conditional Independence

• URL: http://arxiv.org/abs/2605.23316v2
• Date: Mon, 25 May 2026 09:31:47 GMT
• Title: Formal Verification of Probing Security via Conditional Independence
• Abstract summary: Side-channel attacks are a major threat to the security of cryptosystems.<n>Masking is a widely used countermeasure against such attacks, but proving the security of masked algorithms is error-prone without formal verification.<n>We propose a novel approach to formal verification of noninterference properties of masked algorithms based on probabilistic separation logic.
• Score: 0.14323566945483493
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Side-channel attacks are a major threat to the security of cryptosystems. Masking is a widely used countermeasure against such attacks, but proving the security of masked algorithms is error-prone without formal verification. In this work, we propose a novel approach to formal verification of noninterference properties of masked algorithms based on probabilistic separation logic. By establishing a connection between noninterference and conditional independence, we show how noninterference can be verified using Lilac, a separation logic for conditional independence. We also provide several proof rules that facilitate the verification of probing security and demonstrate their application to example algorithms.

Related papers

• Cryptographic certificates of validity for trustworthy AI [0.0]
  We propose cryptographic certificates of validity for agentic AI systems.<n>An agent's action can be accompanied by an independently checkable proof that it satisfies an agreed formal policy.
  arXiv  Detail & Related papers  (2026-06-22T16:42:25Z)
• 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)
• Rigorous Security Proofs for Practical Quantum Key Distribution [0.0]
  This thesis is concerned with rigorous security analyses of Quantum Key Distribution (QKD) protocols.<n>We establish a security proof for variable-length QKD protocols against IID collective attacks, and extend this result to coherent attacks using the postselection technique.<n>Second, we develop a method to bound phase error rates in entropic uncertainty relation-based and phase error rate-based proofs, using only the observed statistics of the protocol.<n>Third, we present a very general security analysis based on the marginal-constrained entropy accumulation theorem.
  arXiv  Detail & Related papers  (2026-04-23T15:48:02Z)
• Protecting Context and Prompts: Deterministic Security for Non-Deterministic AI [0.0]
  Large Language Model (LLM) applications are vulnerable to prompt injection and context manipulation attacks.<n>We introduce two novel primitives--authenticated prompts and authenticated context--that provide cryptographically verifiable provenance.<n>We formalize a policy algebra with four proven theorems providing protocol-level Byzantine resistance.
  arXiv  Detail & Related papers  (2026-02-11T03:38:59Z)
• VeriLLM: A Lightweight Framework for Publicly Verifiable Decentralized Inference [3.8760740008451156]
  We introduce VeriLLM, a publicly verifiable protocol for decentralized language models (LLMs) inference.<n>VeriLLM combines lightweight empirical rerunning with cryptographic commitments, allowing verifiers to validate results at approximately 1% of the underlying inference cost.<n>We show that VeriLLM achieves reliable public verifiability with minimal overhead.
  arXiv  Detail & Related papers  (2025-09-29T04:07:32Z)
• Quantum Bayesian inference with Suport vector states for intrusion detection [0.0]
  We present a quantum Bayesian inference method for intrusion detection.<n>The method yields joint, marginal, and conditional probabilities aligned with causal structure.<n>Our results demonstrate the feasibility and interpretability of quantum-native inference for information security applications.
  arXiv  Detail & Related papers  (2025-07-01T03:41:04Z)
• Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
  We introduce Veracity Search (VS), a discrete search algorithm over veracity assignments.<n>It performs otherwise intractable inference in the posterior distribution over latent veracity values.<n>It generalizes VS, enabling accurate zero-shot veracity inference in novel contexts.
  arXiv  Detail & Related papers  (2025-05-17T04:16:36Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  We introduce a novel problem formulation called Abstract DNN-Verification, which verifies a hierarchical structure of unsafe outputs.<n>By leveraging abstract interpretation and reasoning about output reachable sets, our approach enables assessing multiple safety levels during the formal verification process.<n>Our contributions include a theoretical exploration of the relationship between our novel abstract safety formulation and existing approaches.
  arXiv  Detail & Related papers  (2025-05-08T13:29:46Z)
• Token-Level Adversarial Prompt Detection Based on Perplexity Measures and Contextual Information [67.78183175605761]
  Large Language Models are susceptible to adversarial prompt attacks. This vulnerability underscores a significant concern regarding the robustness and reliability of LLMs. We introduce a novel approach to detecting adversarial prompts at a token level.
  arXiv  Detail & Related papers  (2023-11-20T03:17:21Z)
• Spatial-Frequency Discriminability for Revealing Adversarial Perturbations [53.279716307171604]
  Vulnerability of deep neural networks to adversarial perturbations has been widely perceived in the computer vision community. Current algorithms typically detect adversarial patterns through discriminative decomposition for natural and adversarial data. We propose a discriminative detector relying on a spatial-frequency Krawtchouk decomposition.
  arXiv  Detail & Related papers  (2023-05-18T10:18:59Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)
• Logically Sound Arguments for the Effectiveness of ML Safety Measures [0.1657441317977376]
  We investigate the issues of achieving sufficient rigor in the arguments for the safety of machine learning functions. We sharpen the metric of imprecise pedestrian localization by associating it with the safety goal. We then propose a semi-formal assurance case for arguing the effectiveness of the post-processor.
  arXiv  Detail & Related papers  (2021-11-04T06:09:34Z)
• Asymmetric Modality Translation For Face Presentation Attack Detection [55.09300842243827]
  Face presentation attack detection (PAD) is an essential measure to protect face recognition systems from being spoofed by malicious users. We propose a novel framework based on asymmetric modality translation forPAD in bi-modality scenarios. Our method achieves state-of-the-art performance under different evaluation protocols.
  arXiv  Detail & Related papers  (2021-10-18T08:59:09Z)

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.