Bayes' theorem for a secrecy system: $P_E(M) = P(M)P_M(E)/P(E)$

Open

ShannonSecrecy.bayes_posterior_probability

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

cryptographyinformation-theoryprobability

Shannon 1949, §10, p. 680 (the Bayes relation). In a finite secrecy system with a priori message distribution $p$ , the probability of a cryptogram and the a posteriori probability of a message are related by

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

where $P(M)$ is the a priori probability of the message $M$ ; $P_M(E)$ is the conditional probability of the cryptogram $E$ if the message $M$ is chosen, i.e. the sum of the probabilities of all keys which produce $E$ from $M$ ; $P(E)$ is the probability of obtaining the cryptogram $E$ from any cause; and $P_E(M)$ is the a posteriori probability of the message $M$ if the cryptogram $E$ is intercepted.

The first identity says that the cryptogram probability decomposes over the possible messages; the second is Bayes' theorem in the form Shannon uses to derive his necessary and sufficient condition for perfect secrecy. Together they are the bookkeeping on which the whole of §10 is based.

Formalization Note The a posteriori probability is defined as the joint probability of the pair (message, cryptogram) divided by the total probability of the cryptogram; the content of the statement is that this joint probability factors as $P(M) P_M(E)$ , the message and the key being chosen independently. Both sides are real numbers, and the identity is asserted for every real-valued $p$ , including cryptograms of probability zero, where both sides are $0$ under Lean's division convention.

Preamble

import Definitions.Def_shannon_secrecy_system

Formal statement

namespace ShannonSecrecy

theorem bayes_posterior_probability
    {M K E : Type*} [Fintype M] [Fintype K] [Fintype E] [DecidableEq E]
    (C : Cipher M K E) (p : M → ℝ) (e : E) (m : M) :
    cryptoProb C p e = ∑ m' : M, p m' * msgToCrypto C m' e ∧
      postProb C p e m = p m * 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 (Part II, §10 Perfect Secrecy, the displayed Bayes formula and the list of its four quantities)

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$ , 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$ ), let $p : M \to \mathbb{R}$ be an arbitrary function — no non-negativity or normalization is assumed — and fix $e \in E$ and $m \in M$ . Write

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

The statement is the conjunction of two equalities of real numbers:

\text{(i)}\quad Q(e) \;=\; \sum_{m' \in M} p(m')\, w(m',e), \qquad\qquad \text{(ii)}\quad \frac{\displaystyle\sum_{k\in K}\begin{cases} p(m)P(k) & T_k(m)=e\\ 0 & \text{else}\end{cases}}{Q(e)} \;=\; \frac{p(m)\,w(m,e)}{Q(e)}.

Both quotients in (ii) are real divisions by the same quantity $Q(e)$ , and no hypothesis excludes $Q(e) = 0$ ; in that case both sides are $0$ by the convention that division by zero yields zero, so (ii) holds in that case as well. The claim is purely an identity of finite sums: it uses neither the injectivity of the maps $T_k$ , nor the non-negativity or normalization of $P$ , nor any property of $p$ .

View graph

Bayes' theorem for a secrecy system: PE(M)=P(M)PM(E)/P(E)P_E(M) = P(M)P_M(E)/P(E)PE​(M)=P(M)PM​(E)/P(E)

Bayes' theorem for a secrecy system: $P_E(M) = P(M)P_M(E)/P(E)$