One-Time Pad: Internal proofs

The OTP ciphertext distribution is uniform regardless of message.

@[implicit_reducible]

instance Cslib.Crypto.Protocols.PerfectSecrecy.OTP.bitVecFintype (n : ℕ) : Fintype (BitVec n)

Equations

• Cslib.Crypto.Protocols.PerfectSecrecy.OTP.bitVecFintype n = Fintype.ofEquiv (Fin (2 ^ n)) { toFun := BitVec.ofFin, invFun := BitVec.toFin, left_inv := ⋯, right_inv := ⋯ }

theorem Cslib.Crypto.Protocols.PerfectSecrecy.OTP.eq_xor_iff_xor_eq {l : ℕ} (c m k : BitVec l) : c = k ^^^ m ↔ c ^^^ m = k

XOR by a fixed mask is self-inverse on BitVec: c = k ^^^ m ↔ c ^^^ m = k.

theorem Cslib.Crypto.Protocols.PerfectSecrecy.OTP.otp_ciphertextDist_eq_uniform (l : ℕ) (m : BitVec l) : ((PMF.uniformOfFintype (BitVec l)).bind fun (k : BitVec l) => PMF.pure (k ^^^ m)) = PMF.uniformOfFintype (BitVec l)

The ciphertext distribution of the OTP is uniform, regardless of the message.