SHA2: Use new version where possible

Primitive/Asymmetric/Signature/RSA_PSS.cry

@@ -1,16 +1,16 @@
 /*
-   Copyright (c) 2021, Galois Inc.
-   www.cryptol.net
-*/
-
-/* This module implements an RSA signature scheme
-   with the EMSA-PSS encoding method described in 9.1 of
-
-   PKCS #1: RSA Cryptography Specifications Version 2.2
-
-   See also:
-   https://tools.ietf.org/html/rfc8017
-*/
+ * @copyright Galois Inc. 2021
+ * @author Andrei Stefanescu
+ * www.cryptol.net
+ *
+ * This module implements an RSA signature scheme
+ * with the EMSA-PSS encoding method described in 9.1 of
+ *
+ * PKCS #1: RSA Cryptography Specifications Version 2.2
+ *
+ * See also:
+ * https://tools.ietf.org/html/rfc8017
+ */
 module Primitive::Asymmetric::Signature::RSA_PSS where
 
 import Common::utils
@@ -19,10 +19,19 @@ parameter
   type hLen : # // Number of octets returned by chosen hash function
   type constraint (fin hLen, hLen >= 1)
 
-  hash : {n} (fin n) => [n][8] -> [8 * hLen]
+  /**
+   * Some hash functions have an upper bound on the message length they support.
+   *
+   * Most uses of `hash` here are on a fixed input made of 8 bytes of padding
+   * an `hLen`-byte hashed message, and an `hLen`-byte salt. The type constraint
+   * enforces that all such calls are on valid-length inputs.
+   */
+  type MessageUpperBound : #
+  type constraint (width (8 * (hLen + hLen + 8)) < MessageUpperBound)
 
+  hash : {n} (fin n, width (8 * n) < MessageUpperBound) => [n][8] -> [8 * hLen]
 
-MGF1 : {seedLen, maskLen} (fin seedLen, fin maskLen) => [seedLen][8] -> [maskLen][8]
+MGF1 : {seedLen, maskLen} (fin seedLen, fin maskLen, width (8 * seedLen + 32) < MessageUpperBound) => [seedLen][8] -> [maskLen][8]
 MGF1 seed = take (join [ split (hash (seed # (split c))) | c <- [(0 : [32]) ...] ])
 
 

Primitive/Asymmetric/Signature/RSA_PSS_SHA384.cry

@@ -6,8 +6,9 @@
 
 module Primitive::Asymmetric::Signature::RSA_PSS_SHA384 = Primitive::Asymmetric::Signature::RSA_PSS where
 
-import Primitive::Keyless::Hash::SHA2Imperative::SHA384
+import Primitive::Keyless::Hash::SHA2::Instantiations::SHA384 as SHA384
 
 type hLen = 48
-hash = SHAImp
+hash m = join (SHA384::hashBytes m)
+type MessageUpperBound = SHA384::MessageUpperBound
 

Primitive/Keyless/Hash/HMAC.cry

@@ -10,7 +10,7 @@
 
 module Primitive::Keyless::Hash::HMAC where
 
-import Primitive::Keyless::Hash::SHA2Imperative::SHA384
+import Primitive::Keyless::Hash::SHA2Internal::SHA384
 
 // Pad or hash `key`, depending on its length, until it is 128 bytes long
 key_init : {key_size} (fin key_size) => [key_size][8] -> [128][8]

Primitive/Keyless/Hash/README.md

@@ -1,4 +1,4 @@
-Hash functions.
+This directory includes executable specifications for several hash functions.
 
 | Scheme | [Gold standard](https://github.com/GaloisInc/cryptol-specs/wiki/Reviewing-guidelines)? | Literate |
 | --- | --- | --- |
@@ -9,3 +9,17 @@ Hash functions.
 | FNV | | No |
 | MD5 | | Yes |
 | SHA1 |  | No |
+
+## SHA2
+There are two versions of SHA2 here, as defined in [FIPS 180-4](https://doi.org/10.6028/NIST.FIPS.180-4). The [`SHA2`](/Primitive/Keyless/Hash/SHA2/) directory contains the spec-adherent version and should be used for the vast majority of applications.
+
+The [`SHA2Internal`](/Primitive/Keyless/Hash/SHA2Internal/) directory contains an equivalent implementation. It was originally written as part of a proof of correctness for a Java implementation of SHA2. It makes public several internal components of SHA2, like the compression function and the state representation, that are not part of the public interface defined in FIPS 180-4.
+These are used in the implementation of several other algorithms in this repo, like [HMAC](/Primitive/Keyless/Hash/HMAC.cry) and [SHACAL](/Primitive/Symmetric/Cipher/Block/SHACAL.cry). We've kept the two instantiations that these dependencies use and [checked equivalence of the two versions](SHA2Internal/Equivalence.cry) but recommend using the spec-adherent version where possible.
+
+## SHA3
+The SHA3 specification includes one internal algorithm, known as [Keccak](Keccak.cry), and two families of public interfaces: the hash functions [SHA3](SHA3/) and the extendable-output functions [SHAKE](SHAKE/).
+
+One quirk of the Keccak algorithm is that it assumes a particularly unusual bit ordering for the input. In practice, most applications do not want to rearrange inputs to match that bit ordering (indeed, the KATs provided by NIST are not provided with that ordering), so the default `hash` and `xof` functions for the `SHA3` and `SHAKE` algorithms take input in big-endian, or most-significant-bit first, ordering. For applications that have unusual bit-ordering needs, the [KeccakBitOrdering](KeccakBitOrdering.cry) module has helper functions to convert between various representations of bits.
+
+## HashInterface
+Some applications require an arbitrary hash function. The `HashInterface` provided is instantiated by both the `SHA2` and `SHA3` hashes.

Primitive/Keyless/Hash/SHA2Internal/Equivalence.cry

@@ -0,0 +1,52 @@
+/**
+ * Properties demonstrating equivalence of the spec-adherent `SHA2`
+ * implementation and the alternative `SHA2Internal` implementation.
+ *
+ * @copyright Galois, Inc.
+ * @author Marcella Hastings <marcella@galois.com>
+ */
+import Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 as SHA_256
+import Primitive::Keyless::Hash::SHA2Internal::SHA256 as SHAI_256
+
+import Primitive::Keyless::Hash::SHA2::Instantiations::SHA384 as SHA_384
+import Primitive::Keyless::Hash::SHA2Internal::SHA384 as SHAI_384
+
+/**
+ * The `internal` version of SHA256 matches the spec-adherent version.
+ * ```repl
+ * :exhaust sha256ImplsAreEquivalent`{10}
+ * :check sha256ImplsAreEquivalent`{256}
+ * ```
+ */
+sha256ImplsAreEquivalent : {m} (fin m, width m < SHA_256::MessageUpperBound) => [m] -> Bit
+property sha256ImplsAreEquivalent m = SHA_256::hash m == SHAI_256::sha m
+
+/**
+ * The byte-wise APIs for the two SHA256 implementations match.
+ * ```repl
+ * :exhaust sha256BytewiseImplsAreEquivalent`{1}
+ * :check sha256BytewiseImplsAreEquivalent`{256}
+ * ```
+ */
+sha256BytewiseImplsAreEquivalent : {m} (fin m, width (8 * m) < SHA_256::MessageUpperBound) => [m][8] -> Bit
+property sha256BytewiseImplsAreEquivalent m = join (SHA_256::hashBytes m) == SHAI_256::SHAImp m
+
+/**
+ * The `internal` version of SHA384 matches the spec-adherent version.
+ * ```repl
+ * :exhaust sha384ImplsAreEquivalent`{10}
+ * :check sha384ImplsAreEquivalent`{256}
+ * ```
+ */
+sha384ImplsAreEquivalent : {m} (fin m, width m < SHA_384::MessageUpperBound) => [m] -> Bit
+property sha384ImplsAreEquivalent m = SHA_384::hash m == SHAI_384::sha m
+
+/**
+ * The byte-wise APIs for the two SHA384 implementations match.
+ * ```repl
+ * :exhaust sha384BytewiseImplsAreEquivalent`{1}
+ * :check sha384BytewiseImplsAreEquivalent`{256}
+ * ```
+ */
+sha384BytewiseImplsAreEquivalent : {m} (fin m, width (8 * m) < SHA_384::MessageUpperBound) => [m][8] -> Bit
+property sha384BytewiseImplsAreEquivalent m = join (SHA_384::hashBytes m) == SHAI_384::SHAImp m

Primitive/Keyless/Hash/SHA2Imperative/SHA.cry → Primitive/Keyless/Hash/SHA2Internal/SHA.cry

@@ -17,7 +17,7 @@ www.cryptol.net
     @see https://doi.org/10.6028/NIST.SP.800-107r1.
 */
 
-module Primitive::Keyless::Hash::SHA2Imperative::SHA where
+module Primitive::Keyless::Hash::SHA2Internal::SHA where
 
 import Array
 import Common::ByteArray

Primitive/Keyless/Hash/SHA2Imperative/SHA256.cry → Primitive/Keyless/Hash/SHA2Internal/SHA256.cry

@@ -7,7 +7,7 @@
    www.cryptol.net
 */
 
-module Primitive::Keyless::Hash::SHA2Imperative::SHA256 = Primitive::Keyless::Hash::SHA2Imperative::SHA where
+module Primitive::Keyless::Hash::SHA2Internal::SHA256 = Primitive::Keyless::Hash::SHA2Internal::SHA where
 
 type wp = 32
 

Primitive/Keyless/Hash/SHA2Imperative/SHA384.cry → Primitive/Keyless/Hash/SHA2Internal/SHA384.cry

@@ -5,7 +5,7 @@
    www.cryptol.net
 */
 
-module Primitive::Keyless::Hash::SHA2Imperative::SHA384 = Primitive::Keyless::Hash::SHA2Imperative::SHA where
+module Primitive::Keyless::Hash::SHA2Internal::SHA384 = Primitive::Keyless::Hash::SHA2Internal::SHA where
 
 type wp = 64
 

Primitive/Symmetric/Cipher/Block/SHACAL.cry

@@ -14,7 +14,7 @@
 
 module Primitive::Symmetric::Cipher::Block::SHACAL where
 
-import Primitive::Keyless::Hash::SHA2Imperative::SHA256
+import Primitive::Keyless::Hash::SHA2Internal::SHA256
 import Primitive::Keyless::Hash::SHA1
 
 /**SHACAL1**/

Primitive/Symmetric/KDF/HKDF.md

@@ -1,3 +1,7 @@
+<!---
+ - @copyright Galois, Inc.
+ - @author Aaron Tomb
+ --->
 # HMAC-based Extract-and-Expand Key Derivation Function (HKDF)
 
 ## Welcome
@@ -88,7 +92,7 @@ parameter
     type constraint validHMACSizes KeyLen MsgLen =
       ( fin KeyLen, fin MsgLen
           , 32 >= width MsgLen
-          , 64 >= width (8 * KeyLen)
+          , 64 > width (8 * KeyLen)
           , 64 >= width (8 * 64 + MsgLen))