Shannon's Theorem 6: perfect secrecy $\iff$ $P_M(E) = P(E)$

Open

ShannonSecrecy.perfect_secrecy_iff_msgToCrypto_eq_cryptoProb

by Lucas · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

cryptographyinformation-theoryprobability

Shannon 1949, Theorem 6 (p. 680). A necessary and sufficient condition for perfect secrecy is that

P_M(E) = P(E) \qquad \text{for all } M \text{ and } E,

that is, $P_M(E)$ must be independent of $M$ .

Fix a finite secrecy system: finite sets of messages $M$ , keys $K$ and cryptograms $E$ , an injective enciphering map $T_k : M \to E$ for each key $k$ , and an a priori key distribution $P(k)$ . Write

P_M(E) \;=\; \sum_{k \,:\, T_k M = E} P(k)

for the total probability of the keys that carry the message $M$ to the cryptogram $E$ , and, for an a priori message distribution $p$ ,

P(E) \;=\; \sum_{M} p(M)\, P_M(E), \qquad P_E(M) \;=\; \frac{p(M) P_M(E)}{P(E)} .

The system has perfect secrecy when, for every a priori message distribution $p$ and every cryptogram $E$ with $P(E) \neq 0$ , the a posteriori probabilities coincide with the a priori ones: $P_E(M) = p(M)$ for all $M$ . Requiring this for every $p$ is Shannon's stipulation that the equality hold "independently of the values of $P(M)$ " — he explicitly discards the alternative escape $P(M) = 0$ .

The theorem asserts the equivalence of that condition with the statement that, for every a priori message distribution and every message–cryptogram pair, the key weight $P_M(E)$ equals the unconditional cryptogram probability $P(E)$ . Equivalently: the total probability of all keys transforming $M_i$ into a given cryptogram $E$ equals that of all keys transforming $M_j$ into the same $E$ , for all $M_i$ , $M_j$ and $E$ .

This is the structural characterization on which the rest of §10 rests: it is what makes the counting argument for the number of keys, and the Latin-square description of minimal perfect systems, possible.

Formalization Note The right-hand side quantifies over all a priori distributions $p$ ; since the left-hand side of the equality does not depend on $p$ , this is the same as saying that $P_M(E)$ is independent of $M$ together with its common value being $P(E)$ . Cryptograms of probability zero are excluded from the definition of perfect secrecy, because the a posteriori probability is a real quotient and is not meaningful there.

Preamble

import Definitions.Def_shannon_secrecy_system

Formal statement

namespace ShannonSecrecy

theorem perfect_secrecy_iff_msgToCrypto_eq_cryptoProb
    {M K E : Type*} [Fintype M] [Fintype K] [Fintype E] [DecidableEq E]
    (C : Cipher M K E) :
    PerfectSecrecy C ↔
      ∀ p : M → ℝ, IsPMF p → ∀ (m : M) (e : E), msgToCrypto C m e = cryptoProb C p e := by sorry

end ShannonSecrecy

Source

C. E. Shannon, "Communication Theory of Secrecy Systems", Bell System Technical Journal 28(4):656-715, 1949; https://doi.org/10.1002/j.1538-7305.1949.tb00928.x, p. 680, Theorem 6 (Part II, §10 Perfect Secrecy)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — NON-BLIND: same agent that drafted the statement

Provenance note — this read-back is NOT independent testimony. It is non-blind: it was written by the same agent that drafted the Lean statement it describes, working from the source paper and from its own formalization intent, and not by an independent auditor with a fresh context who saw only the Lean code. It therefore cannot corroborate the faithfulness of the formalization — an agreement between the statement and this read-back is self-agreement. Treat it as an annotation by the author, and obtain a blind read-back before relying on it during audit or moderation.

Let $M$ , $K$ and $E$ be finite types, with decidable equality on $E$ , and let $C$ be a cipher on them: a family of maps $T_k : M \to E$ indexed by $k \in K$ , each injective, together with weights $P(k) \ge 0$ summing to $1$ . Write

w(m,e) \;=\; \sum_{k \in K} \begin{cases} P(k) & T_k(m) = e \\ 0 & \text{otherwise}\end{cases}, \qquad Q_p(e) \;=\; \sum_{m \in M} \sum_{k \in K} \begin{cases} p(m) P(k) & T_k(m) = e \\ 0 & \text{otherwise.}\end{cases}

Call $p : M \to \mathbb{R}$ a PMF when $p \ge 0$ pointwise and $\sum_{m} p(m) = 1$ .

The statement asserts the equivalence of the following two conditions.

For every PMF $p$ , every $e \in E$ with $Q_p(e) \neq 0$ , and every $m \in M$ ,

\frac{\displaystyle\sum_{k \in K} \begin{cases} p(m)P(k) & T_k(m) = e\\ 0 & \text{otherwise}\end{cases}}{Q_p(e)} \;=\; p(m).

For every PMF $p$ , every $m \in M$ and every $e \in E$ (with no exclusion of the case $Q_p(e) = 0$ ), $w(m,e) = Q_p(e)$ .

Both sides range over all PMFs $p$ , so neither fixes an a priori distribution. In condition 1 the quotient is a real division, which returns $0$ when its denominator is $0$ ; that case is excluded by hypothesis. In condition 2 the left-hand side does not depend on $p$ , so the condition forces $Q_p(e)$ to be the same real number for all PMFs $p$ and the same for all messages $m$ .

Degenerate cases included by the quantifiers: if $M$ is empty, no PMF exists, so both conditions hold vacuously and the equivalence is trivially true for such a cipher; $E$ may be empty, in which case both sides are again vacuous; keys of probability $0$ are permitted, and $K$ is automatically nonempty because the weights sum to $1$ . No hypothesis requires $T_k$ to be surjective, nor the sets to have equal cardinality.

View graph

Shannon's Theorem 6: perfect secrecy ⟺ \iff⟺PM(E)=P(E)P_M(E) = P(E)PM​(E)=P(E)

Shannon's Theorem 6: perfect secrecy $\iff$ $P_M(E) = P(E)$