Perfect secrecy requires at least as many keys as messages

Open

ShannonSecrecy.perfect_secrecy_card_msg_le_card_key

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

combinatoricscryptographyinformation-theory

Shannon 1949, §10, p. 681. In a finite secrecy system with perfect secrecy, the number of different keys is at least as great as the number of messages.

Shannon's reasoning: for a fixed key $i$ , the map $T_i$ is a one-to-one correspondence between all the messages and some of the cryptograms, so there are at least as many cryptograms as messages. For perfect secrecy $P_M(E) = P(E) \neq 0$ for any of these cryptograms and any message, hence there is at least one key transforming any given message into any of them. All the keys leading from a fixed message to different cryptograms must be different, and therefore the number of different keys is at least as great as the number of messages.

This is the first quantitative limitation on perfect secrecy, and the origin of the one-time-pad requirement that the key be at least as long as the message.

Formalization Note "Number of messages" and "number of keys" are the cardinalities of the finite types $M$ and $K$ ; the conclusion is the inequality $|M| \le |K|$ . No nonemptiness is assumed: a key set is automatically nonempty because the key probabilities sum to $1$ , and keys of probability $0$ are allowed, so the counting argument must locate keys of positive probability.

Preamble

import Definitions.Def_shannon_secrecy_system

Formal statement

namespace ShannonSecrecy

theorem perfect_secrecy_card_msg_le_card_key
    {M K E : Type*} [Fintype M] [Fintype K] [Fintype E] [DecidableEq E]
    (C : Cipher M K E) (h : PerfectSecrecy C) :
    Fintype.card M ≤ Fintype.card K := 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. 681 (Part II, §10 Perfect Secrecy, the paragraph following Theorem 6)

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$ , $E$ be finite types with decidable equality on $E$ , and let $C$ be a cipher on them: injective maps $T_k : M \to E$ for each $k \in K$ , together with weights $P(k) \ge 0$ satisfying $\sum_{k \in K} P(k) = 1$ .

Assume $C$ has the perfect-secrecy property, namely: for every $p : M \to \mathbb{R}$ with $p \ge 0$ pointwise and $\sum_m p(m) = 1$ , for every $e \in E$ whose total probability

Q_p(e) = \sum_{m \in M}\sum_{k \in K}\begin{cases} p(m)P(k) & T_k(m) = e\\ 0 & \text{else}\end{cases}

is nonzero, and for every $m \in M$ , the ratio of $\sum_{k : T_k(m) = e} p(m) P(k)$ to $Q_p(e)$ equals $p(m)$ .

The conclusion is the inequality of natural numbers

\#M \;\le\; \#K,

that is, the number of elements of the message type is at most the number of elements of the key type. Nothing is claimed about $\#E$ . The hypothesis is not vacuous in general, but note two degenerate readings it permits: if $M$ is empty, there is no PMF on $M$ , so the perfect-secrecy hypothesis holds for every cipher and the conclusion $0 \le \#K$ is trivially true; keys of probability zero are permitted and are counted in $\#K$ .

View graph