From f7e5ada840d750a46fe0d0a95b6c830490cca7c1 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 15 Aug 2024 10:47:02 -0400 Subject: [PATCH 1/6] sha2: Add message schedule #112 --- Primitive/Keyless/Hash/SHA2/Specification.cry | 37 ++++++++++++++++--- 1 file changed, 32 insertions(+), 5 deletions(-) diff --git a/Primitive/Keyless/Hash/SHA2/Specification.cry b/Primitive/Keyless/Hash/SHA2/Specification.cry index dc25b2db..22080208 100644 --- a/Primitive/Keyless/Hash/SHA2/Specification.cry +++ b/Primitive/Keyless/Hash/SHA2/Specification.cry @@ -51,6 +51,19 @@ private */ 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 +187,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 +266,20 @@ private */ parse : {N} () => [N * BlockSize] -> [N][BlockSize] parse M = split M + + /** + * All the SHA functions (excluding SHA-1) in the spec share the same + * message schedule. + * + * [FIPS-180-4] Section 6.2.2 #1 and Section 6.4.2 #1. + */ + messageSchedule : [16][w] -> [ScheduleLength][w] + messageSchedule Mi = take W where + W : [inf][w] + W = Mi # [ sigma1 w2 + w7 + sigma0 w15 + w16 + | w16 <- W + | w15 <- drop`{1} W + | w7 <- drop`{9} W + | w2 <- drop`{14} W + ] + From 606f30f6860ba355c1414bdcf789a10fe66124b9 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 15 Aug 2024 16:12:35 -0400 Subject: [PATCH 2/6] sha2: add hash function implementation #112 - Add tests for SHA256 - I haven't tested this for 512 or for truncated versions --- .../Hash/SHA2/Instantiations/SHA256.cry | 4 +- .../Hash/SHA2/Instantiations/SHA384.cry | 2 + .../Hash/SHA2/Instantiations/SHA512.cry | 2 + Primitive/Keyless/Hash/SHA2/Specification.cry | 49 +++++++++++++++++++ Primitive/Keyless/Hash/SHA2/Tests/SHA256.cry | 40 +++++++++++++++ 5 files changed, 96 insertions(+), 1 deletion(-) create mode 100644 Primitive/Keyless/Hash/SHA2/Tests/SHA256.cry diff --git a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry index eab58044..1830483e 100644 --- a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry +++ b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry @@ -4,11 +4,13 @@ * @copyright Galois, Inc * @author Marcella Hastings */ -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 = [ diff --git a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry index d0f5e686..d9a67ed4 100644 --- a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry +++ b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry @@ -9,6 +9,8 @@ module Primitive::Keyless::Hash::SHA2::Instantiations::SHA384 = 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 = [ diff --git a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry index 171851ef..09586b56 100644 --- a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry +++ b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry @@ -9,6 +9,8 @@ module Primitive::Keyless::Hash::SHA2::Instantiations::SHA512 = 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 = [ diff --git a/Primitive/Keyless/Hash/SHA2/Specification.cry b/Primitive/Keyless/Hash/SHA2/Specification.cry index 22080208..d1654314 100644 --- a/Primitive/Keyless/Hash/SHA2/Specification.cry +++ b/Primitive/Keyless/Hash/SHA2/Specification.cry @@ -31,6 +31,9 @@ parameter type w : # type constraint (w % 32 == 0, 32 <= w, 64 >= w) + type DigestSize : # + type constraint (8 * w >= DigestSize) + /** * Initial hash value. * These are defined in [FIPS-180-4] Section 5.3. @@ -277,9 +280,55 @@ private 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. | w16 <- W | w15 <- drop`{1} W | w7 <- drop`{9} W | w2 <- drop`{14} W ] + type LetterVars = ([w], [w], [w], [w], [w], [w], [w], [w]) + +hash: {l} (ValidMessageLength l) => [l] -> [DigestSize] +hash M = drop (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... + [ digestUpdate l Kt Wt + | l <- letters + + // ...for t=0 to 63 + | Wt <- Ws + | Kt <- K + ] + (a, b, c, d, e, f, g, h) = letters ! 0 + + // Step 4. Compute the intermediate hash value. + 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) + | [Hi0, Hi1, Hi2, Hi3, Hi4, Hi5, Hi6, Hi7] <- digest + ] + + // Step 3. Update temporary and working variables (one iteration). + digestUpdate : LetterVars -> [w] -> [w] -> LetterVars + digestUpdate (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 diff --git a/Primitive/Keyless/Hash/SHA2/Tests/SHA256.cry b/Primitive/Keyless/Hash/SHA2/Tests/SHA256.cry new file mode 100644 index 00000000..23b65e3b --- /dev/null +++ b/Primitive/Keyless/Hash/SHA2/Tests/SHA256.cry @@ -0,0 +1,40 @@ +import Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 as SHA256 + +/** + * ```repl + * :prove abcWorks + * ``` + */ +property abcWorks = SHA256::hash (join "abc") == 0xba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad + +/** + * ```repl + * :prove emptyStringWorks + * ``` + */ +property emptyStringWorks = SHA256::hash [] == 0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855 + +/** + * ```repl + * :prove alphabet448 + * ``` + */ +property alphabet448 = SHA256::hash input == output where + input = join "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq" + output = 0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1 + +/** + * ```repl + * :prove alphabet896 + * ``` + */ +property alphabet896 = SHA256::hash input == output where + input = join "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu" + output = 0xcf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1 + +/** + * This has not yet proved for me. + */ +property aaaaaah = SHA256::hash input == output where + input = join (join (take`{1000000} (repeat "a"))) + output = 0xcdc76e5c9914fb9281a1c7e284d73e67f1809a48a497200e046d39ccc7112cd0 \ No newline at end of file From 33418e3c2c5dddac5f8bafa721510b774efe076f Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Fri, 16 Aug 2024 09:00:39 -0400 Subject: [PATCH 3/6] sha2: add instantiations + tests for 384, 512 #112 - fixes a bug in the truncation (came from the wrong end) --- Primitive/Keyless/Hash/SHA2/Specification.cry | 2 +- Primitive/Keyless/Hash/SHA2/Tests/SHA384.cry | 48 +++++++++++++++++ Primitive/Keyless/Hash/SHA2/Tests/SHA512.cry | 52 +++++++++++++++++++ 3 files changed, 101 insertions(+), 1 deletion(-) create mode 100644 Primitive/Keyless/Hash/SHA2/Tests/SHA384.cry create mode 100644 Primitive/Keyless/Hash/SHA2/Tests/SHA512.cry diff --git a/Primitive/Keyless/Hash/SHA2/Specification.cry b/Primitive/Keyless/Hash/SHA2/Specification.cry index d1654314..2240743d 100644 --- a/Primitive/Keyless/Hash/SHA2/Specification.cry +++ b/Primitive/Keyless/Hash/SHA2/Specification.cry @@ -290,7 +290,7 @@ private type LetterVars = ([w], [w], [w], [w], [w], [w], [w], [w]) hash: {l} (ValidMessageLength l) => [l] -> [DigestSize] -hash M = drop (join (digest ! 0)) where +hash M = take (join (digest ! 0)) where digest = [H0] # [Hi where // Step 1. Prepare the message schedule. diff --git a/Primitive/Keyless/Hash/SHA2/Tests/SHA384.cry b/Primitive/Keyless/Hash/SHA2/Tests/SHA384.cry new file mode 100644 index 00000000..02e10628 --- /dev/null +++ b/Primitive/Keyless/Hash/SHA2/Tests/SHA384.cry @@ -0,0 +1,48 @@ +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 + ] diff --git a/Primitive/Keyless/Hash/SHA2/Tests/SHA512.cry b/Primitive/Keyless/Hash/SHA2/Tests/SHA512.cry new file mode 100644 index 00000000..7234abad --- /dev/null +++ b/Primitive/Keyless/Hash/SHA2/Tests/SHA512.cry @@ -0,0 +1,52 @@ +import Primitive::Keyless::Hash::SHA2::Instantiations::SHA512 as SHA512 + +/** + * ```repl + * :prove abcWorks + * ``` + */ +property abcWorks = SHA512::hash (join "abc") == output where + output = join [ + 0xddaf35a193617aba, 0xcc417349ae204131, 0x12e6fa4e89a97ea2, + 0x0a9eeee64b55d39a, 0x2192992a274fc1a8, 0x36ba3c23a3feebbd, + 0x454d4423643ce80e, 0x2a9ac94fa54ca49f + ] + + +/** + * ```repl + * :prove emptyStringWorks + * ``` + */ +property emptyStringWorks = SHA512::hash [] == output where + output = join [ + 0xcf83e1357eefb8bd, 0xf1542850d66d8007, 0xd620e4050b5715dc, + 0x83f4a921d36ce9ce, 0x47d0d13c5d85f2b0, 0xff8318d2877eec2f, + 0x63b931bd47417a81, 0xa538327af927da3e + ] + +/** + * ```repl + * :prove alphabet448 + * ``` + */ +property alphabet448 = SHA512::hash input == output where + input = join "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq" + output = join [ + 0x204a8fc6dda82f0a, 0x0ced7beb8e08a416, 0x57c16ef468b228a8, + 0x279be331a703c335, 0x96fd15c13b1b07f9, 0xaa1d3bea57789ca0, + 0x31ad85c7a71dd703, 0x54ec631238ca3445 + ] + +/** + * ```repl + * :prove alphabet896 + * ``` + */ +property alphabet896 = SHA512::hash input == output where + input = join "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu" + output = join [ + 0x8e959b75dae313da, 0x8cf4f72814fc143f, 0x8f7779c6eb9f7fa1, + 0x7299aeadb6889018, 0x501d289e4900f7e4, 0x331b99dec4b5433a, + 0xc7d329eeb6dd2654, 0x5e96e55b874be909 + ] \ No newline at end of file From f4d61c7c0135d784ca43ddb052576e70ea25491c Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Fri, 16 Aug 2024 14:06:14 -0400 Subject: [PATCH 4/6] sha2: improve docs, add copyrights #112 --- .../Hash/SHA2/Instantiations/SHA256.cry | 8 ++- .../Hash/SHA2/Instantiations/SHA384.cry | 8 ++- .../Hash/SHA2/Instantiations/SHA512.cry | 8 ++- Primitive/Keyless/Hash/SHA2/Specification.cry | 70 ++++++++++++------- Primitive/Keyless/Hash/SHA2/Tests/SHA256.cry | 49 ++++++++++--- Primitive/Keyless/Hash/SHA2/Tests/SHA384.cry | 20 ++++++ Primitive/Keyless/Hash/SHA2/Tests/SHA512.cry | 22 +++++- 7 files changed, 144 insertions(+), 41 deletions(-) diff --git a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry index 1830483e..ab536860 100644 --- a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry +++ b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry @@ -1,8 +1,14 @@ /** - * Secure hash algorithm SHA256. + * Secure hash algorithm SHA-256 as specified in [FIPS-180-4]. * * @copyright Galois, Inc * @author Marcella Hastings + * + * [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::SHA256 = Primitive::Keyless::Hash::SHA2::Specification diff --git a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry index d9a67ed4..4440af4d 100644 --- a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry +++ b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry @@ -1,8 +1,14 @@ /** - * Secure hash algorithm SHA384. + * Secure hash algorithm SHA-384 as specified in [FIPS-180-4]. * * @copyright Galois, Inc * @author Marcella Hastings + * + * [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 diff --git a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry index 09586b56..2e90fb6c 100644 --- a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry +++ b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry @@ -1,8 +1,14 @@ /** - * Secure hash algorithm SHA512. + * Secure hash algorithm SHA-512 as specified in [FIPS-180-4]. * * @copyright Galois, Inc * @author Marcella Hastings + * + * [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 diff --git a/Primitive/Keyless/Hash/SHA2/Specification.cry b/Primitive/Keyless/Hash/SHA2/Specification.cry index 2240743d..0959bf15 100644 --- a/Primitive/Keyless/Hash/SHA2/Specification.cry +++ b/Primitive/Keyless/Hash/SHA2/Specification.cry @@ -270,28 +270,25 @@ private parse : {N} () => [N * BlockSize] -> [N][BlockSize] parse M = split M - /** - * All the SHA functions (excluding SHA-1) in the spec share the same - * message schedule. - * - * [FIPS-180-4] Section 6.2.2 #1 and Section 6.4.2 #1. - */ - 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. - | w16 <- W - | w15 <- drop`{1} W - | w7 <- drop`{9} W - | w2 <- drop`{14} W - ] - - type LetterVars = ([w], [w], [w], [w], [w], [w], [w], [w]) +/** + * 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 + digest = [H0] # [Hi' where // Step 1. Prepare the message schedule. Ws = messageSchedule (split Mi) @@ -299,27 +296,48 @@ hash M = take (join (digest ! 0)) where // 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... - [ digestUpdate l Kt Wt + // Step 3. Update temporary and working variables... + [ variableUpdate l Kt Wt | l <- letters - // ...for t=0 to 63 + // ...for t=0 to `ScheduleLength`. | Wt <- Ws | Kt <- K ] (a, b, c, d, e, f, g, h) = letters ! 0 - // Step 4. Compute the intermediate hash value. - Hi = [a + Hi0, b + Hi1, c + Hi2, d + Hi3, e + Hi4, f + Hi5, g + Hi6, h + Hi7] + // 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). - digestUpdate : LetterVars -> [w] -> [w] -> LetterVars - digestUpdate (a, b, c, d, e, f, g, h) Kt Wt = + 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 diff --git a/Primitive/Keyless/Hash/SHA2/Tests/SHA256.cry b/Primitive/Keyless/Hash/SHA2/Tests/SHA256.cry index 23b65e3b..7ae63d8d 100644 --- a/Primitive/Keyless/Hash/SHA2/Tests/SHA256.cry +++ b/Primitive/Keyless/Hash/SHA2/Tests/SHA256.cry @@ -1,3 +1,23 @@ +/** + * 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 + * + * [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 /** @@ -5,14 +25,22 @@ import Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 as SHA256 * :prove abcWorks * ``` */ -property abcWorks = SHA256::hash (join "abc") == 0xba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad +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 [] == 0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855 +property emptyStringWorks = SHA256::hash [] == output where + output = join [ + 0xe3b0c442, 0x98fc1c14, 0x9afbf4c8, 0x996fb924, + 0x27ae41e4, 0x649b934c, 0xa495991b, 0x7852b855 + ] /** * ```repl @@ -21,7 +49,10 @@ property emptyStringWorks = SHA256::hash [] == 0xe3b0c44298fc1c149afbf4c8996fb92 */ property alphabet448 = SHA256::hash input == output where input = join "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq" - output = 0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1 + output = join [ + 0x248d6a61, 0xd20638b8, 0xe5c02693, 0x0c3e6039, + 0xa33ce459, 0x64ff2167, 0xf6ecedd4, 0x19db06c1 + ] /** * ```repl @@ -30,11 +61,7 @@ property alphabet448 = SHA256::hash input == output where */ property alphabet896 = SHA256::hash input == output where input = join "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu" - output = 0xcf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1 - -/** - * This has not yet proved for me. - */ -property aaaaaah = SHA256::hash input == output where - input = join (join (take`{1000000} (repeat "a"))) - output = 0xcdc76e5c9914fb9281a1c7e284d73e67f1809a48a497200e046d39ccc7112cd0 \ No newline at end of file + output = join [ + 0xcf5b16a7, 0x78af8380, 0x036ce59e, 0x7b049237, + 0x0b249b11, 0xe8f07a51, 0xafac4503, 0x7afee9d1 + ] diff --git a/Primitive/Keyless/Hash/SHA2/Tests/SHA384.cry b/Primitive/Keyless/Hash/SHA2/Tests/SHA384.cry index 02e10628..f754d629 100644 --- a/Primitive/Keyless/Hash/SHA2/Tests/SHA384.cry +++ b/Primitive/Keyless/Hash/SHA2/Tests/SHA384.cry @@ -1,3 +1,23 @@ +/** + * 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 + * + * [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 /** diff --git a/Primitive/Keyless/Hash/SHA2/Tests/SHA512.cry b/Primitive/Keyless/Hash/SHA2/Tests/SHA512.cry index 7234abad..e2e64e33 100644 --- a/Primitive/Keyless/Hash/SHA2/Tests/SHA512.cry +++ b/Primitive/Keyless/Hash/SHA2/Tests/SHA512.cry @@ -1,3 +1,23 @@ +/** + * Test vectors for SHA512 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 + * + * [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::SHA512 as SHA512 /** @@ -49,4 +69,4 @@ property alphabet896 = SHA512::hash input == output where 0x8e959b75dae313da, 0x8cf4f72814fc143f, 0x8f7779c6eb9f7fa1, 0x7299aeadb6889018, 0x501d289e4900f7e4, 0x331b99dec4b5433a, 0xc7d329eeb6dd2654, 0x5e96e55b874be909 - ] \ No newline at end of file + ] From 166d28a78aaa56a35483bea2e1a067796b851a85 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Mon, 19 Aug 2024 11:28:04 -0400 Subject: [PATCH 5/6] sha2: improve docs #112 --- Primitive/Keyless/Hash/SHA2/Specification.cry | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/Primitive/Keyless/Hash/SHA2/Specification.cry b/Primitive/Keyless/Hash/SHA2/Specification.cry index 0959bf15..db327492 100644 --- a/Primitive/Keyless/Hash/SHA2/Specification.cry +++ b/Primitive/Keyless/Hash/SHA2/Specification.cry @@ -24,13 +24,20 @@ module Primitive::Keyless::Hash::SHA2::Specification where parameter /** - * Word size. + * Length of words, in bits, that are used during hashing. + * * The specification defines words to be either 32 or 64 bits. * [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) @@ -49,8 +56,9 @@ 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 @@ -295,9 +303,9 @@ hash M = take (join (digest ! 0)) where // Step 2. Initialize the eight working variables with the // previous hash value. - letters = [(Hi0, Hi1, Hi2, Hi3, Hi4, Hi5, Hi6, Hi7)] # + letters = [(Hi0, Hi1, Hi2, Hi3, Hi4, Hi5, Hi6, Hi7)] # [ // Step 3. Update temporary and working variables... - [ variableUpdate l Kt Wt + variableUpdate l Kt Wt | l <- letters // ...for t=0 to `ScheduleLength`. From 54cd534f175022772a278016d64385650d1bcc56 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Fri, 23 Aug 2024 09:59:46 -0400 Subject: [PATCH 6/6] sha2: clarify documentation #112 --- Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry | 3 ++- Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry | 3 ++- Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry | 3 ++- Primitive/Keyless/Hash/SHA2/Specification.cry | 4 +++- 4 files changed, 9 insertions(+), 4 deletions(-) diff --git a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry index ab536860..543bf43b 100644 --- a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry +++ b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA256.cry @@ -1,5 +1,6 @@ /** - * Secure hash algorithm SHA-256 as specified in [FIPS-180-4]. + * Instantiation of the secure hash algorithm SHA-256 as specified in + * [FIPS-180-4], Section 5.3.3. * * @copyright Galois, Inc * @author Marcella Hastings diff --git a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry index 4440af4d..2d7c18e9 100644 --- a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry +++ b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA384.cry @@ -1,5 +1,6 @@ /** - * Secure hash algorithm SHA-384 as specified in [FIPS-180-4]. + * Instantiation of the secure hash algorithm SHA-384 as specified in + * [FIPS-180-4], Section 5.3.4. * * @copyright Galois, Inc * @author Marcella Hastings diff --git a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry index 2e90fb6c..788ae712 100644 --- a/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry +++ b/Primitive/Keyless/Hash/SHA2/Instantiations/SHA512.cry @@ -1,5 +1,6 @@ /** - * Secure hash algorithm SHA-512 as specified in [FIPS-180-4]. + * Instantiation of the secure hash algorithm SHA-512 as specified in + * [FIPS-180-4], Section 5.3.5. * * @copyright Galois, Inc * @author Marcella Hastings diff --git a/Primitive/Keyless/Hash/SHA2/Specification.cry b/Primitive/Keyless/Hash/SHA2/Specification.cry index db327492..76b39da2 100644 --- a/Primitive/Keyless/Hash/SHA2/Specification.cry +++ b/Primitive/Keyless/Hash/SHA2/Specification.cry @@ -26,7 +26,9 @@ parameter /** * Length of words, in bits, that are used during hashing. * - * The specification defines words to be either 32 or 64 bits. + * 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 : #