README
1A purely functional implementation and proof of correctness of the AES
2(also known as "Rijndael") algorithm from Rijmen and Daemen. The AES
3homepage is
4
5 http://csrc.nist.gov/encryption/aes/
6
7Unlike most implementations, no arrays or vectors are used in our
8code. The main datastructure operated on is the `state', which is a 4x4
9block of bytes (8 bit words). We model it by a 16-tuple of bytes.
10
11The dependencies are:
12
13 word8Theory (definition of bytes and operations)
14 |
15 |
16 tablesTheory (definition of Sboxes and specialized Sboxes)
17 |
18 |
19 MultTheory (definition of GF_256 multiplication:
20 | recursive, iterative, and tabled versions)
21 |
22 RoundOpTheory (basic operations that happen during a round)
23 |
24 |
25 aesTheory (defn of rounds, key schedule, AES, correctness)
26
27
28This directory is a modification of that found at <holdir>/examples/Rijndael,
29eventually intended to serve as an application of the H/W synthesis package.
30
31Major Changes:
32
33* Integrated Scott Owens' tabled multiplication. Speeds things up
34 dramatically: on the basic example in aes.compute.example,
35 encoding then decoding a block now takes approx 15 seconds
36 and 500K inference steps, vs. the 64 seconds and 2.5M inference
37 steps. Also speeds up the build, especially the many lemmas
38 used to prove the invertibility of column multiplication in
39 RoundOpScript (on average, from 35 seconds to 9).
40
41* Changed the representation of bytes from 8-tuples to an application
42 of a single curried constructor (BYTE) to 8 arguments. This avoids
43 a representation problem with nested tuples (the types on each
44 occurrence of "," get compounded, causing exponential growth in size
45 of types of constants and therefore terms.
46
47 For example, aesTheory with tupled bytes was 24M when compiled, but
48 is now 4M (still a lot).
49
50 Could do the same for blocks and keyschedules, but the current version is
51 a big improvement and localizes the change to word8Theory and
52 tablesTheory.
53