One-time pad over a finite group

DefinitionThe group one-time pad#✓fully proved

Let \(G\) be a finite group. The group one-time pad on \(G\) is the private-key encryption scheme with messages, keys and ciphertexts in \(G\) whose key \(k\) is drawn uniformly from \(G\), which encrypts a message \(m\) as \(k m\), and which decrypts a ciphertext \(c\) as \(k^{-1} c\).

noncomputable def groupOTP : EncScheme G G G :=
  .ofPure (Cslib.Probability.PMF.uniformOfFintype G) (· * ·) (fun k c => k⁻¹ * c) fun k m => by simp

Used by 2

Used byGroup one-time pad ciphertexts are uniform · The group one-time pad is perfectly secret

TheoremGroup one-time pad ciphertexts are uniform#✓fully proved

Let \(G\) be a finite group. For every message \(m \in G\), the ciphertext of \(m\) under the group one-time pad on \(G\), whose key is drawn uniformly from \(G\), is uniformly distributed on \(G\).

theorem groupOTP_ciphertextDist_eq_uniform (m : G) :
    (groupOTP G).ciphertextDist m = Cslib.Probability.PMF.uniformOfFintype G

Uses 1 · Used by 1

Statement usesThe group one-time pad

Used byThe group one-time pad is perfectly secret

TheoremThe group one-time pad is perfectly secret#✓fully proved

Let \(G\) be a finite group. The group one-time pad on \(G\) is perfectly secret: for every probability distribution on messages in \(G\) and every ciphertext \(c\) that occurs with positive probability, the conditional distribution of the message given that the ciphertext is \(c\) equals the prior distribution of the message.

theorem groupOTP_perfectlySecret : (groupOTP G).PerfectlySecret

Sources

• Katz and Lindell, Lemma 11.15.

Uses 2

Statement usesThe group one-time pad

Proof usesGroup one-time pad ciphertexts are uniform

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.