AES-256

Encryption direction only. The S-box is computed from its FIPS-197 definition rather than transcribed. Not constant time.

def Cryptlib.Primitives.Cipher.AES.mul (a b : UInt8) : UInt8

Multiplication in GF(2^8) modulo AES's x^8 + x^4 + x^3 + x + 1.

Equations

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

def Cryptlib.Primitives.Cipher.AES.inv (a : UInt8) : UInt8

The multiplicative inverse in GF(2^8), computed as a^254; inv 0 = 0.

Equations

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

def Cryptlib.Primitives.Cipher.AES.sboxByte (a : UInt8) : UInt8

FIPS-197 §5.1.1: invert in GF(2^8), then apply the affine transformation over GF(2).

Equations

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

def Cryptlib.Primitives.Cipher.AES.sbox : Array UInt8

sboxByte tabulated over all 256 inputs.

Equations

• Cryptlib.Primitives.Cipher.AES.sbox = Array.map (fun (i : Nat) => Cryptlib.Primitives.Cipher.AES.sboxByte (UInt8.ofNat i)) (Array.range 256)

def Cryptlib.Primitives.Cipher.AES.expandKey (key : Vector UInt8 32) : Array UInt8

The AES-256 key schedule: sixty 4-byte words, fifteen round keys.

Equations

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

def Cryptlib.Primitives.Cipher.AES.subBytes (s : Array UInt8) : Array UInt8

Equations

• Cryptlib.Primitives.Cipher.AES.subBytes s = Array.map (fun (b : UInt8) => Cryptlib.Primitives.Cipher.AES.sbox[b.toNat]!) s

def Cryptlib.Primitives.Cipher.AES.shiftRows (s : Array UInt8) : Array UInt8

Byte i of the state is row i % 4, column i / 4; row r rotates left by r columns.

Equations

• Cryptlib.Primitives.Cipher.AES.shiftRows s = Array.ofFn fun (i : Fin 16) => s[(↑i + 4 * (↑i % 4)) % 16]!

def Cryptlib.Primitives.Cipher.AES.mixColumns (s : Array UInt8) : Array UInt8

Each column multiplied by the fixed polynomial {03}x³ + {01}x² + {01}x + {02}.

Equations

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

def Cryptlib.Primitives.Cipher.AES.encryptBlock (rk : Array UInt8) (input : Vector UInt8 16) : Vector UInt8 16

AES-256 on one block, against an expanded key schedule.

Equations

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

def Cryptlib.Primitives.Cipher.AES.encryptBlockWithKey (key : Vector UInt8 32) (input : Vector UInt8 16) : Vector UInt8 16

Expand the key and encrypt one block.

Equations

• Cryptlib.Primitives.Cipher.AES.encryptBlockWithKey key input = Cryptlib.Primitives.Cipher.AES.encryptBlock (Cryptlib.Primitives.Cipher.AES.expandKey key) input