TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

QKD composable secrecy is bounded by correctness plus secrecy

Statement

For every finite authenticated key-distribution protocol and each fixed allowed adversarial strategy, let $δ_{i d}$ , $ε_{c o r}$ , and $ε_{s e c}$ be as in Abort-aware real and ideal QKD outputs and security errors. Then

$δ_{i d} \leq ε_{c o r} + ε_{s e c} .$

Consequently, if correctness and secrecy errors are bounded uniformly over all allowed adversarial strategies by $ε_{c o r}$ and $ε_{s e c}$ , respectively, then the real-ideal trace distance is uniformly at most their sum.

Facts & Assumptions

Given: A finite protocol, one allowed adversarial strategy, and its output state and error quantities from the Definition.

[F1]

Abort-aware real and ideal QKD outputs and security errors: the ideal output has the same abort blocks as the real output, and on acceptance is the uniform shared key tensored with the actual transcript-adversary marginal; $ε_{s e c}$ and $ε_{c o r}$ include the acceptance weighting.

[F2]

The abort-aware ideal output and conditional marginals are states: the normalized real and ideal full outputs and all normalized accepted marginals in the trace distances are density operators; the zero-acceptance case gives identical outputs.

[F3]

The finite classical key-copy map is a quantum channel: $C$ copies each classical Alice-key block into the shared $(A, B)$ key block and leaves transcript and adversary factors unchanged.

[F4]

Replacing Bob's key by a copy of Alice's costs the correctness error: for the accepted state, copying Alice's key changes it by trace distance exactly $\Pr [K_{A} \neq K_{B} ∣ a c c e p t]$ .

[F5]

Trace norm of a finite classical block operator: block-diagonal trace norms add over finite classical labels.

[F6]

Trace Distance and Trace Norm Duality And Norm Properties: state trace distance is half the trace norm and the trace norm satisfies the triangle inequality and scalar homogeneity.

Proof

1.1givenF1F2F5F6algebra

If $p_{a c c} = 0$ , [F2] gives $ρ_{A B T E}^{r e a l} = ρ_{A B T E}^{i d e a l}$ ; both errors are zero by [F1], so the claim holds. Suppose $p_{a c c} > 0$ , and write $ρ_{A B T E}^{⊤}$ for the normalized accepted real state and $σ_{A B T E}^{⊤} : = τ_{A B} \otimes ρ_{T E}^{⊤}$ for the normalized accepted ideal state. The abort blocks cancel in the real-ideal difference. By [F5] the remaining block is the accepted block scaled by $p_{a c c}$ , so [F6] gives $δ_{i d} = p_{a c c} D (ρ_{A B T E}^{⊤}, σ_{A B T E}^{⊤})$ .

1.2givenF2F3F4

Define $γ_{A B T E} : = C (ρ_{A T E}^{⊤})$ . The state $ρ_{A T E}^{⊤}$ is classical in $A$ and $T$ , and the copy formula [F3] gives $γ$ by replacing Bob's accepted key with Alice's. Thus [F4] gives $D (ρ_{A B T E}^{⊤}, γ_{A B T E}) = q$ , where $q : = \Pr [K_{A} \neq K_{B} ∣ a c c e p t]$ .

1.3givenF3F5F6algebra

The uniform product input $τ_{A} \otimes ρ_{T E}^{⊤}$ is classical in $A, T$ , and [F3] gives $C (τ_{A} \otimes ρ_{T E}^{⊤}) = σ_{A B T E}^{⊤}$ . The difference $ρ_{A T E}^{⊤} - τ_{A} \otimes ρ_{T E}^{⊤}$ has one self-adjoint $T E$ block for each $(a, t)$ ; after copying, exactly those blocks occupy slots $(a, a, t)$ and every other $A B T$ slot is zero. The block trace-norm identity [F5] therefore gives $D (γ_{A B T E}, σ_{A B T E}^{⊤}) = D (ρ_{A T E}^{⊤}, τ_{A} \otimes ρ_{T E}^{⊤})$ .

2.1givenF1F6step 1.1step 1.2step 1.3algebra∎

By the triangle inequality from [F6], steps 1.2–1.3 yield $D (ρ_{A B T E}^{⊤}, σ_{A B T E}^{⊤}) \leq q + D (ρ_{A T E}^{⊤}, τ_{A} \otimes ρ_{T E}^{⊤})$ . Multiply by $p_{a c c}$ and use [F1]: $p_{a c c} q = ε_{c o r}$ because mismatch occurs only on acceptance, and $p_{a c c} D (ρ_{A T E}^{⊤}, τ_{A} \otimes ρ_{T E}^{⊤}) = ε_{s e c}$ . Step 1.1 now gives $δ_{i d} \leq ε_{c o r} + ε_{s e c}$ . Since the strategy was arbitrary, the uniform statement follows by applying the same inequality to each strategy.

Depends on

Used by

Dependency tree · two levels

37 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Christopher Portmann and Renato Renner, Cryptographic Security of Quantum Key Distribution (2014), Theorem 4.1 (standard reference, not scraped)
Joseph M. Renes, Quantum Information Theory, ETH Zürich lecture notes (HS2014; revised 4 February 2015), §8.3, Proposition 8.3.1 (standard reference, not scraped)
John Watrous, The Theory of Quantum Information (2018), Chapter 1, §1.1.3 (standard reference, not scraped)