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 the state by a 16-tuple of bytes.
10
11The dependencies are:
12
13 tablesTheory (definition of Sboxes)
14 |
15 |
16 MultTheory (definition of GF_256 multiplication:
17 | recursive, iterative, and tabled versions)
18 |
19 RoundOpTheory (basic operations that happen during a round)
20 |
21 |
22 aesTheory (defn of rounds, key schedule, AES, correctness)
23
24
25This directory is a modification of that found at <holdir>/examples/Rijndael,
26and is eventually intended to serve as an application of the H/W synthesis
27package.
28
29Major Changes:
30
31* Integrated Scott Owens' tabled multiplication. Speeds things up
32 dramatically: on the basic example in aes.compute.example,
33 encoding then decoding a block now takes approx 15 seconds
34 and 500K inference steps, vs. the 64 seconds and 2.5M inference
35 steps. Also speeds up the build, especially the many lemmas
36 used to prove the invertibility of column multiplication in
37 RoundOpScript (on average, from 35 seconds to 9).
38
39* The representation of bytes is as an abstract type "word8",
40 generated by Anthony Fox's word library.
41
42* New definition principles, allowing total functions over
43 bytes to be given by pattern-matching over byte literals,
44 has been implemented by Scott Owens.
45
46