From d166fd86560d9a968d86291290af20ae66590c28 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Wed, 15 Jan 2025 10:27:19 -0500 Subject: [PATCH 1/5] hash: add hash interface #98 --- Primitive/Keyless/Hash/HashInterface.cry | 42 ++++++++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 Primitive/Keyless/Hash/HashInterface.cry diff --git a/Primitive/Keyless/Hash/HashInterface.cry b/Primitive/Keyless/Hash/HashInterface.cry new file mode 100644 index 00000000..f4920942 --- /dev/null +++ b/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 + */ +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} (width m <= MessageUpperBound) => [m] -> [DigestLength] From 7dd768855ab37a3e45608dd621328bb0b30c9f2d Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Wed, 15 Jan 2025 11:00:00 -0500 Subject: [PATCH 2/5] ecdsa: update to use the hash interface #98 - Removes all the hardcoded SHA-256 components (including a hardcoded maximum message width) in ECDSA - Replaces with the `HashInterface` - Updates the instantiations to use SHA-256 --- .../ECDSA/Instantiations/ECDSA_P256.cry | 5 ++--- .../Signature/ECDSA/Specification.cry | 22 ++++++++----------- .../Signature/ECDSA/UnconstrainedSpec.cry | 17 ++++++++------ Primitive/Keyless/Hash/HashInterface.cry | 2 +- Primitive/Keyless/Hash/SHA2/Specification.cry | 22 ++++++++++++++++--- 5 files changed, 41 insertions(+), 27 deletions(-) diff --git a/Primitive/Asymmetric/Signature/ECDSA/Instantiations/ECDSA_P256.cry b/Primitive/Asymmetric/Signature/ECDSA/Instantiations/ECDSA_P256.cry index 2f11615c..43554735 100644 --- a/Primitive/Asymmetric/Signature/ECDSA/Instantiations/ECDSA_P256.cry +++ b/Primitive/Asymmetric/Signature/ECDSA/Instantiations/ECDSA_P256.cry @@ -6,7 +6,6 @@ */ module Primitive::Asymmetric::Signature::ECDSA::Instantiations::ECDSA_P256 = Primitive::Asymmetric::Signature::ECDSA::Specification { - Common::EC::PrimeField::Instantiations::P256 + EC = Common::EC::PrimeField::Instantiations::P256, + Hash = Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 } - - diff --git a/Primitive/Asymmetric/Signature/ECDSA/Specification.cry b/Primitive/Asymmetric/Signature/ECDSA/Specification.cry index dadf19a4..1f254e3d 100644 --- a/Primitive/Asymmetric/Signature/ECDSA/Specification.cry +++ b/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 . 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`. diff --git a/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry b/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry index 819b972b..a10fc025 100644 --- a/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry +++ b/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 diff --git a/Primitive/Keyless/Hash/HashInterface.cry b/Primitive/Keyless/Hash/HashInterface.cry index f4920942..7e36a781 100644 --- a/Primitive/Keyless/Hash/HashInterface.cry +++ b/Primitive/Keyless/Hash/HashInterface.cry @@ -39,4 +39,4 @@ interface module Primitive::Keyless::Hash::HashInterface where * Hash function, mapping an arbitrary-length message to a fixed-length * message digest. */ - hash: {m} (width m <= MessageUpperBound) => [m] -> [DigestLength] + hash: {m} (width m < MessageUpperBound) => [m] -> [DigestLength] diff --git a/Primitive/Keyless/Hash/SHA2/Specification.cry b/Primitive/Keyless/Hash/SHA2/Specification.cry index cf2aff45..0744da0c 100644 --- a/Primitive/Keyless/Hash/SHA2/Specification.cry +++ b/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 /** From 53d132defaf4a60f962683a836e819e95d0e96fb Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Wed, 15 Jan 2025 12:27:24 -0500 Subject: [PATCH 3/5] ecdsa: rename p256-sha256 instantiation #98 Renaming now that we could implement ECDSA with other hash functions -- the instantiation name needs to specify which hash is being used! --- .../Instantiations/{ECDSA_P256.cry => ECDSA_P256_SHA256.cry} | 4 ++-- Primitive/Asymmetric/Signature/ECDSA/Tests/ECDSA_P256.cry | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) rename Primitive/Asymmetric/Signature/ECDSA/Instantiations/{ECDSA_P256.cry => ECDSA_P256_SHA256.cry} (78%) diff --git a/Primitive/Asymmetric/Signature/ECDSA/Instantiations/ECDSA_P256.cry b/Primitive/Asymmetric/Signature/ECDSA/Instantiations/ECDSA_P256_SHA256.cry similarity index 78% rename from Primitive/Asymmetric/Signature/ECDSA/Instantiations/ECDSA_P256.cry rename to Primitive/Asymmetric/Signature/ECDSA/Instantiations/ECDSA_P256_SHA256.cry index 43554735..44b09932 100644 --- a/Primitive/Asymmetric/Signature/ECDSA/Instantiations/ECDSA_P256.cry +++ b/Primitive/Asymmetric/Signature/ECDSA/Instantiations/ECDSA_P256_SHA256.cry @@ -1,10 +1,10 @@ /* - * Instantiate ECDSA with curve P-256 (also known as secp256p1). + * Instantiate ECDSA with curve P-256 (also known as secp256p1) and SHA256. * * @copyright Galois, Inc. * @author Marcella Hastings */ -module Primitive::Asymmetric::Signature::ECDSA::Instantiations::ECDSA_P256 = +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 diff --git a/Primitive/Asymmetric/Signature/ECDSA/Tests/ECDSA_P256.cry b/Primitive/Asymmetric/Signature/ECDSA/Tests/ECDSA_P256.cry index 56389917..0248a1bf 100644 --- a/Primitive/Asymmetric/Signature/ECDSA/Tests/ECDSA_P256.cry +++ b/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 */ -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) /** From 4f5dab582202d273cf10523d7406e3caaca66718 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Wed, 15 Jan 2025 14:42:40 -0500 Subject: [PATCH 4/5] sha3: instantiate `HashInterface` for SHA3 #98 Adds a `fin` constraint to the interface to support truly arbitrary message lengths in SHA3. --- Primitive/Keyless/Hash/HashInterface.cry | 2 +- Primitive/Keyless/Hash/SHA3/SHA3.cry | 21 +++++++++++++++++++++ 2 files changed, 22 insertions(+), 1 deletion(-) diff --git a/Primitive/Keyless/Hash/HashInterface.cry b/Primitive/Keyless/Hash/HashInterface.cry index 7e36a781..70e027fb 100644 --- a/Primitive/Keyless/Hash/HashInterface.cry +++ b/Primitive/Keyless/Hash/HashInterface.cry @@ -39,4 +39,4 @@ interface module Primitive::Keyless::Hash::HashInterface where * Hash function, mapping an arbitrary-length message to a fixed-length * message digest. */ - hash: {m} (width m < MessageUpperBound) => [m] -> [DigestLength] + hash: {m} (fin m, width m < MessageUpperBound) => [m] -> [DigestLength] diff --git a/Primitive/Keyless/Hash/SHA3/SHA3.cry b/Primitive/Keyless/Hash/SHA3/SHA3.cry index 0ad05ab0..f060e187 100644 --- a/Primitive/Keyless/Hash/SHA3/SHA3.cry +++ b/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. From 40cd5d627593e4789f97121a78bfd46120fa7a2c Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Wed, 15 Jan 2025 14:49:05 -0500 Subject: [PATCH 5/5] ecdsa: update readme to reflect generic hash #98 --- Primitive/Asymmetric/Signature/ECDSA/README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Primitive/Asymmetric/Signature/ECDSA/README.md b/Primitive/Asymmetric/Signature/ECDSA/README.md index e12fd65e..b9a38df1 100644 --- a/Primitive/Asymmetric/Signature/ECDSA/README.md +++ b/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/`.