One-Time Pad

The one-time pad (Vernam cipher) over BitVec l ([KatzLindell2020], 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 ([KatzLindell2020], Theorem 2.10)

References

• [J. Katz, Y. Lindell, Introduction to Modern Cryptography][KatzLindell2020]

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 ([KatzLindell2020], Construction 2.9).

Equations

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

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

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