Merge pull request #117 from GaloisInc/112-sha2

Add SHA2 actual hashing

Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry

@@ -1,14 +1,23 @@
 /**
- * Secure hash algorithm SHA256.
+ * Instantiation of the secure hash algorithm SHA-256 as specified in
+ * [FIPS-180-4], Section 5.3.3.
  *
  * @copyright Galois, Inc
  * @author Marcella Hastings <marcella@galois.com>
+ *
+ * [FIPS-180-4]: National Institute of Standards and Technology. Secure Hash
+ *     Standard (SHS). (Department of Commerce, Washington, D.C.), Federal
+ *     Information Processing Standards Publication (FIPS) NIST FIPS 180-4.
+ *     August 2015.
+ *     @see https://doi.org/10.6028/NIST.FIPS.180-4
  */
-module Primitive::Keyless::Hash::SHA2::Instantiations::SHA =
+module Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 =
     Primitive::Keyless::Hash::SHA2::Specification
 where
     type w = 32
 
+    type DigestSize = 256
+
     // Per [FIPS-180-4], these are the first 32 bits of the fractional
     // parts of the square roots of the first 8 prime numbers.
     H0 = [

Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry

@@ -1,14 +1,23 @@
 /**
- * Secure hash algorithm SHA384.
+ * Instantiation of the secure hash algorithm SHA-384 as specified in
+ * [FIPS-180-4], Section 5.3.4.
  *
  * @copyright Galois, Inc
  * @author Marcella Hastings <marcella@galois.com>
+ *
+ * [FIPS-180-4]: National Institute of Standards and Technology. Secure Hash
+ *     Standard (SHS). (Department of Commerce, Washington, D.C.), Federal
+ *     Information Processing Standards Publication (FIPS) NIST FIPS 180-4.
+ *     August 2015.
+ *     @see https://doi.org/10.6028/NIST.FIPS.180-4
  */
 module Primitive::Keyless::Hash::SHA2::Instantiations::SHA384 =
     Primitive::Keyless::Hash::SHA2::Specification
 where
     type w = 64
 
+    type DigestSize = 384
+
     // Per [FIPS-180-4], these are the the first sixty-four bits of the
     // fractional parts of the square roots of the 9th - 16th prime numbers.
     H0 = [

Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry

@@ -1,14 +1,23 @@
 /**
- * Secure hash algorithm SHA512.
+ * Instantiation of the secure hash algorithm SHA-512 as specified in
+ * [FIPS-180-4], Section 5.3.5.
  *
  * @copyright Galois, Inc
  * @author Marcella Hastings <marcella@galois.com>
+ *
+ * [FIPS-180-4]: National Institute of Standards and Technology. Secure Hash
+ *     Standard (SHS). (Department of Commerce, Washington, D.C.), Federal
+ *     Information Processing Standards Publication (FIPS) NIST FIPS 180-4.
+ *     August 2015.
+ *     @see https://doi.org/10.6028/NIST.FIPS.180-4
  */
 module Primitive::Keyless::Hash::SHA2::Instantiations::SHA512 =
     Primitive::Keyless::Hash::SHA2::Specification
 where
     type w = 64
 
+    type DigestSize = 512
+
     // Per [FIPS-180-4], these are the the first sixty-four bits of the
     // fractional parts of the square roots of the first 8 prime numbers.
     H0 = [

Primitive/Keyless/Hash/SHA2/Specification.cry

@@ -24,13 +24,25 @@ module Primitive::Keyless::Hash::SHA2::Specification where
 
 parameter
     /**
-     * Word size.
-     * The specification defines words to be either 32 or 64 bits.
+     * Length of words, in bits, that are used during hashing.
+     *
+     * The specification defines words to be either 32 bits (for
+     * SHA-224 and SHA-256) or 64 bits (for SHA-384, SHA-512, and
+     * SHA-512/t for any valid `t`).
      * [FIPS-180-4] Section 1, Figure 1.
      */
     type w : #
     type constraint (w % 32 == 0, 32 <= w, 64 >= w)
 
+    /**
+     * Length of the message digest produced by the hash algorithm.
+     *
+     * Allowable values for each word size `w` are defined in [FIPS-180-4]
+     * Section 1, Figure 1.
+     */
+    type DigestSize : #
+    type constraint (8 * w >= DigestSize)
+
     /**
      * Initial hash value.
      * These are defined in [FIPS-180-4] Section 5.3.
@@ -46,11 +58,25 @@ type constraint ValidMessageLength L = width L < MaxMessageWidth
 
 private
     /**
-     * Size of blocks of data used in hashing; denoted `m` in the spec.
-     * [FIPS-180-4] Section 1, Figure 1.
+     * Size of blocks of data used in hashing, measured in bits.
+     *
+     * This is denoted `m` in the spec. [FIPS-180-4] Section 1, Figure 1.
      */
     type BlockSize = 16 * w
 
+    /**
+     * `ScheduleLength` is fixed based on `w`: 64 when `w = 32` and 80 when `w = 64`.
+     * We encode this using the relation `48 + w/2`.
+     *
+     * It is not explicitly defined with this name in the spec. You can see it used
+     * in several places:
+     * - The constant `K` has `ScheduleLength` words ([FIPS-180-4] Section
+     *   4.2.2 and 4.2.3)
+     * - The message schedule `W` has length `ScheduleLength` ([FIPS-180-4]
+     *   Section 6.2.2 #1 and Section 6.4.2 #1)
+     */
+    type ScheduleLength = 48 + w / 2
+
     /**
      * Circular rotate left operation.
      * [FIPS-180-4] Section 2.2.2 and Section 3.2 #5.
@@ -174,14 +200,11 @@ private
     /**
      * The SHA family uses a sequence of constant `w`-bit words, which represent
      * the first `w` bits of the fractional parts of the cube roots of the first
-     * `n` prime numbers.
-     *
-     * `n` is fixed based on `w`: 64 when `w = 32` and 80 when `w = 64`. This is
-     * encoded into the type of `K` using the relation `48 + w/2`.
+     * `ScheduleLength` prime numbers.
      *
      * [FIPS-180-4] Section 4.2.2 and 4.2.3.
      */
-    K : [48 + w / 2][w]
+    K : [ScheduleLength][w]
     K | w == 32 => [
         0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5,
         0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174,
@@ -256,3 +279,84 @@ private
      */
     parse : {N} () => [N * BlockSize] -> [N][BlockSize]
     parse M = split M
+
+
+/**
+ * Secure hash function.
+ *
+ * All the SHA functions (excluding SHA-1) share the same structure.
+ * The primary differences can be handled through Cryptol's built-in
+ * polymorphism:
+ * - The word sizes are different;
+ * - The length of the message schedule and subsequent number of iterations
+ *   over the working variables are different; and
+ * - The digest length is different.
+ *
+ * [FIPS-180-4] Section 6.2 - 6.7.
+ * The hash functionality itself is primarily described in Sections 6.2 and
+ * 6.4. The correct truncation for other bit lengths is in the other sections.
+ */
+hash: {l} (ValidMessageLength l) => [l] -> [DigestSize]
+hash M = take (join (digest ! 0)) where
+    digest = [H0] # [Hi'
+        where
+            // Step 1. Prepare the message schedule.
+            Ws = messageSchedule (split Mi)
+
+            // Step 2. Initialize the eight working variables with the
+            // previous hash value.
+            letters = [(Hi0, Hi1, Hi2, Hi3, Hi4, Hi5, Hi6, Hi7)] # [
+                // Step 3. Update temporary and working variables...
+                variableUpdate l Kt Wt
+                | l <- letters
+
+                // ...for t=0 to `ScheduleLength`.
+                | Wt <- Ws
+                | Kt <- K
+            ]
+            (a, b, c, d, e, f, g, h) = letters ! 0
+
+            // Step 4. Compute the next intermediate hash value.
+            // Note that in the spec, this is denoted H^(i).
+            Hi' = [a + Hi0, b + Hi1, c + Hi2, d + Hi3, e + Hi4, f + Hi5, g + Hi6, h + Hi7]
+
+        // Each message block is processed in order.
+        | Mi <- parse (pad M)
+
+        // An intermediate hash digest is computed at each iteration.
+        // Note that in the spec, these are denoted H^(i-1)_j for j = 0..7.
+        | [Hi0, Hi1, Hi2, Hi3, Hi4, Hi5, Hi6, Hi7] <- digest
+    ]
+
+    // Step 1. Prepare the message schedule.
+    messageSchedule : [16][w] -> [ScheduleLength][w]
+    messageSchedule Mi = take W where
+        W : [inf][w]
+        W = Mi # [ sigma1 w2 + w7 + sigma0 w15 + w16
+            // The spec indexes these by counting from the other direction.
+            // We can't do that here because it's an infinite sequence.
+            // Note that 15 - the drop parameter is the index in the spec.
+            | w16 <- W
+            | w15 <- drop`{1} W
+            | w7  <- drop`{9} W
+            | w2  <- drop`{14} W
+        ]
+
+    // Convenience type to describe the set of working variables a - h.
+    type LetterVars = ([w], [w], [w], [w], [w], [w], [w], [w])
+
+    // Step 3. Update temporary and working variables (one iteration).
+    variableUpdate : LetterVars -> [w] -> [w] -> LetterVars
+    variableUpdate (a, b, c, d, e, f, g, h) Kt Wt =
+        (a', b', c', d', e', f', g', h')
+        where
+            T1 = h + Sigma1 e + Ch e f g + Kt + Wt
+            T2 = Sigma0 a + Maj a b c
+            h' = g
+            g' = f
+            f' = e
+            e' = d + T1
+            d' = c
+            c' = b
+            b' = a
+            a' = T1 + T2

Primitive/Keyless/Hash/SHA2/Tests/SHA256.cry

@@ -0,0 +1,67 @@
+/**
+ * Test vectors for SHA256 as specified in [FIPS-180-4].
+ *
+ * These vectors were originally specified in [CSG-SHA], but we also used the
+ * convenient collected test vectors page from David Ireland.
+ * @see DI Management https://www.di-mgt.com.au/sha_testvectors.html
+ *
+ * @copyright Galois, Inc
+ * @author Marcella Hastings <marcella@galois.com>
+ *
+ * [CSG-SHA]: National Institute of Standards and Technology. Example
+ *     algorithms - Secure hashing.
+ *     @see http://csrc.nist.gov/groups/ST/toolkit/examples.html
+ *     @see https://csrc.nist.gov/csrc/media/projects/cryptographic-standards-and-guidelines/documents/examples/sha_all.pdf
+ * [FIPS-180-4]: National Institute of Standards and Technology. Secure Hash
+ *     Standard (SHS). (Department of Commerce, Washington, D.C.), Federal
+ *     Information Processing Standards Publication (FIPS) NIST FIPS 180-4.
+ *     August 2015.
+ *     @see https://doi.org/10.6028/NIST.FIPS.180-4
+ */
+import Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 as SHA256
+
+/**
+ * ```repl
+ * :prove abcWorks
+ * ```
+ */
+property abcWorks = SHA256::hash (join "abc") == output where
+    output = join [
+        0xba7816bf, 0x8f01cfea, 0x414140de, 0x5dae2223,
+        0xb00361a3, 0x96177a9c, 0xb410ff61, 0xf20015ad
+    ]
+
+/**
+ * ```repl
+ * :prove emptyStringWorks
+ * ```
+ */
+property emptyStringWorks = SHA256::hash [] == output where
+    output = join [
+        0xe3b0c442, 0x98fc1c14, 0x9afbf4c8, 0x996fb924,
+        0x27ae41e4, 0x649b934c, 0xa495991b, 0x7852b855
+    ]
+
+/**
+ * ```repl
+ * :prove alphabet448
+ * ```
+ */
+property alphabet448 = SHA256::hash input == output where
+    input = join "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
+    output = join [
+        0x248d6a61, 0xd20638b8, 0xe5c02693, 0x0c3e6039,
+        0xa33ce459, 0x64ff2167, 0xf6ecedd4, 0x19db06c1
+    ]
+
+/**
+ * ```repl
+ * :prove alphabet896
+ * ```
+ */
+property alphabet896 = SHA256::hash input == output where
+    input = join "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
+    output = join [
+        0xcf5b16a7, 0x78af8380, 0x036ce59e, 0x7b049237,
+        0x0b249b11, 0xe8f07a51, 0xafac4503, 0x7afee9d1
+    ]

Primitive/Keyless/Hash/SHA2/Tests/SHA384.cry

@@ -0,0 +1,68 @@
+/**
+ * Test vectors for SHA384 as specified in [FIPS-180-4].
+ *
+ * These vectors were originally specified in [CSG-SHA], but we also used the
+ * convenient collected test vectors page from David Ireland.
+ * @see DI Management https://www.di-mgt.com.au/sha_testvectors.html
+ *
+ * @copyright Galois, Inc
+ * @author Marcella Hastings <marcella@galois.com>
+ *
+ * [CSG-SHA]: National Institute of Standards and Technology. Example
+ *     algorithms - Secure hashing.
+ *     @see http://csrc.nist.gov/groups/ST/toolkit/examples.html
+ *     @see https://csrc.nist.gov/csrc/media/projects/cryptographic-standards-and-guidelines/documents/examples/sha_all.pdf
+ * [FIPS-180-4]: National Institute of Standards and Technology. Secure Hash
+ *     Standard (SHS). (Department of Commerce, Washington, D.C.), Federal
+ *     Information Processing Standards Publication (FIPS) NIST FIPS 180-4.
+ *     August 2015.
+ *     @see https://doi.org/10.6028/NIST.FIPS.180-4
+ */
+import Primitive::Keyless::Hash::SHA2::Instantiations::SHA384 as SHA384
+
+/**
+ * ```repl
+ * :prove abcWorks
+ * ```
+ */
+property abcWorks = SHA384::hash (join "abc") == output where
+    output = join [
+        0xcb00753f45a35e8b, 0xb5a03d699ac65007, 0x272c32ab0eded163,
+        0x1a8b605a43ff5bed, 0x8086072ba1e7cc23, 0x58baeca134c825a7
+    ]
+
+
+/**
+ * ```repl
+ * :prove emptyStringWorks
+ * ```
+ */
+property emptyStringWorks = SHA384::hash [] == output where
+    output = join [
+        0x38b060a751ac9638, 0x4cd9327eb1b1e36a, 0x21fdb71114be0743,
+        0x4c0cc7bf63f6e1da, 0x274edebfe76f65fb, 0xd51ad2f14898b95b
+    ]
+
+/**
+ * ```repl
+ * :prove alphabet448
+ * ```
+ */
+property alphabet448 = SHA384::hash input == output where
+    input = join "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
+    output = join [
+        0x3391fdddfc8dc739, 0x3707a65b1b470939, 0x7cf8b1d162af05ab,
+        0xfe8f450de5f36bc6, 0xb0455a8520bc4e6f, 0x5fe95b1fe3c8452b
+    ]
+
+/**
+ * ```repl
+ * :prove alphabet896
+ * ```
+ */
+property alphabet896 = SHA384::hash input == output where
+    input = join "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
+    output = join [
+        0x09330c33f71147e8, 0x3d192fc782cd1b47, 0x53111b173b3b05d2,
+        0x2fa08086e3b0f712, 0xfcc7c71a557e2db9, 0x66c3e9fa91746039
+    ]