aes: expand docs and properties #77

Common/GF28.cry

@@ -76,11 +76,16 @@ matrixMult xss yss = [ vectorMult xs yss' | xs <- xss ]
  * This proves quickly!
  */
 property inverseDefined x =
-  if x == 0 then True
+  if x == 0 then inverse x == 0
   else mult x (inverse x) == 1
 
 /**
  * Compute the inverse of a value. [FIPS-197u1 Section 4.4, Algorithm 4.11
+ *
+ * Mathematically speaking, the inverse isnt' defined for `x = 0`, but
+ * we take the same liberties as the reference and use a method that
+ * returns 0 for the inverse of 0. This is useful for computing Algorithm
+ * 5.2 later.
  */
 inverse : GF28 -> GF28
 inverse x = pow x 254

Primitive/Symmetric/Cipher/Block/AES/Round.cry

@@ -4,16 +4,31 @@ import Common::GF28 as GF28
 import Primitive::Symmetric::Cipher::Block::AES::State
 import Primitive::Symmetric::Cipher::Block::AES::SubByteSBox
 
-/** One round of AES */
+/**
+ * One round of AES.
+ * [FIPS-197u1] Section 5.3, Algorithm 1, Lines 5-8.
+ */
 AESRound : RoundKey -> State -> State
 AESRound rk s = rk ^ MixColumns (ShiftRows (SubBytes s))
 
+/**
+ * SubBytes applies an invertible, non-linear transformation to the state.
+ * [FIPS-197u1] Section 5.1.1.
+ */
 SubBytes : State -> State
 SubBytes state = [ [ SubByte b | b <- row ] | row <- state ]
 
+/**
+ * ShiftRows transforms the state by cycling the last three rows.
+ * [FIPS-197u1] Section 5.1.2.
+ */
 ShiftRows : State -> State
 ShiftRows state = [ row <<< i | row <- state | i : [2] <- [0 .. 3] ]
 
+/**
+ * MixColumns multiplies the state columns by a fixed matrix.
+ * [FIPS-197u1] Section 5.1.3.
+ */
 MixColumns : State -> State
 MixColumns state = GF28::matrixMult m state
     where m = [ [2,3,1,1] >>> i | i <- [0 .. 3] ]
@@ -22,24 +37,49 @@ MixColumns state = GF28::matrixMult m state
 AESFinalRound : RoundKey -> State -> State
 AESFinalRound rk s = rk ^ ShiftRows (SubBytes s)
 
-
-
-/** One inverse round of AES */
+/**
+ * One inverse round of AES.
+ * [FIPS-197u1] Section 5.3, Algorithm 3, Lines 5-8.
+ */
 AESInvRound : RoundKey -> State -> State
 AESInvRound rk s = InvMixColumns (rk ^ InvSubBytes (InvShiftRows s))
 
-InvSubBytes : State -> State
-InvSubBytes state = [ [ InvSubByte b | b <- row ] | row <- state ]
-
+/**
+ * Inverts the `ShiftRows` function.
+ * [FIPS-197u1] Section 5.3.1.
+ */
 InvShiftRows : State -> State
 InvShiftRows state = [ row >>> shiftAmount | row <- state
                                            | shiftAmount : [2] <- [0 .. 3]
                      ]
 
+/**
+ * Inverts the `MixColumns` function.
+ * [FIPS-197u1] Section 5.3.3.
+ */
+InvSubBytes : State -> State
+InvSubBytes state = [ [ InvSubByte b | b <- row ] | row <- state ]
+
+/**
+ * Inverts the `SubBytes` function.
+ * [FIPS-197u1] Section 5.3.2
+ */
 InvMixColumns : State -> State
 InvMixColumns state = GF28::matrixMult m state
     where m = [[0x0e, 0x0b, 0x0d, 0x09] >>> i | i <- [0 .. 3] ]
 
 /** The final inverted AES round */
 AESFinalInvRound : RoundKey -> State -> State
 AESFinalInvRound rk s = rk ^ InvSubBytes (InvShiftRows s)
+
+// This proves.
+subBytesInverts : State -> Bool
+property subBytesInverts s = InvSubBytes (SubBytes s) == s
+
+// This proves.
+shiftRowsInverts : State -> Bool
+property shiftRowsInverts s = InvShiftRows (ShiftRows s) == s
+
+// This checks (non-exhaustively).
+mixColumnsInverts : State -> Bool
+property mixColumnsInverts s = InvMixColumns (MixColumns s) == s