Channel and question
- Input
- Symbols in a finite alphabet \(\mathcal X\), encoded using private randomness.
- Output
- Legitimate output \(Y\) and eavesdropper output \(Z\) from two DMC marginals with common input.
- Law
- Arbitrary finite transition laws \(W_Y(y\mid x)\) and \(W_Z(z\mid x)\).
- Quantity
- Strong-secrecy capacity \(C_s\), measured in secret bits per channel use.
Criterion. Vanishing legitimate average error and strong information-theoretic secrecy.
- Messages are uniform and the stochastic encoder randomness is private.
- Legitimate average decoding error vanishes.
- Strong secrecy means unnormalized leakage \(I(M;Z^n)\) tends to zero.
Current status
\[C_s=\max_{V-X-(Y,Z)}\bigl[I(V;Y)-I(V;Z)\bigr]\]
Conditions. Finite alphabets and no input-cost constraint.
| Result | Relation | Method | Year |
|---|---|---|---|
| Exact | \(C_s=\max_{V-X-(Y,Z)}[I(V;Y)-I(V;Z)]\) | Random binning and an auxiliary-random-variable converse. | 1978 |
Formal verification
Lean coverageFormally stated
New statements await mathematical review and proofs.
Claims
- The general auxiliary-variable strong-secrecy capacity formula.
operational-capacity· exact capacity · solved · Formally stated · v1
Lean declarations (4)
CapacityAtlas.FiniteWiretapChanneldefinition
lean/CapacityAtlasForMathlib/InformationTheory/FiniteWiretapChannel.lean — Pair of finite legitimate and eavesdropper channels.CapacityAtlas.WiretapCodedefinition
lean/CapacityAtlasForMathlib/InformationTheory/FiniteWiretapChannel.lean — Finite stochastic wiretap block-code structure.CapacityAtlas.finiteWiretapAuxiliaryCapacitydefinition
lean/CapacityAtlasForMathlib/InformationTheory/FiniteWiretapChannel.lean — Single-auxiliary information expression.CapacityAtlas.Claims.generalWiretapclaim · operational-capacity
lean/CapacityAtlas/Claims/GeneralWiretap.lean — The general auxiliary-variable strong-secrecy capacity formula.
References
- Imre Csiszár and János Körner (1978). Broadcast Channels with Confidential Messages. IEEE Transactions on Information Theory. DOI 10.1109/TIT.1978.1055892.
- Sreejith Sreekumar, Alexander Bunin, Ziv Goldfeld, Haim H. Permuter, and Shlomo Shamai (2020). The Secrecy Capacity of Cost-Constrained Wiretap Channels. arXiv preprint.