Minimal perfect systems are Latin squares with equiprobable keys

Open

ShannonSecrecy.perfect_secrecy_latin_square

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

combinatoricscryptographyinformation-theory

Shannon 1949, §10, p. 681. Perfect systems in which the number of cryptograms, the number of messages, and the number of keys are all equal are characterized by the properties that (1) each message is connected to each cryptogram by exactly one line, and (2) all keys are equally likely; thus the matrix representation of the system is a "Latin square".

Concretely: let a finite secrecy system have perfect secrecy and satisfy $|M| = |K| = |E|$ . Then

for every message $M$ and every cryptogram $E$ there is exactly one key $k$ with $T_k M = E$ , and
all keys have the same a priori probability (necessarily $1/|K|$ ).

Consequently the $|M| \times |E|$ table whose $(M, E)$ entry is the unique key carrying $M$ to $E$ is a Latin square: each key occurs exactly once in each row and once in each column. This identifies the minimal perfect systems — those meeting the bound "as many keys as messages" — up to relabelling.

Formalization Note "Exactly one line from $M$ to $E$ " is the unique-existence of a key $k$ with $T_k M = E$ ; "all keys equally likely" is stated as the equality of the a priori probabilities of any two keys, from which the value $1/|K|$ follows by normalization. The cardinality hypotheses are exactly Shannon's "the number of cryptograms, the number of messages, and the number of keys are all equal".

Preamble

import Definitions.Def_shannon_secrecy_system

Formal statement

namespace ShannonSecrecy

theorem perfect_secrecy_latin_square
    {M K E : Type*} [Fintype M] [Fintype K] [Fintype E] [DecidableEq E]
    (C : Cipher M K E) (h : PerfectSecrecy C)
    (hMK : Fintype.card M = Fintype.card K) (hKE : Fintype.card K = Fintype.card E) :
    (∀ (m : M) (e : E), ∃! k : K, C.encipher k m = e) ∧
      ∀ k k' : K, C.keyProb k = C.keyProb 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 characterizing perfect systems as Latin squares)

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: injective maps $T_k : M \to E$ for $k \in K$ , weights $P(k) \ge 0$ with $\sum_k P(k) = 1$ . Assume:

$C$ has the perfect-secrecy property — for every $p : M \to \mathbb{R}$ with $p \ge 0$ and $\sum_m p(m) = 1$ , for every $e$ with nonzero total probability $Q_p(e)$ , and for every $m$ , the a posteriori ratio $\big(\sum_{k : T_k(m) = e} p(m)P(k)\big)/Q_p(e)$ equals $p(m)$ ;
$\#M = \#K$ ;
$\#K = \#E$ .

The conclusion is a conjunction:

(i) for every message $m$ and every cryptogram $e$ there exists a unique key $k$ with $T_k(m) = e$ — existence and uniqueness, for every pair, with no exclusion of any $m$ or $e$ ;
(ii) for all keys $k, k'$ , $P(k) = P(k')$ ; that is, the key weights are constant. The common value is not named in the statement, although constancy together with $\sum_k P(k) = 1$ pins it down.

Degenerate case: if all three types are empty — excluded here, since $\sum_{k} P(k) = 1$ forces $K$ to be nonempty — both clauses would be vacuous. With $\#K \ge 1$ the cardinality hypotheses force $M$ and $E$ to be nonempty as well, so clause (i) has content. Nothing in the conclusion mentions a Latin square or a matrix; it is the pair of properties (i) and (ii) only.

View graph