One-Time Pad

The one-time pad (Vernam cipher) over BitVec l ([KL20], Construction 2.9).

Main definitions

• Cslib.Crypto.Protocols.PerfectSecrecy.otp: the one-time pad encryption scheme

Main results

• Cslib.Crypto.Protocols.PerfectSecrecy.otp_perfectlySecret: the one-time pad is perfectly secret ([KL20], Theorem 2.10)

References

• J. Katz, Y. Lindell, Introduction to Modern Cryptography

noncomputable def Cslib.Crypto.Protocols.PerfectSecrecy.otp (l : ℕ) : EncScheme (BitVec l) (BitVec l) (BitVec l)

The one-time pad over l-bit strings. Encryption and decryption are XOR ([KL20], Construction 2.9).

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Crypto.Protocols.PerfectSecrecy.otp_ciphertextDist_eq_uniform (l : ℕ) (m : BitVec l) : (otp l).ciphertextDist m = PMF.uniformOfFintype (BitVec l)

The ciphertext distribution of the OTP is uniform, regardless of the message: masking with a uniform key is the permutation Equiv.xor of the uniform distribution.

theorem Cslib.Crypto.Protocols.PerfectSecrecy.otp_perfectlySecret (l : ℕ) : (otp l).PerfectlySecret

The one-time pad is perfectly secret ([KL20], Theorem 2.10).