International Association
for Cryptologic Research

A blind signature scheme allows a user to interact with a signer to obtain a valid signature on a message, while ensuring that the signer cannot learn any information on the message being signed, nor link a given couple message-signature to the specific interaction that produced it (blindness). In round-optimal (i.e., two-move) blind signature schemes, a user sends a request (typically a commitment) for a message, and the signer responds with a signature. To achieve blindness, the resulting blind signature usually consists of a zero-knowledge proof of knowledge of a valid signature from the signer on a request. This reliance on zero-knowledge proofs has become the main bottleneck in reducing the blind signature size. In particular, state-of-the-art lattice-based blind signature schemes are instantiated based on the zero-knowledge proof system from [Lyubashevsky et al., EUROCRYPT, 2022], which results in blind signatures of at least 22 KB. In this work, we carefully design a blind signature protocol following the classical lattice-based Σ-protocol as in [Ducas et al., CRYPTO, 2013], so that the last component naturally forms a short preimage of the hash of the message, as a classical GPV signature. As a result, this removes the need for zero-knowledge proofs in the blind signature. Eventually, this design allows us to obtain a significantly more compact blind signature of size 4.7 KB, with concurrent security under the Module-SIS assumption. As a trade-off, our protocol may require more than one round with small probability, due to the rejection sampling in lattice-based Σ-protocols. Under our proposed parameters, however, the expected number of rounds for honest users can be as small as 1.1, which is very close to optimal. To minimize the number of rounds, we require users to prove that they failed to derive a blind signature in the previous round, before starting a new one. This technique yields a moderately looser bound on the expected number of rounds for malicious users, who will be forced to terminate in at most 2.6 rounds.

Harvesting ciphertext from cloud storage needs no quantum computer; decrypting it later does. That gap is the harvest-now-decrypt-later exposure: anything protected by RSA or ECDH today that must stay secret for decades is already compromised. Small and medium-sized enterprises are least able to respond: they neither run the infrastructure on which their data sits on nor employ a cryptographer. Bespoke migration suits firms with security budgets; a managed key service relocates trust rather than removing it. The obstacle is architectural, not cryptographic. We present Quantum Cloud Guard (QCG), a software-only three-layer architecture. No prior SME-oriented system combines its three elements: client-side hybrid post-quantum encryption, self-hosted key custody with client-verifiable ML-DSA-87 signatures on served keys, and an integrated application-layer abuse-prevention gateway. Files never leave the client: each is sealed under AES-256-GCM, its key wrapped to an ML-KEM-1024 public key from the enterprise’s key service. The enterprise alone administers it; it signs every key with ML-DSA-87, so a client that pinned it detects substitution. Separating key custody from data custody is the point: a provider holding both can read the data. On a 24 MHz STM32F407, ML-KEM-1024 key generation takes 40.8 ms and decapsulation 44.0 ms; on the server every post-quantum operation stays sub-millisecond, signing adding 0.24 ms per request. The service runs on a 4.49 EUR/month virtual server. Under sustained flooding, the in-process gateway Sentinel Gate rejected 98.8% of attack traffic while a legitimate client’s median latency moved from 621 to 625 ms. Being single-source, this shows filtering effectiveness, not DDoS resilience.

We present a neural network-based pipeline for efficiently generating fast matrix multiplication (FMM) algorithms of small but arbitrary dimensions $(n,m,k)$. Our neural network is general and tunable to output FMM schemes with specific properties, and in this paper we specifically target aspects that are useful and important in practical implementation, such as ternarity (coefficients in $\{-1, 0, 1\}$), sparseness and a low number of additions after optimization (addition reduction carried out separately).

We generate and optimize thousands of FMM algorithms and show that our generation method is beneficial in terms of performance across the entire FMM pipeline (both the FMM generation itself and optimization of additions). We discuss performance metrics and utilize heatmaps to visualize and understand this performance.

We achieve record-low arithmetic (additive) complexity for various combinations of dimensions. For $(n,m,k) = (2,2,k)$, our method performs particularly well. Our improvement compared to previous results increases with $k$.

We show that the (addition) optimization process can behave very differently depending on the dimensions considered, indicating how further improvements (beyond our results) can be targeted. In particular, in the $(n,m,k) = (2,2,k)$ setting, we show evidence of structural FMM properties coming into play, concretely showing that FMM generation with a minimal number of additions is sometimes suboptimal with respect to the entire FMM pipeline.

Finally, we make our neural network implementation, our generated FMM schemes, heatmap utilities and datasets publicly available.

We present the Pilot--Sailor Framework, an LLM-guided system for studying theoretical open problems in symmetric cryptography. Pilot proposes intermediate statements and proof plans. Sailor attempts formal proofs, and the proof assistant admits only checked declarations to the verified context. We apply this methodology to Boolean-function theory and symmetric cryptanalysis through fourteen mathematical case studies, comprising complete resolutions, corrected formulations, counterexamples, and scoped quantitative advances. In particular, we prove the original pointwise Tu--Deng conjecture for all word lengths and admissible residues. We further characterize equality in this bound: if \(t\) has \(z\) zero bits, equality holds exactly when every cyclic gap between consecutive zeros is at least \(z\). This criterion also gives a closed formula for the number of equality cases for each \(z\). We also prove that, for \(n=2k\geq6\) and \(k

The main message of this paper is that several seemingly different circular-style primitives are existentially equivalent. In particular, somewhat surprisingly, we show that hinting PRGs (Koppula and Waters, CRYPTO 2019) are equivalent to secret-key encryption (SKE) schemes satisfying key-dependent-message (KDM) security. As a conceptual centerpiece, we introduce key-dependent-shift (KDS) security for weak pseudorandom functions (PRFs), and show that they serve as a convenient hub connecting these primitives. We also show that KDS secure weak PRFs imply other cryptographic primitives with circular-style security, such as linear-resistant PRGs (Hajiabadi et al., ITC 2023) and hinting weak PRFs (Alamati and Patranabis, ASIACRYPT 2022), all of which are thus existentially equivalent to KDM secure SKE and hinting PRGs as well. Hence, KDS secure weak PRFs can be thought of as a unifying umbrella for circular-secure cryptographic primitives. As another application of our new notion, we show that KDS security enables new constructions of public-key encryption (PKE) satisfying randomness-dependent-message (RDM) security and correlated-product secure trapdoor functions (TDFs). Our key technical contribution is a generic construction of KDS secure weak PRFs from any KDM secure SKE.

Authenticated data structures are widely used to compute compact digests of evolving collections of elements and to support efficient verification of element inclusion. However, the authenticated collection often should not grow forever: older elements may expire and no longer require verification. Many implemented append-only approaches, for example used in Certificate Transparency (CT), do not directly support this setting, since previously accumulated elements remain part of the authenticated state indefinitely. In this work, we introduce a pruning accumulator, a stateful accumulator that supports both incremental addition of new elements and pruning of an old prefix of previously accumulated elements. The resulting digest represents the unpruned sequence, while pruned elements are removed from the authenticated state. Unpruned elements continue to support proof-of-inclusion verification, proof updates, update verification, and consistency checks. This captures applications that require authenticated, incrementally maintained state over a moving window of elements. We present two constructions of Merkle-tree-based pruning accumulators, both with efficient accumulation, prefix pruning, proof generation, proof updating, and verification. The constructions preserve the standard Merkle-tree style of verification for active elements while reducing long-term storage requirements. We provide formal definitions, correctness and security analysis, an open-source implementation, and experimental evaluation demonstrating the performance benefits of pruning.

BitVM2 brought arbitrary program execution to Bitcoin, yielding the first light-client-based bridge to its second layers and reducing the trust required at setup to a single honest participant. Its successors, BitVM3 and BABE, move the disputed computation off-chain into Garbled Circuits (GCs), cutting worst-case on-chain dispute costs by roughly three orders of magnitude and so opening participation beyond well-capitalized operators; BABE in turn cuts the off-chain storage and setup costs of BitVM3's garbled circuits by a comparable factor. What still reaches the chain, however, is bulkier than it need be. BitVM2 commits its data with compact Winternitz one-time signatures (WOTS), whereas BitVM3 and BABE must reveal GC input labels on-chain and so fall back on far bulkier Lamport signatures, which play two roles at once: GC input labels and Bitcoin-verifiable commitments. WOTS cannot simply be substituted, because its hash chains are monotonic---an evaluator holding one state's preimage can hash forward and obtain several active labels on a single input wire, destroying the circuit's privacy. Recovering BitVM2's compactness therefore calls for a practical GC whose input labels are WOTS signatures---a construction that has remained out of reach. We close this gap with a non-interactive \emph{WOTS-to-Lamport translation gadget}: the garbler commits on-chain using compact WOTS chains, and the evaluator expands them off-chain into exactly the orthogonal Lamport labels the GC consumes, learning nothing about the mutually exclusive ones. A naive translation table that enumerated messages would be exponentially large. Two symmetries bring it down to quadratic: reconstruction from a Shamir sharing depends only on \emph{how many} shares are held and not on \emph{which}, which collapses the exponentially many messages onto the single checksum weight WOTS already computes; and monotonicity, the very property that made WOTS unusable, orders an evaluator's access by inclusion. We model the gadget as a garbling scheme and prove it adaptively private. Applied to BABE, it restores WOTS-scale commitments to a GC-based protocol, cutting total on-chain script size by more than $3\times$ and bringing dispute transactions within Bitcoin's standardness limit.

We construct the first multi-key fully homomorphic encryption (MKFHE) scheme where the ciphertext size, public key size, and secret key size remain independent of the number of users, $N$. Our construction is leveled and relies on the standard Learning with Errors (LWE) assumption. All prior MKFHE schemes incur at least linear growth in ciphertext size with the number of users ($|\mathsf{ct}| \propto N$), a limitation that has persisted across more than a decade of research. Our results provide the first evidence that MKFHE with constant ciphertext size is achievable under standard assumptions and paves the way for many interesting applications.

We also describe a single-round distributed decryption protocol for multi-key ciphertexts in our fully-succinct MKFHE scheme. More remarkably, we show that our MKFHE scheme simultaneously satisfies the following properties: (1) the size of each user's partial decryption share is identically equal to the plaintext length (i.e., partial decryption shares are truly rate-1), and (2) an honest user's partial decryption can be simulated. To the best of our knowledge prior to this work, we did not have any MKFHE with one-round distributed decryption from standard assumptions that simultaneously satisfied both these properties. We show that our MKFHE is significantly useful in designing various forms of multi-party computation (MPC) protocols with asymptotically optimal communication complexity.

ML-KEM is IND-CCA2 secure only because of one check inside decapsulation: the receiver re-encrypts the message it recovered and returns the true shared secret only if the result matches the received ciphertext exactly. This is the Fujisaki–Okamoto (FO) check. wolfSSL implemented it in hand-written SIMD assembly, and on two backends it compared fewer than all of the ciphertext bytes. The x86-64 AVX2 path compared 1536 of 1568 bytes; the ARM64 NEON path compared roughly half.

These bugs were documented as a weakening of IND-CCA2 security, in that a tampered ciphertext can slip past the check. We show they are worse than that. The bytes the check skips carry the tail of the decryption noise, and that noise is an exact linear function of the secret key. An attacker who varies those unchecked bytes and watches the decapsulation output reads the noise off one coordinate at a time. Stacking the measurements gives an overdetermined linear system in the secret, which we solve by ordinary least squares with no lattice reduction.

The measurement is a plaintext-checking oracle, the same primitive that key-mismatch attacks use. What is new is where it comes from. Reading it off the unchecked v-tail, rather than from chosen sparse-u ciphertexts, means it survives even when u is fully validated, as on AVX2, so the standard "validate all of u" hardening does not close it. The price is queries, 10⁵ to 10⁶ against a few thousand for key-mismatch, so the contribution is reach rather than efficiency.

We recover most of the ML-KEM-1024 private key end-to-end against the shipped binaries on both backends: 98.0% of the 2048 secret coefficients at 400 ciphertexts on AVX2, and 98.5% at 600 on NEON, reaching the full key with more ciphertexts (the verified reference model recovers all 2048 at about 1300 ciphertexts). The cost appears to track the geometry of which bytes go unchecked more than their number: NEON leaves about 2.5× more coordinates unchecked than AVX2 yet needs more ciphertexts. We conclude that an incomplete FO comparison is a key-recovery vulnerability, and should be triaged as one.

Key transparency enables a centralized encrypted messaging provider to publicly commit to the public keys it distributes, allowing clients to detect potentially malicious keys. Recent deployments by WhatsApp and iMessage demonstrate the promise of this approach, but they rely on third-party global auditors to detect misbehavior by the key server. No existing system supports auditing efficiently enough to be done by lightweight end users while also providing scalability to billions of users and short epoch latency.

We present $\mathsf{Aegon}$, a key transparency scheme designed for global-scale encrypted messaging. Building on ideas from $\mathsf{IronDict}$, $\mathsf{Aegon}$ avoids per-epoch work that scales with the full dictionary size: its server computation depends only on the number of updates in the current epoch, eliminating global invariance proofs and enabling epoch latency of under a minute ($500\times$ reduction compared to $\mathsf{IronDict}$). $\mathsf{Aegon}$ further introduces a sharded dictionary design that reduces global parameters to shard-dependent sizes and enables horizontal scaling. To control long-term storage, $\mathsf{Aegon}$ uses proof caching to safely discard historical dictionary snapshots, so storage grows only with retained history.

We provide a production-grade Rust implementation of $\mathsf{Aegon}$ and demonstrate practical scalability to a dictionary with $4$ billion entries, comparing it against the public codebase of WhatsApp Key Transparency ($\mathsf{AKD}$). At the throughput of $1{,}250$ updates per second, $\mathsf{Aegon}$ produces constant size auditor proofs of under $30$ KB, verifiable in under $65$ ms and independent of the number of updates per epoch or of the directory fill. At a fully-populated $2^{32}$-entry directory this is roughly an $80{,}000\times$ reduction in audit proof size and a $370\times$ reduction in verify time relative to $\mathsf{AKD}$. All other server and client operations remain highly efficient and comparable to $\mathsf{AKD}$, while $\mathsf{Aegon}$ achieves stronger privacy guarantees.

Nonlinear feedback shift registers (NFSRs) are fundamental building blocks for modern stream-cipher constructions. An $n$-stage NFSR $f$ is classified as irreducible when the output sequence set of $f$ does not contain the output family of any NFSR of order less than $n$. Existing research has established upper and lower bounds for the density of irreducible NFSRs, confining this value within the range of 0.4461 to 0.4834. This study tightens these bounding intervals with high accuracy, reducing the original 0.04 gap down to only $8\times10^{-6}$.

In this work, we revisit multi-round public-coin proof systems by enabling the use of their simulators and extractors within other cryptographic protocols. Although research on multi-round public-coin proofs has rapidly progressed, their simulators and extractors typically differ from the 3-move (e.g., Sigma protocols) setting in interface and behavior, and are rarely studied from this viewpoint.

Prior work [Abe et al., Eurocrypt ’26] introduced the notion of critical-round zero-knowledge, showing that, for some classes of protocols, multi-round ZK simulators can be as useful in protocol constructions as the 3-move ones. In this paper, we focus on soundness and introduce critical-round special soundness, a property that enables multi-round witness extractors to be used in protocol design in a manner analogous to 3-move special soundness. We show that several existing multi-round public-coin proof systems satisfy this property and present three applications: - A witness sharing scheme that verifiably secret-shares an NP witness without interaction among recipients. It can be realized in a hash-based way by combining MPC-in-the-Head with secret sharing. - An offline trapdoor-extractable trapdoor commitment scheme where a trapdoor is extracted immediately upon a double opening. Offline trapdoor extractability was previously known from 3-move public-coin proofs, but no general construction from multi-round proofs was known; our approach closes this gap. - A parameter improvement for the multi-round Fischlin transform [Rotem–Tessaro, Crypto’25]. The improved parameter extends the design space of the multi-round Fischlin transform and reduces the prover’s complexity in practice.

Overall, our results clarify how multi-round public-coin proofs can support protocol design beyond their traditional role as stand-alone proof systems.

Since the seminal work of Carlini et al. at CRYPTO 2020, cryptanalytic model extraction has shown neural-networks parameters can be recovered from black-box queries. Existing attacks are largely built around piecewise-linear phenomena. Softmax attention, as the key component of the transformer architecture, presents a different extraction landscape: its nonlinearity is smooth and sequence-dependent, which renders the existing piecewise-linear-based method inapplicable. Recent work has investigated the learnability of a single-head attention model, while in the multi-head case, the parameters of the multi-head attention layer cannot be uniquely identified from value queries alone.

In this paper, we propose the first attack against multi-head attention models. We formalize the extractable representative of multi-head attention and give a polynomial-time algorithm for extracting the parameters of the canonical representative model. We also test our algorithm end to end under finite precision, and successfully extract the parameters of a softmax attention model with token dimension 8 and 6 heads to accuracy $2^{-51}$. Moreover, we overcome the limitation that existing parameter extraction algorithms for one-layer single-head Transformers fail when the ReLU feedforward networks (FFNs) include bias terms. The effectiveness of our approach is demonstrated through model extraction attacks in finite-precision experiments. These results show that softmax normalization itself exposes exploitable algebraic structure, extending cryptanalytic extraction beyond ReLU-centric techniques.

Secure group messaging protocols, now standardized by the IETF as Messaging Layer Security (MLS), provide end-to-end encryption for billions of users. The cryptographic core of these protocols is continuous group key agreement (CGKA), a primitive designed to maintain a shared secret among a dynamic group while providing security guarantees like forward secrecy and post-compromise security. A critical challenge for CGKA is achieving efficiency, particularly sublinear complexity (in the size of the group), for group operations. While practical tree-based protocols like TreeKEM offer logarithmic complexity in ideal (so-called "fair-weather") scenarios, their performance degrades to linear in the worst-case, and even realistic average-case, scenarios. This performance collapse raises the fundamental question of whether any CGKA protocol can achieve provably sublinear worst-case complexity.

Prior work has established significant barriers to this goal, including black-box impossibility results ruling out efficient constructions from standard public-key encryption. Theoretical solutions circumvent these barriers using powerful tools like indistinguishability obfuscation ($i\mathcal{O}$), but these constructions are astronomically inefficient and often provide weaker security guarantees, such as lacking forward secrecy. This leaves a wide gap between practical protocols with poor worst-case guarantees and theoretical solutions that are entirely impractical.

In this paper, we narrow this gap by presenting the first CGKA protocol that achieves provably logarithmic worst-case complexity for both computation and communication. Our first construction is based on a falsifiable and plausibly post-quantum assumption called decomposed learning with errors (decomposed LWE), and achieves basic CGKA security (only group members know the key) and post-compromise security, but not forward secrecy. We then show how to extend our scheme in the random oracle model to achieve optimal security (including forward secrecy) while retaining worst-case sublinear communication. However, the forward-secure refresh operation takes linear time in the group size, while still producing compact ciphertexts.

Our work is the first to establish that worst-case efficient CGKA is theoretically possible from simple falsifiable assumptions. Moreover, it offers a plausible roadmap towards concretely efficient constructions.

Secure key leasing (SKL) is a quantum cryptographic primitive that enables the leasing of decryption keys to delegated users with the guarantee that, once revoked, the lessees irreversibly lose decryption capability. A key feature that makes SKL practically relevant is classical revocation: the ability to revoke keys at any time and from anywhere, without relying on a quantum channel.

In this work, we revisit SKL schemes for public-key encryption (PKE) and identity-based encryption (IBE), and present a new approach for concrete efficiency under the standard Learning With Errors (LWE) assumption. First, we refine the security analysis of the Dual-Regev SKL-PKE scheme with classical revocation from [Ananth, Poremba, and Vaikuntanathan, TCC 2023; Ananth, Hu, and Huang, TCC 2024], establishing security under the polynomial hardness of LWE with polynomial modulus. Together with the resource efficiency of the Dual-Regev-based construction, our analysis shows that this approach yields the most quantum-efficient known SKL-PKE scheme. Second, we present a simple and efficient construction of selectively secure SKL-IBE with classical revocation from standard LWE. Our approach directly extends the Dual-Regev SKL-PKE within the IBE framework of [Agrawal, Boneh, and Boyen, Eurocrypt 2010], avoiding garbled circuits and obfuscation-based assumptions and achieving improved concrete efficiency over prior generic approaches.

Multi-party computation (MPC) enables multiple parties to jointly process sensitive data without revealing their inputs. However, existing MPC protocols remain inefficient for high-dimensional sparse data. In plaintext, sparse linear algebra algorithms address this problem using two fundamental primitives, Scatter and Gather.

We propose SparseMPC, an outsourced MPC protocol that securely implements Scatter and Gather and uses them to perform sparse matrix multiplication. Our protocol supports an arbitrary number of data owners and provides a low memory footprint, constant round complexity, and low communication cost. Beyond sparse matrix multiplication, SparseMPC provides a foundation for efficiently realizing a broader class of sparse computations in outsourced MPC.

Autonomous agents are increasingly used to plan and execute paid workflows on behalf of users. Existing agentic-payment frameworks support this delegation through merchant-admission authorization credentials but require the user to specify merchants before execution. However, complex paid workflows often span multiple services and merchants, and agents may choose among them based on intermediate results. This creates two limitations: (1) requiring the user to choose each merchant in advance either limits the agent's adaptability or forces the user back into the loop; and (2) reusing a stable identifier across merchants lets observers link separate paid calls and infer the user's broader intent. To address these limitations, we introduce MinMandate, which grants adaptive merchant selection within user-approved task bounds and derives fresh per-call payment views without introducing a stable cross-merchant identifier. Extensive experiments on AgentDojo tasks demonstrate that, when 50% of merchants are unavailable, MinMandate improves task success by 32.7 percentage points on average across four tested planners compared with an AP2 baseline that preauthorizes one merchant per service class. Reintroducing a reusable public payment-layer handle in the Stable Handle ablation raises attacker task-recovery success by 27.4 percentage points on average, isolating the privacy cost of a stable join handle. The code is available at https://github.com/Zora-G/minmandate.

Certified deletion enables a party to prove that it has erased the sensitive information contained in a quantum state. Bartusek and Raizes (CRYPTO 2024) gave the first secret-sharing scheme with privately verifiable deletion. Subsequently, Katz and Sela (EUROCRYPT 2025) constructed secret-sharing schemes with publicly verifiable deletion under computational assumptions. Constructing such a publicly verifiable scheme without cryptographic assumptions remains open.

In this work, we introduce an intermediate notion called unanimously verifiable deletion, where deletion certificates are verified jointly by the parties in the protocol. While private verification relies on the dealer and public verification allows any third party to verify deletion, unanimous verification assigns the verification responsibility to the parties in the secret-sharing scheme themselves. We construct an information-theoretically secure linearly homomorphic threshold secret-sharing batch scheme with adaptive unanimously verifiable deletion. In particular, to obtain its linear-homomorphic property, we exploit a linearly homomorphic structure of BB84-type states that enables linear operations on encoded values while preserving certified deletion. More generally, this structure can be used to upgrade certain primitives with certified deletion to their linearly homomorphic counterparts.

As another major contribution, we demonstrate an application of this batch scheme by constructing outsourced multi-party computation (MPC) protocols for arbitrary arithmetic circuits. Our outsourced MPC has honest classical clients and quantum servers, and achieves adaptive unanimously verifiable deletion security in the trusted-preprocessing and security-with-abort setting, supports public output reconstruction, and is secure against malicious, rushing quantum server adversaries for any $t

Large-state ARX-based S-boxes have become a key component of modern lightweight cryptographic designs, yet deriving tight security bounds for their differential and linear properties remains challenging. In this paper, we study the security of Alzette, the 64-bit ARX-based S-box used in the SPARKLE permutation, and present a general framework for the analysis and design of large-state ARX S-boxes. We introduce SMCS, a hybrid search strategy that combines MILP-based optimization with SMT-based model checking, enabling the computation of tight bounds on maximum expected differential probabilities and linear correlations. Using SMCS, we refine existing bounds for Alzette and, for the first time, establish tight linear bounds (resp. differential bounds) for up to 15 rounds (resp. 14 rounds). Building on these results, we propose S-box configurational encoding, an automated design method for ARX-based S-boxes, and introduce a new family of S-boxes called AFS (ARX-Feistel Structure) with 32-bit and 64-bit instances. We show that selected AFS instances achieve strictly better resistance to single-trail differential and linear cryptanalysis than SPECKEY and Alzette, respectively, while preserving comparable hardware and software costs. Finally, we present the first bit-based SMT model for optimal long-trail decomposition and apply it to derive more accurate bounds for SPARX-128 and SPARKLE. Our results show that replacing the S-boxes with AFS instances yields substantial improvements in cryptanalytic security margins.

Noise flooding is a standard defense against decryption attacks on approximate homomorphic encryption, but its security proof is unusually sensitive to composition. Replacing each of \(q\) adaptive decryption answers with a statistically close simulation and applying an ordinary hybrid argument loses linearly in \(q\). The cryptographic proof instead accumulates conditional Kullback-Leibler (KL) costs and converts to statistical distance once, giving the parameter-critical square-root loss.

We machine-check this argument using Rocq and SSProve. Given any fully homomorphic encryption scheme that is approximately correct and IND-CPA secure, we formalize a reduction for every \(q\)-query IND-CPAD adversary and prove \[ \Pr[\mathsf{IND\text{-}CPAD}_{\mathsf{NF}}^{\mathcal A}=1] \leq \beta_{\mathsf{CPA}}(\mathcal B_{\mathcal A,q}) + \frac{\sqrt{qn}}{2\gamma}. \] where \(n\) is the plaintext dimension and \(\gamma\) is the flooding-width multiplier. Our proof constructs a new relational program logic over SSProve semantics. Its Pythagorean judgment composes conditional KL budgets without converting them to statistical distance, and a verified trace compiler lifts a local oracle rule to arbitrary adaptive programs with a single final conversion.