From 4ae5dbb4aef756eb8d035ab6955ef7d4014b6367 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 23 Jan 2025 12:56:01 -0500 Subject: [PATCH 1/7] rsa-pss: update with new sha2 implementation #122 - adds some type constraints to accommodate the message length limits in sha2 --- Primitive/Asymmetric/Signature/RSA_PSS.cry | 17 +++++++++++++---- .../Asymmetric/Signature/RSA_PSS_SHA384.cry | 5 +++-- 2 files changed, 16 insertions(+), 6 deletions(-) diff --git a/Primitive/Asymmetric/Signature/RSA_PSS.cry b/Primitive/Asymmetric/Signature/RSA_PSS.cry index ac3ca891..be12d668 100644 --- a/Primitive/Asymmetric/Signature/RSA_PSS.cry +++ b/Primitive/Asymmetric/Signature/RSA_PSS.cry @@ -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] - - -MGF1 : {seedLen, maskLen} (fin seedLen, fin maskLen) => [seedLen][8] -> [maskLen][8] + /** + * 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, width (8 * seedLen + 32) < MessageUpperBound) => [seedLen][8] -> [maskLen][8] MGF1 seed = take (join [ split (hash (seed # (split c))) | c <- [(0 : [32]) ...] ]) diff --git a/Primitive/Asymmetric/Signature/RSA_PSS_SHA384.cry b/Primitive/Asymmetric/Signature/RSA_PSS_SHA384.cry index 3d9fd833..0bff9bcd 100644 --- a/Primitive/Asymmetric/Signature/RSA_PSS_SHA384.cry +++ b/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 From 768a60bda6feb17484497f4f9a93678a74e164ef Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 23 Jan 2025 13:16:45 -0500 Subject: [PATCH 2/7] hmac: replace SHA2 with new instantiation #122 Also adds a test vector. --- Primitive/Symmetric/MAC/HMAC.cry | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/Primitive/Symmetric/MAC/HMAC.cry b/Primitive/Symmetric/MAC/HMAC.cry index f4802e3a..80effc5f 100644 --- a/Primitive/Symmetric/MAC/HMAC.cry +++ b/Primitive/Symmetric/MAC/HMAC.cry @@ -7,16 +7,16 @@ module Primitive::Symmetric::MAC::HMAC where -import Primitive::Keyless::Hash::SHA2Imperative::SHA256 +import Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 as SHA256 //////// Functional version //////// -sha256Wrap msg = sha (join msg) +sha256Wrap msg = SHA256::hash (join msg) hmacSHA256 : {pwBytes, msgBytes} (fin pwBytes, fin msgBytes , 32 >= width msgBytes - , 64 >= width (8*pwBytes) + , 64 > width (8*pwBytes) , 64 >= width (8 * (64 + msgBytes)) ) => [pwBytes][8] -> [msgBytes][8] -> [256] hmacSHA256 = hmac `{blockLength=64} sha256Wrap sha256Wrap sha256Wrap @@ -50,7 +50,18 @@ hmac hash hash2 hash3 key message = hash2 (okey # internal) ikey = [k ^ 0x36 | k <- ks] internal = split (hash (ikey # message)) - +/** + * Test vector from NIST's CAVP program. + * @see https://csrc.nist.gov/projects/cryptographic-algorithm-validation-program/message-authentication#Testing + * ```repl + * :prove cavpTest30 + * ``` + */ +property cavpTest30 = digest == expected_digest where + key = split 0x9779d9120642797f1747025d5b22b7ac607cab08e1758f2f3a46c8be1e25c53b8c6a8f58ffefa176 + msg = split 0xb1689c2591eaf3c9e66070f8a77954ffb81749f1b00346f9dfe0b2ee905dcc288baf4a92de3f4001dd9f44c468c3d07d6c6ee82faceafc97c2fc0fc0601719d2dcd0aa2aec92d1b0ae933c65eb06a03c9c935c2bad0459810241347ab87e9f11adb30415424c6c7f5f22a003b8ab8de54f6ded0e3ab9245fa79568451dfa258e + expected_digest = 0x769f00d3e6a6cc1fb426a14a4f76c6462e6149726e0dee0ec0cf97a16605ac8b + digest = hmacSHA256 key msg From a6c53e99be41aca980a446d55dd3528cc8f5fb8f Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 23 Jan 2025 14:03:29 -0500 Subject: [PATCH 3/7] hkdf: fix constraints to match hmac #122 Adjusting to match the underlying SHA2 requirement Also this accidentally changes the newline format from CRLF to LF --- Primitive/Symmetric/KDF/HKDF.md | 2 +- Primitive/Symmetric/KDF/HKDF256.cry | 23 +++++++++++------------ 2 files changed, 12 insertions(+), 13 deletions(-) diff --git a/Primitive/Symmetric/KDF/HKDF.md b/Primitive/Symmetric/KDF/HKDF.md index 38cb49b3..94492d60 100644 --- a/Primitive/Symmetric/KDF/HKDF.md +++ b/Primitive/Symmetric/KDF/HKDF.md @@ -88,7 +88,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)) diff --git a/Primitive/Symmetric/KDF/HKDF256.cry b/Primitive/Symmetric/KDF/HKDF256.cry index 3e42f16f..7b50d9f4 100644 --- a/Primitive/Symmetric/KDF/HKDF256.cry +++ b/Primitive/Symmetric/KDF/HKDF256.cry @@ -1,12 +1,11 @@ -module Primitive::Symmetric::KDF::HKDF256 = Primitive::Symmetric::KDF::HKDF where - -import Primitive::Symmetric::MAC::HMAC - -type HashLen = 32 -HMAC = hmacBytes - -hmacBytes : {n, m} (64 >= width (8 * (64 + m)), - 64 >= width (8 * n), 32 >= width m, fin m, fin n) => - [n][8] -> [m][8] -> [32][8] -hmacBytes key msg = split (hmacSHA256 key msg) - +module Primitive::Symmetric::KDF::HKDF256 = Primitive::Symmetric::KDF::HKDF where + +import Primitive::Symmetric::MAC::HMAC + +type HashLen = 32 +HMAC = hmacBytes + +hmacBytes : {n, m} (64 >= width (8 * (64 + m)), + 64 > width (8 * n), 32 >= width m, fin m, fin n) => + [n][8] -> [m][8] -> [32][8] + hmacBytes key msg = split (hmacSHA256 key msg) From 179ba2b0545722a158315fdab7abaeb43c148985 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 23 Jan 2025 14:06:51 -0500 Subject: [PATCH 4/7] sha2: rename version that reveals internals #122 --- Primitive/Keyless/Hash/HMAC.cry | 2 +- .../Keyless/Hash/SHA2Imperative/SHA224.cry | 34 -------------- .../Keyless/Hash/SHA2Imperative/SHA512.cry | 47 ------------------- .../Hash/SHA2Imperative/SHA512_224.cry | 47 ------------------- .../Hash/SHA2Imperative/SHA512_256.cry | 47 ------------------- .../{SHA2Imperative => SHA2Internal}/SHA.cry | 2 +- .../SHA256.cry | 2 +- .../SHA384.cry | 2 +- Primitive/Symmetric/Cipher/Block/SHACAL.cry | 2 +- 9 files changed, 5 insertions(+), 180 deletions(-) delete mode 100644 Primitive/Keyless/Hash/SHA2Imperative/SHA224.cry delete mode 100644 Primitive/Keyless/Hash/SHA2Imperative/SHA512.cry delete mode 100644 Primitive/Keyless/Hash/SHA2Imperative/SHA512_224.cry delete mode 100644 Primitive/Keyless/Hash/SHA2Imperative/SHA512_256.cry rename Primitive/Keyless/Hash/{SHA2Imperative => SHA2Internal}/SHA.cry (99%) rename Primitive/Keyless/Hash/{SHA2Imperative => SHA2Internal}/SHA256.cry (92%) rename Primitive/Keyless/Hash/{SHA2Imperative => SHA2Internal}/SHA384.cry (95%) diff --git a/Primitive/Keyless/Hash/HMAC.cry b/Primitive/Keyless/Hash/HMAC.cry index ae7a6617..78a3d749 100644 --- a/Primitive/Keyless/Hash/HMAC.cry +++ b/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] diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA224.cry b/Primitive/Keyless/Hash/SHA2Imperative/SHA224.cry deleted file mode 100644 index adf77f18..00000000 --- a/Primitive/Keyless/Hash/SHA2Imperative/SHA224.cry +++ /dev/null @@ -1,34 +0,0 @@ -/* - @copyright Galois Inc. 2018 - @author Sean Weaver - @editor Sam Breese - www.cryptol.net -*/ - -module Primitive::Keyless::Hash::SHA2Imperative::SHA224 = Primitive::Keyless::Hash::SHA2Imperative::SHA where - -type wp = 32 - -type digest_size = 224 - -type j = 64 - -H0 = [ 0xc1059ed8, 0x367cd507, 0x3070dd17, 0xf70e5939, - 0xffc00b31, 0x68581511, 0x64f98fa7, 0xbefa4fa4] - -K = [ 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5, - 0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174, - 0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da, - 0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967, - 0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85, - 0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070, - 0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3, - 0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2] - -SIGMA_0 x = (x >>> 2) ^ (x >>> 13) ^ (x >>> 22) - -SIGMA_1 x = (x >>> 6) ^ (x >>> 11) ^ (x >>> 25) - -sigma_0 x = (x >>> 7) ^ (x >>> 18) ^ (x >> 3) - -sigma_1 x = (x >>> 17) ^ (x >>> 19) ^ (x >> 10) \ No newline at end of file diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA512.cry b/Primitive/Keyless/Hash/SHA2Imperative/SHA512.cry deleted file mode 100644 index 7f5dd8ff..00000000 --- a/Primitive/Keyless/Hash/SHA2Imperative/SHA512.cry +++ /dev/null @@ -1,47 +0,0 @@ -/* - @copyright Galois Inc. 2018 - @author Sean Weaver - @editor Sam Breese - www.cryptol.net -*/ - -module Primitive::Keyless::Hash::SHA2Imperative::SHA512 = Primitive::Keyless::Hash::SHA2Imperative::SHA where - -type wp = 64 - -type digest_size = 512 - -type j = 80 - -H0 = [ 0x6a09e667f3bcc908, 0xbb67ae8584caa73b, 0x3c6ef372fe94f82b, 0xa54ff53a5f1d36f1, - 0x510e527fade682d1, 0x9b05688c2b3e6c1f, 0x1f83d9abfb41bd6b, 0x5be0cd19137e2179] - -K = [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc, - 0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118, - 0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2, - 0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694, - 0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65, - 0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5, - 0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4, - 0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70, - 0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df, - 0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b, - 0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30, - 0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8, - 0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8, - 0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3, - 0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec, - 0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b, - 0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178, - 0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b, - 0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c, - 0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817] - -SIGMA_0 x = (x >>> 28) ^ (x >>> 34) ^ (x >>> 39) - -SIGMA_1 x = (x >>> 14) ^ (x >>> 18) ^ (x >>> 41) - -sigma_0 x = (x >>> 1) ^ (x >>> 8) ^ (x >> 7) - -sigma_1 x = (x >>> 19) ^ (x >>> 61) ^ (x >> 6) - diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA512_224.cry b/Primitive/Keyless/Hash/SHA2Imperative/SHA512_224.cry deleted file mode 100644 index 6e26fe51..00000000 --- a/Primitive/Keyless/Hash/SHA2Imperative/SHA512_224.cry +++ /dev/null @@ -1,47 +0,0 @@ -/* - @copyright Galois Inc. 2018 - @author Sean Weaver - @editor Sam Breese - www.cryptol.net -*/ - -module Primitive::Keyless::Hash::SHA2Imperative::SHA512_224 = Primitive::Keyless::Hash::SHA2Imperative::SHA where - -type wp = 64 - -type digest_size = 224 - -type j = 80 - -H0 = [ 0x8c3d37c819544da2, 0x73e1996689dcd4d6, 0x1dfab7ae32ff9c82, 0x679dd514582f9fcf, - 0x0f6d2b697bd44da8, 0x77e36f7304c48942, 0x3f9d85a86a1d36c8, 0x1112e6ad91d692a1] - -K = [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc, - 0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118, - 0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2, - 0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694, - 0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65, - 0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5, - 0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4, - 0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70, - 0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df, - 0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b, - 0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30, - 0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8, - 0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8, - 0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3, - 0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec, - 0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b, - 0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178, - 0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b, - 0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c, - 0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817] - -SIGMA_0 x = (x >>> 28) ^ (x >>> 34) ^ (x >>> 39) - -SIGMA_1 x = (x >>> 14) ^ (x >>> 18) ^ (x >>> 41) - -sigma_0 x = (x >>> 1) ^ (x >>> 8) ^ (x >> 7) - -sigma_1 x = (x >>> 19) ^ (x >>> 61) ^ (x >> 6) - diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA512_256.cry b/Primitive/Keyless/Hash/SHA2Imperative/SHA512_256.cry deleted file mode 100644 index ff33291e..00000000 --- a/Primitive/Keyless/Hash/SHA2Imperative/SHA512_256.cry +++ /dev/null @@ -1,47 +0,0 @@ -/* - @copyright Galois Inc. 2018 - @author Sean Weaver - @editor Sam Breese - www.cryptol.net -*/ - -module Primitive::Keyless::Hash::SHA2Imperative::SHA512_256 = Primitive::Keyless::Hash::SHA2Imperative::SHA where - -type wp = 64 - -type digest_size = 256 - -type j = 80 - -H0 = [ 0x22312194fc2bf72c, 0x9f555fa3c84c64c2, 0x2393b86b6f53b151, 0x963877195940eabd, - 0x96283ee2a88effe3, 0xbe5e1e2553863992, 0x2b0199fc2c85b8aa, 0x0eb72ddc81c52ca2] - -K = [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc, - 0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118, - 0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2, - 0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694, - 0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65, - 0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5, - 0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4, - 0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70, - 0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df, - 0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b, - 0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30, - 0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8, - 0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8, - 0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3, - 0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec, - 0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b, - 0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178, - 0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b, - 0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c, - 0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817] - -SIGMA_0 x = (x >>> 28) ^ (x >>> 34) ^ (x >>> 39) - -SIGMA_1 x = (x >>> 14) ^ (x >>> 18) ^ (x >>> 41) - -sigma_0 x = (x >>> 1) ^ (x >>> 8) ^ (x >> 7) - -sigma_1 x = (x >>> 19) ^ (x >>> 61) ^ (x >> 6) - diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA.cry b/Primitive/Keyless/Hash/SHA2Internal/SHA.cry similarity index 99% rename from Primitive/Keyless/Hash/SHA2Imperative/SHA.cry rename to Primitive/Keyless/Hash/SHA2Internal/SHA.cry index 01f50e3e..3c0176a4 100644 --- a/Primitive/Keyless/Hash/SHA2Imperative/SHA.cry +++ b/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 diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA256.cry b/Primitive/Keyless/Hash/SHA2Internal/SHA256.cry similarity index 92% rename from Primitive/Keyless/Hash/SHA2Imperative/SHA256.cry rename to Primitive/Keyless/Hash/SHA2Internal/SHA256.cry index 6a95efcb..969af110 100644 --- a/Primitive/Keyless/Hash/SHA2Imperative/SHA256.cry +++ b/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 diff --git a/Primitive/Keyless/Hash/SHA2Imperative/SHA384.cry b/Primitive/Keyless/Hash/SHA2Internal/SHA384.cry similarity index 95% rename from Primitive/Keyless/Hash/SHA2Imperative/SHA384.cry rename to Primitive/Keyless/Hash/SHA2Internal/SHA384.cry index d572176b..138b286f 100644 --- a/Primitive/Keyless/Hash/SHA2Imperative/SHA384.cry +++ b/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 diff --git a/Primitive/Symmetric/Cipher/Block/SHACAL.cry b/Primitive/Symmetric/Cipher/Block/SHACAL.cry index 6d551318..e52e9812 100644 --- a/Primitive/Symmetric/Cipher/Block/SHACAL.cry +++ b/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**/ From a7236448450cffc22063d96a3bf34b7af65b8948 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 23 Jan 2025 14:49:52 -0500 Subject: [PATCH 5/7] sha2: add equivalence proof of sha2 versions #122 --- .../Keyless/Hash/SHA2Internal/Equivalence.cry | 52 +++++++++++++++++++ 1 file changed, 52 insertions(+) create mode 100644 Primitive/Keyless/Hash/SHA2Internal/Equivalence.cry diff --git a/Primitive/Keyless/Hash/SHA2Internal/Equivalence.cry b/Primitive/Keyless/Hash/SHA2Internal/Equivalence.cry new file mode 100644 index 00000000..f521a958 --- /dev/null +++ b/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 + */ +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 From 6dfaebce544e0a4aed1cd5cb26c73e8ebd47ef9a Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 23 Jan 2025 14:51:26 -0500 Subject: [PATCH 6/7] hash: update README for hash functions #122 --- Primitive/Keyless/Hash/README.md | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/Primitive/Keyless/Hash/README.md b/Primitive/Keyless/Hash/README.md index 099bd267..21424715 100644 --- a/Primitive/Keyless/Hash/README.md +++ b/Primitive/Keyless/Hash/README.md @@ -1 +1,16 @@ -Hash functions. + +This directory includes executable specifications for several hash functions. + +## 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. From 78a6cb559ef4e768e4e2aafb63507109ff6d6f60 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 23 Jan 2025 15:05:09 -0500 Subject: [PATCH 7/7] sha2: fix copyright notices, spacing, on deps #122 --- Primitive/Asymmetric/Signature/RSA_PSS.cry | 24 +++++++++++----------- Primitive/Symmetric/KDF/HKDF.md | 4 ++++ Primitive/Symmetric/KDF/HKDF256.cry | 6 +++++- 3 files changed, 21 insertions(+), 13 deletions(-) diff --git a/Primitive/Asymmetric/Signature/RSA_PSS.cry b/Primitive/Asymmetric/Signature/RSA_PSS.cry index be12d668..d6a287b3 100644 --- a/Primitive/Asymmetric/Signature/RSA_PSS.cry +++ b/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 diff --git a/Primitive/Symmetric/KDF/HKDF.md b/Primitive/Symmetric/KDF/HKDF.md index 94492d60..4c0ab2d1 100644 --- a/Primitive/Symmetric/KDF/HKDF.md +++ b/Primitive/Symmetric/KDF/HKDF.md @@ -1,3 +1,7 @@ + # HMAC-based Extract-and-Expand Key Derivation Function (HKDF) ## Welcome diff --git a/Primitive/Symmetric/KDF/HKDF256.cry b/Primitive/Symmetric/KDF/HKDF256.cry index 7b50d9f4..724cc09b 100644 --- a/Primitive/Symmetric/KDF/HKDF256.cry +++ b/Primitive/Symmetric/KDF/HKDF256.cry @@ -1,3 +1,7 @@ +/** + * @copyright Galois, Inc + * @author Aaron Tomb + */ module Primitive::Symmetric::KDF::HKDF256 = Primitive::Symmetric::KDF::HKDF where import Primitive::Symmetric::MAC::HMAC @@ -8,4 +12,4 @@ HMAC = hmacBytes hmacBytes : {n, m} (64 >= width (8 * (64 + m)), 64 > width (8 * n), 32 >= width m, fin m, fin n) => [n][8] -> [m][8] -> [32][8] - hmacBytes key msg = split (hmacSHA256 key msg) +hmacBytes key msg = split (hmacSHA256 key msg)