Security

Degraded discrete memoryless wiretap channel

A sender communicates reliably to a legitimate receiver while keeping the message secret from a degraded eavesdropper.

Solved Lean: not started

01 · Model

Channel specification

Input

$X\in\mathcal X$

Output

Legitimate output $Y\in\mathcal Y$ and eavesdropper output $Z\in\mathcal Z$.

Law

The channel is memoryless and physically degraded: $X\to Y\to Z$.

Reliability is required at the legitimate receiver.
Information leakage to the eavesdropper vanishes under the chosen secrecy criterion.

02 · Capacity

C_s=\max_{P_X}\bigl[I(X;Y)-I(X;Z)\bigr]

Conditions. The channel is physically degraded.

Symbol: $C_s$
Error criterion: Reliable communication with asymptotically vanishing leakage.

03 · Evidence

Type	Claim	Method	Source
lower	$C_s\ge\max_{P_X}[I(X;Y)-I(X;Z)]$	Stochastic encoding and random binning.	1975 [1]
upper	$C_s\le\max_{P_X}[I(X;Y)-I(X;Z)]$	Fano's inequality, secrecy, and degradedness.	1975 [1]

04 · History

1975
Wyner introduced the wiretap channel and proved the degraded secrecy-capacity formula.
Reference

05 · Lean

Lean: not started

Secrecy criteria and mutual-information converses are not yet present in the Lean core.

No Lean file is linked yet. A contribution should begin by reusing the shared definitions under lean/CapacityAtlas.

References

Aaron D. Wyner (1975). The wire-tap channel. Bell System Technical Journal. doi:10.1002/j.1538-7305.1975.tb02040.x
Thomas M. Cover and Joy A. Thomas (2006). Elements of Information Theory. Wiley, second edition. doi:10.1002/047174882X

Keep exploring

Point-to-point Updated 2026-08-09

Solved Lean: definitions

Each bit is independently flipped with probability p. This is the canonical finite noisy channel.

Multi-user Updated 2026-08-09

Open Lean: not started

A relay assists communication from a source to a destination. Decode-forward and the cut-set bound do not coincide in general.

Point-to-point Updated 2026-08-09

Solved Lean: definitions

Each transmitted bit is either received correctly or replaced by a visible erasure symbol.