The cyclic system $T_i M_j = E_{i+j \bmod n}$ has perfect secrecy

Open

ShannonSecrecy.cyclic_cipher_perfect_secrecy

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

cryptographyinformation-theoryprobability

Shannon 1949, §10, p. 681, Fig. 5. Perfect secrecy is attainable with exactly as many keys as messages.

Number the messages and the cryptograms $1, \dots, n$ and take $n$ equally likely keys, the key $i$ acting by

T_i M_j = E_s, \qquad s = i + j \ (\mathrm{mod}\ n).

Then, whatever the a priori message distribution, every cryptogram has probability $1/n$ and the a posteriori probability of each message equals its a priori probability, so the system has perfect secrecy. This is the finite one-time pad: it shows that the bound "at least as many keys as messages" is attained.

Formalization Note The messages, keys and cryptograms are all $\mathbb{Z}/n\mathbb{Z}$ for $n \ge 1$ , the enciphering map is $T_k(m) = k + m$ , and the key distribution is uniform, $P(k) = 1/n$ . Perfect secrecy is the property quantified over all a priori message distributions, so the statement is not about one particular distribution of messages.

Preamble

import Definitions.Def_shannon_secrecy_system

Formal statement

namespace ShannonSecrecy

theorem cyclic_cipher_perfect_secrecy (n : ℕ) [NeZero n] :
    PerfectSecrecy (cyclicCipher n) := 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 example accompanying Fig. 5)

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.

Fix a natural number $n$ with $n \neq 0$ . Consider the cipher whose message, key and cryptogram sets are all $\mathbb{Z}/n\mathbb{Z}$ , whose enciphering map is $T_k(m) = k + m$ computed in $\mathbb{Z}/n\mathbb{Z}$ , and whose key weights are the constant $P(k) = 1/n$ .

The statement asserts that this cipher has the perfect-secrecy property: for every function $p : \mathbb{Z}/n\mathbb{Z} \to \mathbb{R}$ with $p(m) \ge 0$ for all $m$ and $\sum_{m} p(m) = 1$ , for every $e \in \mathbb{Z}/n\mathbb{Z}$ such that

Q_p(e) \;=\; \sum_{m}\sum_{k} \begin{cases} p(m)\cdot \tfrac1n & k + m = e\\ 0 & \text{else}\end{cases} \;\neq\; 0,

and for every $m$ ,

\frac{\displaystyle\sum_{k} \begin{cases} p(m)\cdot\tfrac1n & k+m = e\\ 0 & \text{else}\end{cases}}{Q_p(e)} \;=\; p(m).

The claim is made for a single fixed family of ciphers — one for each $n \ge 1$ — and quantifies over all a priori distributions $p$ . The case $n = 1$ is included: there is then exactly one message, one key and one cryptogram. Nothing is asserted about other ciphers, and no minimality of the number of keys is part of the statement.

View graph

The cyclic system TiMj=Ei+j mod nT_i M_j = E_{i+j \bmod n}Ti​Mj​=Ei+jmodn​ has perfect secrecy

The cyclic system $T_i M_j = E_{i+j \bmod n}$ has perfect secrecy