AI 中文总结
本文通过Rocq与SSProve机器验证，改进了同态加密噪声泛滥防御的安全性证明，将线性损失优化为平方根损失，形式化归约并证明了q次查询IND-CPAD敌手的优势边界。
AI 中文摘要
噪声泛滥（Noise flooding）是针对近似同态加密解密攻击的标准防御手段，但其安全性证明对组合异常敏感。将q个自适应解密答案中的每一个替换为统计接近的模拟结果，并应用普通混合论证会产生线性于q的损失。密码学证明转而累积条件Kullback-Leibler（KL）代价并一次性转换为统计距离，从而得到对参数至关重要的平方根损失。我们使用Rocq和SSProve对该论证进行机器验证。对于任何近似正确且具备IND-CPA安全性的全同态加密方案，我们为每个q次查询的IND-CPAD敌手形式化归约，并证明：Pr[IND-CPAD_NF^A =1] ≤ β_CPA(B_A,q) + √(qn)/(2γ)，其中n为明文维度，γ为泛滥宽度乘数。我们的证明在SSProve语义上构建了一种新的关系程序逻辑，其毕达哥拉斯判断在不将条件KL预算转换为统计距离的情况下对其进行组合，且经过验证的跟踪编译器将局部预言规则提升为任意自适应程序，仅进行一次最终转换。
英文摘要
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 β_{\mathsf{CPA}}(\mathcal B_{\mathcal A,q}) + \frac{\sqrt{qn}}{2γ}. \] where $n$ is the plaintext dimension and $γ$ 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.
