AES-256-GCM (NIST SP 800-38D), 96-bit nonces and 128-bit tags

Nonces must not repeat under one key.

@[reducible, inline]

abbrev Cryptlib.Primitives.Cipher.AESGCM.Key : Type

Equations

• Cryptlib.Primitives.Cipher.AESGCM.Key = Vector UInt8 32

@[reducible, inline]

abbrev Cryptlib.Primitives.Cipher.AESGCM.Nonce : Type

Equations

• Cryptlib.Primitives.Cipher.AESGCM.Nonce = Vector UInt8 12

def Cryptlib.Primitives.Cipher.AESGCM.gctr (key : Key) (n : Nonce) (d : ByteArray) : ByteArray

Equations

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

def Cryptlib.Primitives.Cipher.AESGCM.tagOf (key : Key) (n : Nonce) (ad ct : ByteArray) : ByteArray

E(K, J₀) ⊕ GHASH_H(pad(A) ‖ pad(C) ‖ BE64(|A| bits) ‖ BE64(|C| bits)), H = E(K, 0¹²⁸).

Equations

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

def Cryptlib.Primitives.Cipher.AESGCM.encrypt (key : Key) (n : Nonce) (ad pt : ByteArray) : ByteArray

Equations

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

def Cryptlib.Primitives.Cipher.AESGCM.decrypt (key : Key) (n : Nonce) (ad ct : ByteArray) : Option ByteArray

Structural equality on the tag; a deployed implementation must compare in constant time.

Equations

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

theorem Cryptlib.Primitives.Cipher.AESGCM.decrypt_sound (key : Key) (n : Nonce) (ad ct pt : ByteArray) (h : decrypt key n ad ct = some pt) : encrypt key n ad pt = ct

def Cryptlib.Primitives.Cipher.AESGCM.Scheme : AEAD.AEAD

Equations

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