Channel and question
- Input
- A stochastic encoder maps independent uniform messages \(M_0,M_1\) to \(X^n\) over a finite alphabet, using private randomness.
- Output
- Receiver 1 observes \(Y^n\) and decodes both messages; receiver 2 observes \(Z^n\) and decodes \(M_0\).
- Law
- A fixed finite memoryless broadcast channel with marginals \(W_Y(y\mid x)\) and \(W_Z(z\mid x)\).
- Quantity
- Common-message and confidential-message capacity region \(\mathcal C_{\mathrm{BCC}}\), measured in bits per channel use.
Criterion. The closed set of nonnegative rate pairs \((R_0,R_1)\), normalized by blocklength, attainable at every sufficiently large blocklength with vanishing errors and normalized leakage.
- There is no feedback, receiver cooperation, shared secret key, or input-cost constraint.
- Each decoder uses only its own output. Arbitrary correlation between receiver outputs within a use does not change this operational region.
- Both average decoding errors vanish, and weak secrecy requires \(I(M_1;Z^n)/n\to0\).
Current status
\[\mathcal C_{\mathrm{BCC}}=\overline{\bigcup_{U-V-X-(Y,Z)}\{(R_0,R_1)\ge0:\ R_0\le\min\{I(U;Y),I(U;Z)\},\ R_1\le I(V;Y\mid U)-I(V;Z\mid U)\}}\]
The union ranges over all finite auxiliaries and stochastic prefixes. This is the perfect-secrecy specialization of the Csiszár–Körner rate-equivocation region; Bloch–Laneman Theorem 3, equation (9), also states this region for weak-secrecy metric S4. No auxiliary-cardinality bound is imposed here.
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(\mathcal C_{\mathrm{BCC}}\supseteq\overline{\bigcup_{U-V-X-(Y,Z)}\{(R_0,R_1)\ge0:\ R_0\le\min\{I(U;Y),I(U;Z)\},\ R_1\le I(V;Y\mid U)-I(V;Z\mid U)\}}\) | Superposition coding, stochastic prefixing, and randomization for secrecy. | 1978 |
| Upper | \(\mathcal C_{\mathrm{BCC}}\subseteq\overline{\bigcup_{U-V-X-(Y,Z)}\{(R_0,R_1)\ge0:\ R_0\le\min\{I(U;Y),I(U;Z)\},\ R_1\le I(V;Y\mid U)-I(V;Z\mid U)\}}\) | Fano inequalities, the Csiszár sum identity, and time sharing. | 1978 |
Formal verification
Lean coverageFormally stated
The local proof constructs stochastic block codes and proves achievability and converse, including zero-rate boundaries. It uses weak secrecy; it does not formalize strong secrecy or auxiliary-cardinality bounds.
Claims
- The operational weak-secrecy region equals the closure of the finite-auxiliary common-message and confidential-message region.
capacity-region· exact capacity · solved · Formally proved · v1
Lean declarations (4)
CapacityAtlas.ConfidentialBroadcast.Codedefinition
lean/CapacityAtlasForMathlib/InformationTheory/ConfidentialBroadcast/Basic.lean — Stochastic encoder with two independent messages and separate receiver decoders.CapacityAtlas.ConfidentialBroadcast.capacityRegiondefinition
lean/CapacityAtlasForMathlib/InformationTheory/ConfidentialBroadcast/Basic.lean — Vanishing average errors and normalized information leakage, with rate closure.CapacityAtlas.ConfidentialBroadcast.informationRegiondefinition
lean/CapacityAtlasForMathlib/InformationTheory/ConfidentialBroadcast/Basic.lean — Closure of the union over finite auxiliaries and stochastic prefixes.CapacityAtlas.Claims.confidentialBroadcastCapacityclaim · capacity-region
lean/CapacityAtlas/Claims/ConfidentialBroadcast.lean — Locally proved equality of operational and single-letter regions.
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.
- Matthieu R. Bloch and J. Nicholas Laneman (2013). Strong Secrecy from Channel Resolvability. IEEE Transactions on Information Theory.