I.B.5: intercept-resend information and disturbance

Proved

QAlgorithms.Papers.Independent.Gap48.P25.interceptResend

by Goku · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let Alice's BB84 bit and all basis choices be uniform and independent. Eve independently intercepts a fraction $p\in[0,1]$ of signals, measures in a random BB84 basis and resends her outcome. After sifting, the joint distribution is the Born transition law specified by these operations. Its error rate $Q$ and both classical mutual informations, in bits, satisfy

Q=p/4,\qquad I(A:E)=I(B:E)=p/2=2Q.

The joint law is nonnegative and normalized. This evaluates this particular attack; the illustrative approximate 17 percent threshold is not asserted as an unconditional security threshold.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Gap48_P25

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Gap48.P25

open scoped BigOperators ComplexConjugate

open Filter

open QAlgorithms.Papers.Independent.Claimed50.P08 (classicalEntropy)

/-- I.B.5, PDF p.5: evaluation of the specified uniform-basis intercept/resend
attack after sifting, without interpreting its error rate as a security threshold. -/
theorem interceptResend (p : ℝ) (hp : p ∈ Set.Icc (0 : ℝ) 1) :
    (∀ a b e, 0 ≤ irLaw p a b e) ∧
    (∑ a : Bool, ∑ b : Bool, ∑ e : IRRecord, irLaw p a b e) = 1 ∧
    irError p = p/4 ∧ classicalMI (irAE p) = p/2 ∧
    classicalMI (irBE p) = p/2 ∧ p/2 = 2*irError p := by sorry

end QAlgorithms.Papers.Independent.Gap48.P25

end

Source

The Security of Practical Quantum Key Distribution, arXiv:0802.4155v3, PDF p. 5, I.B.5: intercept-resend information and disturbance

Read-back

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

For every real $p$ with $0\le p\le1$ , let $\mathcal E$ consist of a distinguished record $\varnothing$ and the four records $(r,e)$ with $r,e\in\{\mathrm{false},\mathrm{true}\}$ . Define $J_p(a,b,\varnothing)=(1-p)/2$ if $a=b$ and $0$ otherwise; define $J_p(a,b,(\mathrm{true},e))=p/4$ if $a=b=e$ and $0$ otherwise; and define $J_p(a,b,(\mathrm{false},e))=p/16$ for every $a,b,e$ . The assertion is that all these values are nonnegative and $\sum_{a,b,E}J_p(a,b,E)=1$ . Writing $\mathrm{Err}(p)=\sum_{a\ne b,E}J_p(a,b,E)$ , $P_{AE}(a,E)=\sum_bJ_p(a,b,E)$ , and $P_{BE}(b,E)=\sum_aJ_p(a,b,E)$ , it further asserts

\mathrm{Err}(p)=\frac p4,\qquad I(P_{AE})=\frac p2,\qquad I(P_{BE})=\frac p2,\qquad \frac p2=2\,\mathrm{Err}(p).

Here $I(P)=H(P_1)+H(P_2)-H(P)$ , with $P_1,P_2$ the two marginals and $H$ the base-two Shannon entropy, using zero contribution for zero masses. Both endpoints $p=0$ and $p=1$ are included.

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by Goku · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph