AES-256-GCM-SIV

RFC 8452, 256-bit keys. Nonce-misuse resistant: a repeated nonce reveals only whether two plaintexts were equal.

1. Derive a POLYVAL key and a message-encryption key from the key and nonce.
2. Tag: POLYVAL over padded AD, padded plaintext and the lengths, XORed with the nonce, top bit cleared, then encrypted under the message-encryption key.
3. Encrypt the plaintext in CTR mode, with the counter seeded from the tag.

@[reducible, inline]

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

The key-generating key.

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Cryptlib.Primitives.Cipher.AESGCMSIV.Block : Type

Equations

• Cryptlib.Primitives.Cipher.AESGCMSIV.Block = Vector UInt8 16

CTR mode is its own inverse

Sealing and opening

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

Compute the tag, encrypt under a counter seeded by it, then append the tag.

Equations

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

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

Split off the tag, decrypt, recompute the tag and accept only on equality. The comparison is not constant time.

Equations

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

The AEAD instance

theorem Cryptlib.Primitives.Cipher.AESGCMSIV.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.AESGCMSIV.Scheme : AEAD.AEAD

AES-256-GCM-SIV as an AEAD.

Equations

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