Authenticated encryption with associated data

Confidentiality and authenticity are computational and are not stated as laws. The laws are correctness (decrypt_encrypt), fixed tag expansion (size_encrypt), and soundness (decrypt_sound): decrypt only accepts ciphertexts that encrypt produces. Together they make decrypt the partial inverse of encrypt (decrypt_eq_some_iff).

The nonce is an explicit argument; choosing unique nonces is the caller's responsibility. Failure is Option so that no failure reason is reported.

structure Cryptlib.Primitives.Cipher.AEAD.AEAD : Type 1

• Key : Type

  Opaque, so an implementation may carry a precomputed key schedule.

• name : String
• keySize : Nat
• nonceSize : Nat
• tagSize : Nat
• maxPlaintextSize : Nat

  The largest plaintext, in bytes, for which the security claim holds. Not used by any law.

• maxADSize : Nat

  The largest associated data, in bytes, for which the security claim holds.

• keyFromBytes : Vector UInt8 self.keySize → self.Key
• encrypt : self.Key → Vector UInt8 self.nonceSize → (ad pt : ByteArray) → ByteArray
• decrypt : self.Key → Vector UInt8 self.nonceSize → (ad ct : ByteArray) → Option ByteArray
• size_encrypt (k : self.Key) (n : Vector UInt8 self.nonceSize) (ad pt : ByteArray) : (self.encrypt k n ad pt).size = pt.size + self.tagSize

  The tag is the only expansion.

• decrypt_encrypt (k : self.Key) (n : Vector UInt8 self.nonceSize) (ad pt : ByteArray) : self.decrypt k n ad (self.encrypt k n ad pt) = some pt

  Correctness, unconditional on length limits.

• decrypt_sound (k : self.Key) (n : Vector UInt8 self.nonceSize) (ad ct pt : ByteArray) : self.decrypt k n ad ct = some pt → self.encrypt k n ad pt = ct

  Soundness: only ciphertexts produced by encrypt under the same key, nonce and associated data are accepted.

theorem Cryptlib.Primitives.Cipher.AEAD.AEAD.decrypt_eq_some_iff (A : AEAD) (k : A.Key) (n : Vector UInt8 A.nonceSize) (ad ct pt : ByteArray) : A.decrypt k n ad ct = some pt ↔ A.encrypt k n ad pt = ct

A ciphertext decrypts to a plaintext exactly when it is that plaintext's encryption.

theorem Cryptlib.Primitives.Cipher.AEAD.AEAD.decrypt_of_size_lt (A : AEAD) (k : A.Key) (n : Vector UInt8 A.nonceSize) (ad ct : ByteArray) (h : ct.size < A.tagSize) : A.decrypt k n ad ct = none

Nothing shorter than a tag is accepted.

theorem Cryptlib.Primitives.Cipher.AEAD.AEAD.size_of_decrypt (A : AEAD) (k : A.Key) (n : Vector UInt8 A.nonceSize) (ad ct pt : ByteArray) (h : A.decrypt k n ad ct = some pt) : ct.size = pt.size + A.tagSize

A ciphertext's length determines its plaintext's length.

theorem Cryptlib.Primitives.Cipher.AEAD.AEAD.decrypt_inj (A : AEAD) (k : A.Key) (n : Vector UInt8 A.nonceSize) (ad ct₁ ct₂ pt : ByteArray) (h₁ : A.decrypt k n ad ct₁ = some pt) (h₂ : A.decrypt k n ad ct₂ = some pt) : ct₁ = ct₂

Distinct ciphertexts cannot decrypt to the same plaintext under one key, nonce and associated data.

@[instance_reducible]

instance Cryptlib.Primitives.Cipher.AEAD.instInhabitedAEAD : Inhabited AEAD

The identity cipher, showing the laws are satisfiable. Provides no security.

Equations

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