Cryptol.AES

A TBox-based implementation of AES primitives, based on the AES example code from SBV. Here we've stripped out everything except the basic primitives needed, which essentially boil down to table table lookups in most cases.

Documentation

type State = [Word32]

AES state. The state consists of four 32-bit words, each of which is in turn treated as four GF28's, i.e., 4 bytes. The T-Box implementation keeps the four-bytes together for efficient representation.

type Key = [Word32]

The key, which can be 128, 192, or 256 bits. Represented as a sequence of 32-bit words.

keyExpansionWords :: Integer -> Key -> [Word32]

invMixColumns :: State -> State

The InvMixColumns transformation, as described in Section 5.3.3 of the standard. Note that this transformation is only used explicitly during key-expansion in the T-Box implementation of AES.

aesRound :: State -> State

aesFinalRound :: State -> State

aesInvRound :: State -> State

aesInvFinalRound :: State -> State