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