Add interface for fixed-length hash functions

Primitive/Asymmetric/Signature/ECDSA/Instantiations/ECDSA_P256_SHA256.cry

@@ -0,0 +1,11 @@
+/*
+ * Instantiate ECDSA with curve P-256 (also known as secp256p1) and SHA256.
+ *
+ * @copyright Galois, Inc.
+ * @author Marcella Hastings <[email protected]>
+ */
+module Primitive::Asymmetric::Signature::ECDSA::Instantiations::ECDSA_P256_SHA256 =
+    Primitive::Asymmetric::Signature::ECDSA::Specification {
+        EC = Common::EC::PrimeField::Instantiations::P256,
+        Hash = Primitive::Keyless::Hash::SHA2::Instantiations::SHA256
+    }

Primitive/Asymmetric/Signature/ECDSA/README.md

@@ -1,10 +1,10 @@
 # Elliptic curve digital signature algorithm (ECDSA)
 
-ECDSA is the elliptic-curve analog of the digital signature algorithm, specified in [FIPS 186-5](https://doi.org/10.6028/NIST.FIPS.186-5). The security of ECDSA depends on two primitives: the elliptic curve and the hash function. At this time, the implementation is generic over elliptic curve but fixes the hash function to SHA-256.
+ECDSA is the elliptic-curve analog of the digital signature algorithm, specified in [FIPS 186-5](https://doi.org/10.6028/NIST.FIPS.186-5). The security of ECDSA depends on two primitives: the elliptic curve and the hash function. At this time, the implementation is generic over both primitives.
 
 Structurally, there are two separate specification files:
-- `Specification.cry` matches the spec as closely as possible;
-- `UnconstrainedSpec.cry` implements the same algorithms but omits some of the top-level domain parameter constraints (e.g. on the size of the curve; on the relative security of the curve and hash function)
+- `UnconstrainedSpec.cry` implements the algorithms from the spec;
+- `Specification.cry` uses the algorithms from the unconstrained spec and adds required constraints on the domain parameters. Specifically, it sets a minimum allowable bit length for the size of the elliptic curve and requires the hash function to be at least as secure as the elliptic curve.
 
 We recommend using `Specification.cry` for most applications to ensure compliance with FIPS 186-5.
 The FIPS 186-5 compliant implementation has been instantiated and tested with curve P-256 and SHA256 (see `Instantiations/` and `Tests/`, respectively). Both versions rely on the curve implementation in `Common/EC/PrimeField/`.

Primitive/Asymmetric/Signature/ECDSA/Specification.cry

@@ -39,22 +39,18 @@ module Primitive::Asymmetric::Signature::ECDSA::Specification where
  */
 import interface Common::EC::ECInterface as EC
 
-
-import Primitive::Asymmetric::Signature::ECDSA::UnconstrainedSpec
-    { interface EC } as USpec
-
 /**
  * ECDSA digital signature generation and verification requires an approved
  * hash function or XOF (extendable-output function).
- * This implementation currently fixes the hash function to SHA256, as
- * specified in [FIPS-180-4].
- *
- * @design Marcella Hastings <[email protected]>. Fixing the hash function
- *   to SHA256 is due to lack of an appropriate hash-function interface, not
- *   for any technical reason. This is intended to be a temporary state,
- *   blocked on the creation of such an interface.
  */
-import Primitive::Keyless::Hash::SHA2Imperative::SHA256 as Hash
+import interface Primitive::Keyless::Hash::HashInterface as Hash
+
+/**
+ * The unconstrained spec is instantiated with the same curve and hash function
+ * specified here.
+ */
+import Primitive::Asymmetric::Signature::ECDSA::UnconstrainedSpec
+    { EC = interface EC , Hash = interface Hash } as USpec
 
 /**
  * The standard specifies four ranges for the bit length of `n` (the order of
@@ -75,7 +71,7 @@ type ECSecurityStrength = (width EC::n / 2)
  * security strength associated with the curve.
  * [FIPS-186-5] Section 6.1.1.
  */
-interface constraint (ECSecurityStrength <= Hash::securityStrength)
+interface constraint (ECSecurityStrength <= Hash::SecurityStrength)
 
 // Documentation for the public interface of this API can be found in
 // `UnconstrainedSpec.cry`.

Primitive/Asymmetric/Signature/ECDSA/Tests/ECDSA_P256.cry

@@ -9,7 +9,7 @@ Test vectors for ECDSA with curve P256.
 @copyright Galois, Inc.
 @author Marcella Hastings <[email protected]>
 */
-import Primitive::Asymmetric::Signature::ECDSA::Instantiations::ECDSA_P256 as ECDSA
+import Primitive::Asymmetric::Signature::ECDSA::Instantiations::ECDSA_P256_SHA256 as ECDSA
 import Common::utils(BVtoZ)
 
 /**

Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry

@@ -50,7 +50,7 @@ import interface Common::EC::ECInterface as EC
  * This implementation currently fixes the hash function to SHA256, as
  * specified in [FIPS-180-4].
  */
-import Primitive::Keyless::Hash::SHA2Imperative::SHA256 as Hash
+import interface Primitive::Keyless::Hash::HashInterface as Hash
 
 /**
  * ECDSA signature generation algorithm.
@@ -99,7 +99,8 @@ import Primitive::Keyless::Hash::SHA2Imperative::SHA256 as Hash
  * In all inputs and outputs, `n` is the order of the base point `G` for the
  * elliptic curve specified in the `PFEC` interface.
  */
-sign : {m} (fin m, width m < 64) => [m] -> Z EC::n -> Z EC::n -> Option (Z EC::n, Z EC::n)
+sign : {m} (fin m, width m < Hash::MessageUpperBound) =>
+    [m] -> Z EC::n -> Z EC::n -> Option (Z EC::n, Z EC::n)
 sign M d k = if inputsInRange then maybe_rs else None
     where
         // Preconditions must hold.
@@ -160,7 +161,8 @@ sign M d k = if inputsInRange then maybe_rs else None
  * In all inputs and outputs, `n` is the order of the base point `G` for the
  * elliptic curve specified in the `PFEC` interface.
  */
-verify : {m} (fin m, width m < 64) => [m] -> (Z EC::n, Z EC::n) -> EC::Point -> Bool
+verify : {m} (fin m, width m < Hash::MessageUpperBound) =>
+    [m] -> (Z EC::n, Z EC::n) -> EC::Point -> Bool
 verify M (r, s) Q = inputsInRange && rMatches
     where
         // Step 1.
@@ -210,7 +212,8 @@ publicKey d = EC::scmul (fromZ d) EC::G
  * :check signAndVerifyIsCorrect`{64}
  * ```
  */
-signAndVerifyIsCorrect : {m} (fin m, width m < 64) => [m] -> Z EC::n -> Z EC::n -> Bool
+signAndVerifyIsCorrect : {m} (fin m, width m < Hash::MessageUpperBound) =>
+    [m] -> Z EC::n -> Z EC::n -> Bool
 property signAndVerifyIsCorrect M d k = verification
     where
         Q = publicKey d
@@ -223,11 +226,11 @@ private
     /**
      * Hash a message and convert it to an integer mod `n`.
      */
-    hashAndTruncate : {m} (fin m, width m < 64) => [m] -> Z EC::n
+    hashAndTruncate : {m} (fin m, width m < Hash::MessageUpperBound) => [m] -> Z EC::n
     hashAndTruncate M = e
         where
-            H = Hash::sha M
-            e' = take`{min (width EC::n) Hash::digestSize} H
+            H = Hash::hash M
+            e' = take`{min (width EC::n) Hash::DigestLength} H
             // Cryptol's default bitstring-to-integer `toInteger` conversion
             // matches the routine specified in [FIPS-186-5] Appendix B.2.1.
             // We further convert it to an element in `Z n` to support the modular

Primitive/Keyless/Hash/HashInterface.cry

@@ -0,0 +1,42 @@
+/*
+ * Interface for a hash function with a fixed-length digest.
+ *
+ * This is designed for use in algorithms that require an arbitrary hash
+ * function. It does not support extendable-output functions that allow
+ * arbitrary-length outputs.
+ *
+ * @copyright Galois, Inc 2025
+ * @author Marcella Hastings <[email protected]>
+ */
+interface module Primitive::Keyless::Hash::HashInterface where
+    /**
+     * Upper bound on the length of messages that can be hashed with this
+     * hash function.
+     *
+     * This can be set to `inf` for hash functions that do not have a
+     * restriction on message length.
+     */
+    type MessageUpperBound : #
+
+    /**
+     * Length of the hash digest, in bits.
+     */
+    type DigestLength : #
+
+    /**
+     * Security strength (in bits) of the hash function.
+     *
+     * This is assumed to be the minimum of the collision resistance strength,
+     * the preimage resistance strength, and the second preimage resistance
+     * strength. For most NIST-standardized hash functions, the security
+     * strength is half the digest length. The exception is SHA-1, which is
+     * largely deprecated.
+     * @see https://csrc.nist.gov/projects/hash-functions#security-strengths
+     */
+    type SecurityStrength : #
+
+    /**
+     * Hash function, mapping an arbitrary-length message to a fixed-length
+     * message digest.
+     */
+    hash: {m} (fin m, width m < MessageUpperBound) => [m] -> [DigestLength]

Primitive/Keyless/Hash/SHA2/Specification.cry

@@ -55,10 +55,26 @@ parameter
 
 /**
  * Upper bound on the width of messages that can be processed.
- * [FIPS-180-4] Section 1, Figure 1.
+ * [FIPS-180-4] Section 1, Figure 1, "Message Size (bits)"
  */
-type MaxMessageWidth = 2 * w
-type constraint ValidMessageLength L = width L < MaxMessageWidth
+type MessageUpperBound = 2 * w
+type constraint ValidMessageLength L = width L < MessageUpperBound
+
+/**
+ * Length of the hash digest.
+ *
+ * This is made public to instantiate the `HashInterface`.
+ */
+type DigestLength = DigestSize
+
+/**
+ * Security strength (in bits) of the hash function.
+ * @see NIST SP 800-107 (to be withdrawn): https://csrc.nist.gov/pubs/sp/800/107/r1/final
+ * @see Hash functions webpage: https://csrc.nist.gov/projects/hash-functions
+ *
+ * This is made public to instantiate the `HashInterface`.
+ */
+type SecurityStrength = DigestSize / 2
 
 private
     /**

Primitive/Keyless/Hash/SHA3/SHA3.cry

@@ -30,6 +30,27 @@ parameter
     type digest : #
     type constraint (fin digest, digest % 8 == 0, digest >= 224, digest <= 512)
 
+/**
+ * Length of the hash digest.
+ *
+ * This is made public to instantiate the `HashInterface`.
+ */
+type DigestLength = digest
+
+/**
+ * There is no upper bound on the message length for SHA3 hashes.
+ */
+type MessageUpperBound = inf
+
+/**
+ * Security strength (in bits) of the hash function.
+ * [FIPS-202] Appendix A.1, Table 4.
+ * @see Hash functions webpage: https://csrc.nist.gov/projects/hash-functions#security-strengths
+ *
+ * This is made public to instantiate the `HashInterface`.
+ */
+type SecurityStrength = DigestLength / 2
+
 /**
  * SHA-3 hash function specification.
  * [FIPS-202] Section 6.1.