Data.SBV.Examples.Crypto.AES

Formalizing GF(2^8)

type GF28

gf28Mult

gf28Pow

gf28Inverse

Implementing AES

Types and basic operations

type State

type Key

type KS

toBytes

fromBytes

rotR

The key schedule

roundConstants

invMixColumns

keyExpansion

The S-box transformation

sboxTable

sbox

The inverse S-box transformation

unSBoxTable

unSBox

sboxInverseCorrect

AddRoundKey transformation

addRoundKey

Tables for T-Box encryption

t0Func

t0

t1

t2

t3

Tables for T-Box decryption

u0Func

u0

u1

u2

u3

AES rounds

doRounds

aesRound

aesInvRound

AES API

aesKeySchedule

aesEncrypt

aesDecrypt

Test vectors

128-bit enc/dec test

t128Enc

t128Dec

192-bit enc/dec test

t192Enc

t192Dec

256-bit enc/dec test

t256Enc

t256Dec

Verification

aes128IsCorrect

Code generation

cgAES128BlockEncrypt

C-library generation

aes128LibComponents

cgAES128Library

hex8