Lemma 2: secrecy plus correctness implies security

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.secrecy_correctness_security

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $P^{\rm pass}_{S_A S_B T E\mid Z}$ be a normalized classical-device law with a common finite nonempty key alphabet $\mathcal K$ and finite nonempty transcript, Eve-output and Eve-input alphabets. The $(S_A,S_B,T)$ marginal is independent of $Z$ . The ideal pass law replaces the keys by a uniform perfectly correlated pair, independent of the actual $(T,E\mid Z)$ marginal. The intermediate law copies Alice's key into Bob's register and preserves $(S_A,T,E\mid Z)$ . Let $r\in[0,1]$ be the abort probability, with an identical normalized abort branch in all three systems. Write $d_{\rm NS}$ for the operational NS distance, and $s,c,k$ for the pass-weighted secrecy, disagreement and security errors, respectively. Thus $s=(1-r)d_{\rm NS}(P_{S_A T E\mid Z}^{\rm pass},P_{S_A T E\mid Z}^{\rm ideal,pass})$ , $c=(1-r)\Pr[S_A\ne S_B\mid\mathrm{pass}]$ , and $k=(1-r)d_{\rm NS}(P^{\rm pass},P^{\rm ideal,pass})$ .

For any nonnegative error budgets $\varepsilon_{\rm sec}$ and $\varepsilon_{\rm cor}$ ,

s\le\varepsilon_{\rm sec}\quad\text{and}\quad c\le\varepsilon_{\rm cor}\quad\Longrightarrow\quad k\le\varepsilon_{\rm sec}+\varepsilon_{\rm cor}.

Separate secrecy and correctness estimates therefore imply security.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P22

Formal statement

noncomputable section

open scoped BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P22

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Advance50.P47
  (Box IsCorrelation IsNoSignaling HasLocalModel correlationMixture prBox)

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Information100.P27 (shannon)

open QAlgorithms.Papers.Independent.Gap48.P25 (classicalMI)

/-- PDF pp.32–33, Lemma 2, (105)–(112): the comma in (105) means subtraction,
as made explicit in (106),(112). Both error budgets are nonnegative. -/
theorem secrecy_correctness_security {K T E Z : Type}
    [Fintype K] [Fintype T] [Fintype E] [Fintype Z]
    [Nonempty K] [Nonempty T] [Nonempty E] [Nonempty Z]
    (r : KeyOutput K T E Z) (z : Z) (es ec : ℝ) (hes : 0 ≤ es) (hec : 0 ≤ ec)
    (hs : cdSecrecyError r ≤ es) (hc : correctnessError r z ≤ ec) :
    securityError r ≤ es + ec := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P22

end

Source

Limitations on device independent key secure against non signaling adversary via the squashed non-locality, arXiv:1903.12154v7, PDF p. 32, Lemma 2 / equation (105)

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For finite nonempty types $K,T,E,Z$ , let $r$ have abort probability $\alpha\in[0,1]$ and pass and abort arrays $P,Q$ , each nonnegative, normalized over $a,b,t,e$ at every $z$ , and with $\sum_eR_z(a,b,t,e)$ independent of $z$ . Define

I_z(a,b,t,e)=\mathbf1_{\{a=b\}}\frac{\sum_{u,v}P_z(u,v,t,e)}{|K|}, \qquad P^A_z(a,t,e)=\sum_bP_z(a,b,t,e), \qquad I^A_z(a,t,e)=\sum_bI_z(a,b,t,e).

For arrays on $Z\times C\times E$ , define $d(R,S)$ as the supremum of

\frac12\sum_{j=0}^{m-1} \left|\sum_{c,z,e}u(c,z)(R_z(c,e)-S_z(c,e))v(c,z,e,j)\right|

over positive integers $m$ and nonnegative kernels $u,v$ satisfying $\sum_z u(c,z)=1$ and $\sum_jv(c,z,e,j)=1$ . For every $z_0\in Z$ and real numbers $\varepsilon_s,\varepsilon_c\ge0$ , if

(1-\alpha)d(P^A,I^A)\le\varepsilon_s,\qquad (1-\alpha)\sum_{\substack{a,b\\a\ne b}}\sum_{t,e}P_{z_0}(a,b,t,e)\le\varepsilon_c,

then

(1-\alpha)d(P,I)\le\varepsilon_s+\varepsilon_c.

Here $C=K\times T$ for the first distance and $C=K\times K\times T$ for the second.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph