An element of the Galois Field 2^8, which are essentially polynomials with maximum degree 7. They are conveniently represented as values between 0 and 255.

Multiplication in GF(2^8). This is simple polynomial multiplication, followed by the irreducible polynomial x^8+x^4+x^3+x^1+1. We simply use the pMult function exported by SBV to do the operation.

Exponentiation by a constant in GF(2^8). The implementation uses the usual square-and-multiply trick to speed up the computation.

Computing inverses in GF(2^8). By the mathematical properties of GF(2^8) and the particular irreducible polynomial used x^8+x^5+x^3+x^1+1, it turns out that raising to the 254 power gives us the multiplicative inverse. Of course, we can prove this using SBV:

>>> prove $ \x -> x ./= 0 .=> x `gf28Mult` gf28Inverse x .== 1
Q.E.D.

Note that we exclude 0 in our theorem, as it does not have a multiplicative inverse.

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.

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

The key schedule. AES executes in rounds, and it treats first and last round keys slightly differently than the middle ones. We reflect that choice by being explicit about it in our type. The length of the middle list of keys depends on the key-size, which in turn determines the number of rounds.

Rotating a state row by a fixed amount to the right.

Definition of round-constants, as specified in Section 5.2 of the AES standard.

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.

Key expansion. Starting with the given key, returns an infinite sequence of words, as described by the AES standard, Section 5.2, Figure 11.

The values of the AES S-box table. Note that we describe the S-box programmatically using the mathematical construction given in Section 5.1.1 of the standard. However, the code-generation will turn this into a mere look-up table, as it is just a constant table, all computation being done at "compile-time".

The sbox transformation. We simply select from the sbox table. Note that we are obliged to give a default value (here 0) to be used if the index is out-of-bounds as required by SBV's select function. However, that will never happen since the table has all 256 elements in it.

The values of the inverse S-box table. Again, the construction is programmatic.

The inverse s-box transformation.

Prove that the sbox and unSBox are inverses. We have:

>>> prove sboxInverseCorrect
Q.E.D.

Adding the round-key to the current state. We simply exploit the fact that addition is just xor in implementing this transformation.

T-box table generation function for encryption

First look-up table used in encryption

Second look-up table used in encryption

Third look-up table used in encryption

Fourth look-up table used in encryption

T-box table generating function for decryption

First look-up table used in decryption

Second look-up table used in decryption

Third look-up table used in decryption

Fourth look-up table used in decryption

Generic round function. Given the function to perform one round, a key-schedule, and a starting state, it performs the AES rounds.

One encryption round. The first argument indicates whether this is the final round or not, in which case the construction is slightly different.

One decryption round. Similar to the encryption round, the first argument indicates whether this is the final round or not.

Key schedule. Given a 128, 192, or 256 bit key, expand it to get key-schedules for encryption and decryption. The key is given as a sequence of 32-bit words. (4 elements for 128-bits, 6 for 192, and 8 for 256.) Compare this function to aesInvKeySchedule which can calculate the key-expansion for decryption on the fly, as opposed to calculating the forward key-expansion first.

Block encryption. The first argument is the plain-text, which must have precisely 4 elements, for a total of 128-bits of input. The second argument is the key-schedule to be used, obtained by a call to aesKeySchedule. The output will always have 4 32-bit words, which is the cipher-text.

Block decryption. The arguments are the same as in aesEncrypt, except the first argument is the cipher-text and the output is the corresponding plain-text.

Inverse key expansion. Starting from the final round key, unwinds key generation operation to construct keys for the previous rounds. Used in on-the-fly decryption.

AES inverse key schedule. Starting from the last-round key, construct the sequence of keys that can be used for doing on-the-fly decryption. Compare this function to aesKeySchedule which returns both encryption and decryption schedules: In this case, we don't calculate the encryption sequence, hence we can fuse this function with the decryption operation.

Block decryption, starting from the unwound key. That is, start from the final key. Also; we don't use the T-box implementation. Just pure AES inverse cipher.

Common plain text for test vectors

Key for 128-bit encryption test

Key for 192-bit encryption test

Key for 256-bit encryption test

Expected cipher-text for 128-bit encryption

Expected cipher-text for 192-bit encryption

Expected cipher-text for 256-bit encryption

Calculate the 128-bit final-round key from on-the-fly decryption key schedule

Calculate the 192-bit final-round key from on-the-fly decryption key schedule

Calculate the 192-bit final-round key from on-the-fly decryption key schedule. Compare this to aes192InvKey: Typically we just need the final 6-blocks, but it is advantageous to have the entire last 8-blocks even for 192-bit keys. That is, e store the final 256-bits of key-expansion for speed purposes for both 192 and 256 bit versions. (But only the final 128 bits for the 128-bit version.)

Calculate the 256-bit final-round key from on-the-fly decryption key schedule

Extract the final key for on-the-fly decryption. This will extract exactly the number of blocks we need.

Extract the extended key for on-the-fly decryption. This will extract 4-blocks for 128-bit decryption, but 256 bit for both 192 and 256-bit variants

128-bit encryption test, from Appendix C.1 of the AES standard:

>>> map hex8 t128Enc
["69c4e0d8","6a7b0430","d8cdb780","70b4c55a"]

128-bit decryption test, from Appendix C.1 of the AES standard:

>>> map hex8 t128Dec
["00112233","44556677","8899aabb","ccddeeff"]

192-bit encryption test, from Appendix C.2 of the AES standard:

>>> map hex8 t192Enc
["dda97ca4","864cdfe0","6eaf70a0","ec0d7191"]

192-bit decryption test, from Appendix C.2 of the AES standard:

>>> map hex8 t192Dec
["00112233","44556677","8899aabb","ccddeeff"]

256-bit encryption, from Appendix C.3 of the AES standard:

>>> map hex8 t256Enc
["8ea2b7ca","516745bf","eafc4990","4b496089"]

256-bit decryption, from Appendix C.3 of the AES standard:

>>> map hex8 t256Dec
["00112233","44556677","8899aabb","ccddeeff"]

Various tests for round-trip properties. We have:

>>> runAESTests False
GOOD: Key generation AES128
GOOD: Key generation AES192
GOOD: Key generation AES256
GOOD: Encryption     AES128
GOOD: Decryption     AES128
GOOD: Decryption-OTF AES128
GOOD: Encryption     AES192
GOOD: Decryption     AES192
GOOD: Decryption-OTF AES192
GOOD: Encryption     AES256
GOOD: Decryption     AES256
GOOD: Decryption-OTF AES256

Correctness theorem for 128-bit AES. Ideally, we would run:

  prove aes128IsCorrect

to get a proof automatically. Unfortunately, while SBV will successfully generate the proof obligation for this theorem and ship it to the SMT solver, it would be naive to expect the SMT-solver to finish that proof in any reasonable time with the currently available SMT solving technologies. Instead, we can issue:

  quickCheck aes128IsCorrect

and get some degree of confidence in our code. Similar predicates can be easily constructed for 192, and 256 bit cases as well.

128-bit encryption, that takes 128-bit values, instead of chunks. We have:

>>> hex8 $ aes128Enc 0x000102030405060708090a0b0c0d0e0f 0x00112233445566778899aabbccddeeff
"69c4e0d86a7b0430d8cdb78070b4c55a"

You can also render this function as a stand-alone function using:

  sbv2smt (smtFunction "aes128Enc" aes128Enc)

Code generation for 128-bit AES encryption.

The following sample from the generated code-lines show how T-Boxes are rendered as C arrays:

  static const SWord32 table1[] = {
      0xc66363a5UL, 0xf87c7c84UL, 0xee777799UL, 0xf67b7b8dUL,
      0xfff2f20dUL, 0xd66b6bbdUL, 0xde6f6fb1UL, 0x91c5c554UL,
      0x60303050UL, 0x02010103UL, 0xce6767a9UL, 0x562b2b7dUL,
      0xe7fefe19UL, 0xb5d7d762UL, 0x4dababe6UL, 0xec76769aUL,
      ...
      }

The generated program has 5 tables (one sbox table, and 4-Tboxes), all converted to fast C arrays. Here is a sample of the generated straightline C-code:

  const SWord8  s1915 = (SWord8) s1912;
  const SWord8  s1916 = table0[s1915];
  const SWord16 s1917 = (((SWord16) s1914) << 8) | ((SWord16) s1916);
  const SWord32 s1918 = (((SWord32) s1911) << 16) | ((SWord32) s1917);
  const SWord32 s1919 = s1844 ^ s1918;
  const SWord32 s1920 = s1903 ^ s1919;

The GNU C-compiler does a fine job of optimizing this straightline code to generate a fairly efficient C implementation.

Components of the AES implementation that the library is generated from. For each case, we provide the driver values from the AES test-vectors.

Generate code for AES functionality; given the key size.

Generate a C library, containing functions for performing 128-bit encdeckey-expansion. A note on performance: In a very rough speed test, the generated code was able to do 6.3 million block encryptions per second on a decent MacBook Pro. On the same machine, OpenSSL reports 8.2 million block encryptions per second. So, the generated code is about 25% slower as compared to the highly optimized OpenSSL implementation. (Note that the speed test was done somewhat simplistically, so these numbers should be considered very rough estimates.)

For doctest purposes only

Chunk in groups of 4. (This function must be in some standard library, where?)