Merge pull request #158 from GaloisInc/139-keccakp

SHA3: Add Keccak-p function

Primitive/Keyless/Hash/keccak.cry → Primitive/Keyless/Hash/Keccak.cry

@@ -1,8 +1,6 @@
 /**
  * Specification of the Keccak (SHA-3) hash function.
  *
- *
- *
  * [FIPS-202]: National Institute of Standards and Technology. SHA-3 Standard:
  *     Permutation-Based Hash and Extendable-Output Functions. (Department of
  *     Commerce, Washington, D.C.), Federal Information Processing Standards
@@ -14,7 +12,7 @@
  * @author Marcella Hastings <marcella@galois.com>
  *
  */
-module Primitive::Keyless::Hash::keccak where
+module Primitive::Keyless::Hash::Keccak where
 
 parameter
     /**
@@ -31,23 +29,12 @@ parameter
     type constraint (fin b, b % 25 == 0, b <= 1600, (2 ^^ (lg2 (b / 25))) * 25 == b)
 
     /**
-     * Rounds: the number of iterations of an internal transformation.
+     * Rounds: the number of iterations of an internal transformation (any
+     * positive integer).
      * [FIPS-202] Section 3 (intro).
-     *
-     * Note: this is currently specialized to a fixed value relative to `b`.
-     * This limitation matches the `Keccak-f` requirement, but is not
-     * necessary for the more generic `Keccak-p`permutation.
-     * For the standardized SHA3 parameter sets, only `Keccak-f` is required.
-     * [FIPS-202] Section 3.4.
-     *
-     * @design Marcella Hastings <marcella@galois.com>. I intend to refactor
-     * this and the RC functions to allow the fully generic `Keccak-p`
-     * implementation; right now it's restricted to this specific function of
-     * `b`, as is required by `Keccak-f`; this is enough to support the
-     * standardized SHA3 functions but not the fully generic specification.
      */
     type nr : #
-    type constraint (fin nr, nr > 0, nr == 12 + 2 * (lg2 ( b / 25)))
+    type constraint (fin nr, nr > 0)
 
     /**
      * Capacity parameter for the sponge construction.
@@ -78,12 +65,12 @@ Keccak M = digest where
     // Step 5.
     S = zero : [b]
     // Step 6. We create a list `Ss` instead of overwriting the variable `S`.
-    Ss = [S] # [Keccak_f (S' ^ (Pi # (zero : [c]))) | Pi <- Ps | S' <- Ss]
+    Ss = [S] # [Keccak_p (S' ^ (Pi # (zero : [c]))) | Pi <- Ps | S' <- Ss]
     // Steps 7 - 10. This step is sometimes known as "squeeze".
     // The truncation in Step 8 is handled here with `take`{r}`
     // The truncation in Step 9 is below with `take`{front=d, back=inf}`.
     extend : [b] -> [inf]
-    extend Z = (take`{r} Z) # extend (Keccak_f Z)
+    extend Z = (take`{r} Z) # extend (Keccak_p Z)
     digest = take`{front=d, back=inf} (extend (Ss ! 0))
 
 private
@@ -295,7 +282,7 @@ private
      *
      * [FIPS-202] Section 3.2.5, Algorithm 5.
      */
-    rc : [8] -> Bit
+    rc : Integer -> Bit
     rc t = if (t % 255) == 0 then 1 // Step 1.
          else Rs @ (t % 255) @0 // Step 4.
          where
@@ -326,8 +313,8 @@ private
      *
      * Equivalent to [FIPS-202] Section 3.2.5, Algorithm 5.
      */
-    rc_hardcoded : [8] -> Bit
-    rc_hardcoded t = constants @ t where
+    rc_hardcoded : Integer -> Bit
+    rc_hardcoded t = constants @ (t % 255) where
         constants = join [
             0x80b1e87f90a7d57062b32fde6ee54a25,
             0xa339e361175edf0d35b504ec9303a471
@@ -348,7 +335,7 @@ private
      * `(0, 0)` according to the round index.
      * [FIPS-202] Section 3.2.5, Algorithm 6.
      */
-    ι : State -> [8] -> State
+    ι : State -> Integer -> State
     ι A ir = A'' where
         // Step 1.
         A' = A
@@ -357,7 +344,7 @@ private
         // Step 3. 0 is the identity for XOR, so we iteratively set the
         // `2^j-1`th element by XORing the previously-set bits of RC with the
         // correct value at the desired index.
-        RCs = [RC0] # [RC' ^ (zext`{w} [rc_hardcoded (j + 7 * ir)] << (2^^j - 1))
+        RCs = [RC0] # [RC' ^ (zext`{w} [rc_hardcoded (toInteger j + 7 * ir)] << (2^^j - 1))
             | RC' <- RCs
             | j <- [0..ell] ]
         RC = (RCs ! 0) : [w]
@@ -387,30 +374,37 @@ private
     pad : {x, m} (fin x, fin m, x >= 1) => [x * ((m + 2) /^ x) - m]
     pad = [1] # zero # [1]
 
+    /**
+     * The Keccak-p[b, nr] permutation.
+     * [FIPS-202] Section 3.3, Algorithm 7.
+     */
+    Keccak_p : [b] -> [b]
+    Keccak_p S = S' where
+        // The round transformation is defined in [FIPS-202] Section 3.3.
+        Rnd A ir = ι (χ (π (ρ_hardcoded (θ A)))) ir
+
+        // Step 1.
+        A0 = unflatten_noindex S
+        // Step 2.
+        // The round index `ir` is allowed to be negative, but Cryptol types
+        // must be non-negative. Thus we iterate over the number of rounds and
+        // compute the round index as a value, rather than a type.
+        As = [A0] # [ Rnd A ir where
+                ir = 12 + 2 * `ell - r
+            | A <- As
+            | r <- [nr, nr - 1 .. 1]]
+        // Step 3.
+        S' = flatten_noindex (As ! 0)
+
     /**
      * Keccak-f family of permutations.
      *
-     * This is implemented as defined in Section 3.4, but while `Keccak-p` isn't
-     * explicitly implemented, we "expanded" the `Keccak-p` implementation
-     * according to the parameters given in the definition of `Keccak-f`.
-     * Specifically, note the range of `ir`.
-     *
-     * The number of rounds is a parameter to this functor and not passed
-     * explicitly here.
-     *
+     * This specializes `Keccak-p` to the case where `nr = 12 + 2*ell`; we
+     * enforce this in the type constraint on this function.
      * [FIPS-202] Section 3.4.
      */
-    Keccak_f : [b] -> [b]
-    Keccak_f S = S'
-        where
-            // The round transformation is defined in [FIPS-202] Section 3.3.
-            Rnd A ir = ι (χ (π (ρ_hardcoded (θ A)))) ir
-            // Step 1.
-            A0 = unflatten_noindex S
-            // Step 2.
-            rounds = [A0] # [ Rnd A ir | A <- rounds | ir <- [0..nr - 1]]
-            // Step 3.
-            S' = flatten_noindex (rounds ! 0)
+    Keccak_f : (nr == 12 + 2 * ell) => [b] -> [b]
+    Keccak_f = Keccak_p
 
 /**
  * See https://keccak.team/files/Keccak-reference-3.0.pdf, Section 1.2

Primitive/Keyless/Hash/SHA3/SHA3.cry

@@ -13,7 +13,7 @@
  */
 module Primitive::Keyless::Hash::SHA3::SHA3 where
 import Primitive::Keyless::Hash::KeccakBitOrdering as KBO
-import Primitive::Keyless::Hash::keccak where
+import Primitive::Keyless::Hash::Keccak where
     type b = 1600
     type nr = 24
     type c = 2 * digest
@@ -27,7 +27,7 @@ parameter
  * [FIPS-202] Section 6.1.
  *
  * Note that the specification of `c` is above, in the instantiation of the
- * `keccak` module.
+ * `Keccak` module.
  *
  * This expects input and produces output in the bit ordering used by the
  * `Keccak` spec, where bytes are in MSB order and the bits in each byte are

Primitive/Keyless/Hash/SHAKE/SHAKE128.cry

@@ -14,7 +14,7 @@
  *
  */
 module Primitive::Keyless::Hash::SHAKE::SHAKE128 where
-import Primitive::Keyless::Hash::keccak where
+import Primitive::Keyless::Hash::Keccak where
     type b = 1600
     type nr = 24
     // The capacity is double the security level, so this provides a security

Primitive/Keyless/Hash/SHAKE/SHAKE256.cry

@@ -14,7 +14,7 @@
  *
  */
 module Primitive::Keyless::Hash::SHAKE::SHAKE256 where
-import Primitive::Keyless::Hash::keccak where
+import Primitive::Keyless::Hash::Keccak where
     type b = 1600
     type nr = 24
     // The capacity is double the security level, so this provides a security