Empirical/QM: B92 quantum-key-distribution security (two-state protocol)

Category: 3-Local (QM-validity content, no CSD ontology).

B92 (Bennett 1992) is the minimal QKD protocol: Alice encodes each bit in one of just two non-orthogonal states,

• bit 0 → |0⟩,
• bit 1 → |+⟩ = (|0⟩+|1⟩)/√2,

and Bob performs unambiguous state discrimination. Because the two encodings are non-orthogonal they cannot be perfectly cloned or distinguished, so an eavesdropper cannot copy the signal without disturbance — the security root is exactly no-cloning, reused verbatim from Empirical/QM/NoCloning.lean (the two B92 encoding states are the Wiesner pair |0⟩, |+⟩).

Bob's discrimination is error-free on conclusive events thanks to two zero-overlaps:

• Bob measures Z; the outcome |1⟩ is impossible from |0⟩ (|⟨1|0⟩|² = 0), so a |1⟩ click conclusively signals bit 1.
• Bob measures X; the outcome |−⟩ is impossible from |+⟩ (|⟨−|+⟩|² = 0), so a |−⟩ click conclusively signals bit 0.

A conclusive click occurs, per matched round, with Born probability ½ (bornProb |1⟩ |+⟩ = ½, bornProb |−⟩ |0⟩ = ½); the complementary events are inconclusive and discarded, never wrong.

This module reuses the Born layer of Crypto/BB84.lean (ket0, ket1, ketPlus, ketMinus, bornProb, bornProb_comm, and the proved transition values). The only new inner product it establishes is the X-basis orthogonality ⟨−|+⟩ = 0, which BB84 did not need.

What this delivers (all Born-grounded)

• b92_encode — the encoding map Bool → EuclideanSpace ℂ (Fin 2) (false ↦ |0⟩, true ↦ |+⟩): the states have a genuine protocol consumer.
• b92_nonorthogonal — ⟨0|+⟩ ≠ 0: the resource (reuses BB84).
• b92_unambiguous_one — bornProb |1⟩ |0⟩ = 0: a |1⟩ (Z) click excludes the bit-0 state |0⟩, so it is conclusive for bit 1.
• b92_unambiguous_zero — bornProb |−⟩ |+⟩ = 0: a |−⟩ (X) click excludes the bit-1 state |+⟩, so it is conclusive for bit 0.
• b92_conclusive_rate_one — bornProb |1⟩ |+⟩ = ½: matched-round conclusive rate for bit 1.
• b92_conclusive_rate_zero — bornProb |−⟩ |0⟩ = ½: matched-round conclusive rate for bit 0.
• b92_no_perfect_eavesdrop — the security capstone: no universal cloner can copy both encoding states |0⟩ and |+⟩ against a fixed blank, an exact instance of NoCloning.no_universal_cloner_of_witness (same shape as quantum_money_unforgeable).

Honest scope

This proves the B92 unambiguous-discrimination structure (error-free conclusive events + ½ conclusive rates) and the no-cloning security root, all Born-grounded via ‖⟨a|b⟩‖². The conclusive events are modelled as Born zero-overlaps; no measurement-update / collapse operator is used.

The full composable finite-key security — phrased via a measurement-update (collapse) operator turning an unambiguous-discrimination POVM into a sifted key with a min-entropy accounting — stays out of scope, the same LF5 gate noted in Crypto/BB84.lean and Empirical/QM/Resources/Teleportation.lean. Nothing beyond the unambiguous-discrimination model and no-cloning is claimed here.

References

• Bennett 1992, Phys. Rev. Lett. 68, 3121 ("Quantum cryptography using any two nonorthogonal states"): the two-state protocol and its unambiguous- discrimination reading.
• Cross-links: Empirical/QM/Crypto/BB84.lean (the reused Born layer and intercept-resend QBER), Empirical/QM/Crypto/QuantumMoney.lean (the same no-cloning witness idiom on the |0⟩, |+⟩ pair), Empirical/QM/NoCloning.lean (no_universal_cloner_of_witness).
• specs/future-work.md — QKD security-model tranche (composable finite-key).

The B92 encoding map

noncomputable def CSD.Empirical.B92.b92_encode : Bool → EuclideanSpace ℂ (Fin 2)

The B92 encoding map. Alice encodes bit false as |0⟩ and bit true as |+⟩; the two encodings are non-orthogonal (b92_nonorthogonal).

Equations

• CSD.Empirical.B92.b92_encode false = CSD.Empirical.BB84.ket0
• CSD.Empirical.B92.b92_encode true = CSD.Empirical.BB84.ketPlus

@[simp]

theorem CSD.Empirical.B92.b92_encode_false : b92_encode false = BB84.ket0

@[simp]

theorem CSD.Empirical.B92.b92_encode_true : b92_encode true = BB84.ketPlus

Supporting facts on the two encoding states

theorem CSD.Empirical.B92.half : (↑√2)⁻¹ * (↑√2)⁻¹ = 1 / 2

(√2⁻¹)² = ½, the only nonalgebraic fact used below.

theorem CSD.Empirical.B92.ket0_unit : ‖BB84.ket0‖ = 1

‖|0⟩‖ = 1 (from BB84's ⟨0|0⟩ = 1).

theorem CSD.Empirical.B92.ketPlus_inner_self : inner ℂ BB84.ketPlus BB84.ketPlus = 1

⟨+|+⟩ = 1, used to get ‖|+⟩‖ = 1.

theorem CSD.Empirical.B92.ketPlus_unit : ‖BB84.ketPlus‖ = 1

‖|+⟩‖ = 1.

theorem CSD.Empirical.B92.ketMinus_inner_ketPlus : inner ℂ BB84.ketMinus BB84.ketPlus = 0

X-basis orthogonality ⟨−|+⟩ = 0. Not needed by BB84; it is the second zero-overlap that makes a |−⟩ click conclusive for bit 0.

theorem CSD.Empirical.B92.b92_encoding_witness : inner ℂ BB84.ket0 BB84.ketPlus ≠ 0 ∧ inner ℂ BB84.ket0 BB84.ketPlus ≠ 1

The B92 encoding pair is non-orthogonal and not equal up to phase: ⟨0|+⟩ ∉ {0, 1}. This is the witness that drives b92_no_perfect_eavesdrop.

The B92 security theorems

theorem CSD.Empirical.B92.b92_nonorthogonal : inner ℂ BB84.ket0 BB84.ketPlus ≠ 0

The non-orthogonality resource. The two B92 encoding states are non-orthogonal, ⟨0|+⟩ ≠ 0 (reuses BB84). This is why Bob's discrimination is only ever conclusive with probability < 1, and why Eve cannot clone.

theorem CSD.Empirical.B92.b92_unambiguous_one : BB84.bornProb BB84.ket1 BB84.ket0 = 0

Conclusive detection of bit 1 is error-free. A |1⟩ (Z) click is impossible from the bit-0 state |0⟩: bornProb |1⟩ |0⟩ = 0. So whenever Bob reads |1⟩ he conclusively knows Alice sent bit 1.

theorem CSD.Empirical.B92.b92_unambiguous_zero : BB84.bornProb BB84.ketMinus BB84.ketPlus = 0

Conclusive detection of bit 0 is error-free. A |−⟩ (X) click is impossible from the bit-1 state |+⟩: bornProb |−⟩ |+⟩ = 0. So whenever Bob reads |−⟩ he conclusively knows Alice sent bit 0.

theorem CSD.Empirical.B92.b92_conclusive_rate_one : BB84.bornProb BB84.ket1 BB84.ketPlus = 1 / 2

Matched-round conclusive rate for bit 1. When Alice sends bit 1 (|+⟩) and Bob measures Z, he gets the conclusive |1⟩ click with Born probability ½: bornProb |1⟩ |+⟩ = ½.

theorem CSD.Empirical.B92.b92_conclusive_rate_zero : BB84.bornProb BB84.ketMinus BB84.ket0 = 1 / 2

Matched-round conclusive rate for bit 0. When Alice sends bit 0 (|0⟩) and Bob measures X, he gets the conclusive |−⟩ click with Born probability ½: bornProb |−⟩ |0⟩ = ½.

theorem CSD.Empirical.B92.b92_no_perfect_eavesdrop {Htensor : Type u_1} [NormedAddCommGroup Htensor] [InnerProductSpace ℂ Htensor] (tensor : EuclideanSpace ℂ (Fin 2) → EuclideanSpace ℂ (Fin 2) → Htensor) (h_tensor_inner : ∀ (a b c d : EuclideanSpace ℂ (Fin 2)), inner ℂ (tensor a b) (tensor c d) = inner ℂ a c * inner ℂ b d) (e0 : EuclideanSpace ℂ (Fin 2)) (he0 : ‖e0‖ = 1) : ¬∃ (U : Htensor → Htensor), (∀ (x y : Htensor), inner ℂ (U x) (U y) = inner ℂ x y) ∧ U (tensor BB84.ket0 e0) = tensor BB84.ket0 BB84.ket0 ∧ U (tensor BB84.ketPlus e0) = tensor BB84.ketPlus BB84.ketPlus

B92 no-perfect-eavesdropping (security capstone). Over any tensor structure with the inner-product factorisation ⟨tensor a b, tensor c d⟩ = ⟨a,c⟩·⟨b,d⟩ and a fixed unit blank e0, no isometry can clone both B92 encoding states |0⟩ and |+⟩ against the same blank. Because the two encodings are non-orthogonal (b92_encoding_witness), Eve cannot copy Alice's signal — she cannot eavesdrop without disturbance. An exact instance of NoCloning.no_universal_cloner_of_witness, the same shape as quantum_money_unforgeable.