arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2610.25636

Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)

Tetsuya Sato
View original source ↗Read source document ↗Export metadata ↓

Abstract

Differential privacy (DP) is a gold-standard definition of privacy designed to evaluate the privacy guarantee of databases. Rényi differential privacy (RDP) is an important variant of DP that gives tight evaluations of machine learning algorithms. These formulations are easy to understand, but evaluating privacy for actual databases is complicated. Even a small change in the database can break its privacy, and evaluations of DP and RDP themselves are complicated. In particular, RDP evaluations in recent studies have become much harder. Therefore, formal verification of them has been studied for over a decade. In this paper, we propose an Isabelle/HOL library for formalizing Rényi differential privacy in a general setting. We first formalize RDP for continuous distributions. As a technical basis, we formalize several properties of convex functions and $f$-divergences for nonnegative convex functions. We formalize basic properties of RDP, conversion laws from RDP to DP, the moment accountants in DP, and the Gaussian mechanism and its RDP. Finally, we discuss the stochastic gradient descent mechanism with Gaussian noise and formalize a rough evaluation of its RDP and DP.

Explore related subjects

cs.CRcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Tetsuya Sato. 2026-10-19. Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version). https://arxiv.org/abs/2610.25636

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Arithmetic limiting laws over shifted primes: dimension zero, Fourier decay, and absolute continuity

For each prime $p$, let $c(p)=\frac{φ(p-1)}{p-1}\prod_{j\ge1}(1-p^{-j})$, the limiting probability, as $n\to\infty$, that a uniformly chosen matrix in $M_n(\mathbb{F}_p)$ has primitive-root determinant. As $p$ ranges over the primes, $c(p)$ has the classical shifted-totient limiting law $μ_G$ on $[0,1/2]$. Let $μ_f$ be its image under $x\mapsto-\log x$. We prove that $μ_G$ has Hausdorff dimension zero and gives full mass to absolutely normal Liouville numbers. Every Borel set of positive $μ_G$-mass has packing dimension at least $1/2$, and local dimension fails to exist $μ_G$-almost everywhere. Both Fourier transforms satisfy the effective bound $O((\log|τ|)^{-1/3}(\log\log|τ|)^{1/3})$. In every fixed reduced progression, the empirical laws of $c(p)$ and $φ(p-1)/(p-1)$ approach their respective limiting laws with sharp Kolmogorov order $1/\log x$. Over unrestricted primes, these laws and their negative-logarithmic images converge in $W_1$ at rate $O_B((\log x)^{-B})$ for every fixed $B>0$. We obtain concentration expansions to every fixed inverse-logarithmic order and prove that every sufficiently short maximizing interval for $μ_f$ contains $\log3$. For $U_T$ uniform on $[0,T]$, $(\log T)\widehat{μ_f}(U_T)$ converges in distribution to a circularly symmetric random variable whose modulus is an explicit random Euler product, with convergence of absolute moments of every real order $s>-1$. For every $A>0$, the strongly additive function $f_A$ with prime values $(\log\ell)^{-A}$ has absolutely continuous limiting laws for $f_A(n)$ and $f_A(p-1)$. We give extremal estimates and certified NTT prime searches. A lattice supplement determines second distinct nonzero squared norms of type-$A$ tensor products and gives uniform cyclotomic smoothing asymptotics at $ε=2^{-cφ(m)}$ for every fixed $c>0$. These statements are unconditional.

cs.CR↗
arXiv2026

Sequential Behavioral Watermarking for LLM Agents

LLM-based agents act through sequences of executable decisions, but their trajectories provide little evidence of which agent or policy produced them, making provenance, ownership, and unauthorized reuse difficult to establish from observed behavior alone. This motivates watermarking signals embedded directly into agent behavior rather than only into generated text, since text watermarking cannot capture the action-level decisions that define agent execution. Recent agent watermarking methods address this gap by moving the watermark from generated text to behavioral choices. However, by treating each action step as an independent trial, they overlook trajectory structure and become fragile when trajectories are perturbed, truncated, or observed without reliable alignment. We propose SeqWM, a sequential behavioral watermarking framework that embeds signals into history-conditioned transition patterns and verifies trajectories position-agnostically against random-key baselines. Experiments across diverse agent benchmarks and LLM backbones show that SeqWM consistently achieves reliable detection while preserving agent utility, and remains robust under trajectory corruption where round-indexed behavioral watermarks collapse.

cs.CR↗
arXiv2026

Mobius Injection: From One-Shot Prompt Injection to Sustained Resource Exhaustion in AI Agent Infrastructure

Large Language Model (LLM) agents have emerged as key intermediaries, orchestrating complex interactions between human users and a wide range of digital services and LLM infrastructures. While prior research has extensively examined the security of LLMs and agents in isolation, the systemic risk of the agent acting as a disruptive "hub" within the user-agent-service chain remains largely overlooked. In this work, we expose a novel threat paradigm by introducing Mobius Injection, a sophisticated attack that weaponizes autonomous agents into zombie nodes to launch what we define as Agent-based and -Oriented DDoS (AbO-DDoS) attacks. Mobius Injection composes known indirect prompt injection and persistent agent components through a distinct structural mechanism named Semantic Closure, which induces sustained recursive execution of agent components through a single injection event. We demonstrate that this attack is lightweight for the adversary, can evade traditional volumetric DDoS monitors and input filters calibrated for low false-positive rates, and is highly configurable, allowing for surgical targeting of specific environments or model providers. To evaluate the real-world impact, we conduct extensive experiments across three representative claw-style agents and three mainstream coding agents, integrated with 12 frontier proprietary or open-weight LLMs. Our results demonstrate that Mobius Injection achieves substantial attack success across diverse tasks, driving single-node call amplification up to 51.0x. Under coordinated multi-node pressure, each infected node still drains about 123k--127k tokens on a shared five-GPU backend; benign request latency rises by abou 23x--24x, and coordinated infections eventually saturate shared capacity until benign traffic is effectively denied service.

cs.CR↗