ChaCha20-Poly1305 (RFC 8439)

The IETF ChaCha20 block (32-bit counter, 96-bit nonce) is the original block with the first nonce word in the counter's high half, so ChaCha20.block serves both.

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

def Cryptlib.Primitives.Cipher.ChaChaPoly.block (key : Key) (n : Nonce) (counter : UInt32) : Array UInt8

RFC 8439 §2.3: one 64-byte block at a 32-bit counter.

Equations

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

def Cryptlib.Primitives.Cipher.ChaChaPoly.chacha20 (key : Key) (n : Nonce) (d : ByteArray) : ByteArray

RFC 8439 §2.4: encryption starts at counter 1, block 0 being reserved for the Poly1305 key.

Equations

• Cryptlib.Primitives.Cipher.ChaChaPoly.chacha20 key n d = Cryptlib.Primitives.Cipher.ChaChaPoly.xorKeystream✝ (Cryptlib.Primitives.Cipher.ChaChaPoly.keystream✝ key n d.size) d

def Cryptlib.Primitives.Cipher.ChaChaPoly.poly1305 (otk : Vector UInt8 32) (msg : ByteArray) : Vector UInt8 16

RFC 8439 §2.5. Field arithmetic over Nat modulo 2^130 - 5.

Equations

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

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

RFC 8439 §2.8: Poly1305 keyed from block 0, over pad(ad) ‖ pad(ct) ‖ LE64 |ad| ‖ LE64 |ct|.

Equations

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

def Cryptlib.Primitives.Cipher.ChaChaPoly.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.ChaChaPoly.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.ChaChaPoly.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.ChaChaPoly.Scheme : AEAD.AEAD

Equations

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