ChaCha20 (original/Bernstein construction, 64-bit nonce)

Single-block function; ChaChaPoly builds the RFC 8439 variant on top of it.

def Cryptlib.Primitives.Cipher.ChaCha20.block (key nonce : Array UInt8) (counterLo counterHi : UInt32) : Array UInt8

One 64-byte ChaCha20 block: 32-byte key, 8-byte nonce, 64-bit counter (as two 32-bit little-endian words).

Equations

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

def Cryptlib.Primitives.Cipher.ChaCha20.keystream32 (key : Array UInt8) : Array UInt8

The first 32 bytes of the ChaCha20 keystream for key, with zero nonce and counter.

Equations

• Cryptlib.Primitives.Cipher.ChaCha20.keystream32 key = (Cryptlib.Primitives.Cipher.ChaCha20.block key (Array.replicate 8 0) 0 0).extract 0 32