From c514ca2347beb2a71c5ca717d21566a5a1f856d5 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Fri, 6 Sep 2024 14:26:02 -0400 Subject: [PATCH] sha3: add copyright notices #132 --- .../Asymmetric/Signature/DSA/p2048_q224.cry | 7 ++ Primitive/Keyless/Hash/SHA3/SHA3.cry | 20 ++++++ Primitive/Keyless/Hash/SHA3/SHA3_224.cry | 17 +++-- Primitive/Keyless/Hash/SHA3/SHA3_256.cry | 13 ++-- Primitive/Keyless/Hash/SHA3/SHA3_384.cry | 15 ++-- Primitive/Keyless/Hash/SHA3/SHA3_512.cry | 14 ++-- Primitive/Keyless/Hash/SHA3/Tests.cry | 71 +++++++++++++++++-- Primitive/Keyless/Hash/SHAKE/SHAKE128.cry | 22 ++++++ Primitive/Keyless/Hash/SHAKE/SHAKE256.cry | 26 ++++++- 9 files changed, 171 insertions(+), 34 deletions(-) diff --git a/Primitive/Asymmetric/Signature/DSA/p2048_q224.cry b/Primitive/Asymmetric/Signature/DSA/p2048_q224.cry index bcccea95..899fc0b8 100644 --- a/Primitive/Asymmetric/Signature/DSA/p2048_q224.cry +++ b/Primitive/Asymmetric/Signature/DSA/p2048_q224.cry @@ -1,3 +1,10 @@ +/* + * DSA instantiated with SHA-1 and SHA-3. + * + * @copyright Galois, Inc + * @author Ajay Kumar Eeralla + * + */ module Primitive::Asymmetric::Signature::DSA::p2048_q224= Primitive::Asymmetric::Signature::DSA::DSA where import Common::utils diff --git a/Primitive/Keyless/Hash/SHA3/SHA3.cry b/Primitive/Keyless/Hash/SHA3/SHA3.cry index 7dc4e251..0ad5999b 100644 --- a/Primitive/Keyless/Hash/SHA3/SHA3.cry +++ b/Primitive/Keyless/Hash/SHA3/SHA3.cry @@ -1,3 +1,16 @@ +/* + * SHA-3 hash function, as specified in [FIPS-202]. + * + * [FIPS-202]: National Institute of Standards and Technology. SHA-3 Standard: + * Permutation-Based Hash and Extendable-Output Functions. (Department of + * Commerce, Washington, D.C.), Federal Information Processing Standards + * Publication (FIPS) NIST FIPS 202. August 2015. + * @see https://dx.doi.org/10.6028/NIST.FIPS.202 + * + * @copyright Galois, Inc. + * @author Ajay Kumar Eeralla + * @editor Marcella Hastings + */ module Primitive::Keyless::Hash::SHA3::SHA3 where import Primitive::Keyless::Hash::keccak where type b = 1600 @@ -8,5 +21,12 @@ parameter type digest : # type constraint (fin digest, digest >= 224, digest <= 512) +/** + * SHA-3 hash function specification. + * [FIPS-202] Section 6.1. + * + * Note that the specification of `c` is above, in the instantiation of the + * `keccak` module. + */ sha3 : {n} (fin n) => [n] -> [digest] sha3 M = Keccak`{d=digest} (M # 0b01) diff --git a/Primitive/Keyless/Hash/SHA3/SHA3_224.cry b/Primitive/Keyless/Hash/SHA3/SHA3_224.cry index 725f1ae1..b74923bb 100644 --- a/Primitive/Keyless/Hash/SHA3/SHA3_224.cry +++ b/Primitive/Keyless/Hash/SHA3/SHA3_224.cry @@ -1,10 +1,9 @@ +/** + * Instantiation of SHA3-224. + * + * @copyright Galois Inc. + * @author Ajay Kumar Eeralla + */ module Primitive::Keyless::Hash::SHA3::SHA3_224 = - Primitive::Keyless::Hash::SHA3::SHA3 -where - -type digest = 224 - - - - - + Primitive::Keyless::Hash::SHA3::SHA3 where + type digest = 224 diff --git a/Primitive/Keyless/Hash/SHA3/SHA3_256.cry b/Primitive/Keyless/Hash/SHA3/SHA3_256.cry index 28158541..75693afb 100644 --- a/Primitive/Keyless/Hash/SHA3/SHA3_256.cry +++ b/Primitive/Keyless/Hash/SHA3/SHA3_256.cry @@ -1,6 +1,9 @@ +/** + * Instantiation of SHA3-256. + * + * @copyright Galois Inc. + * @author Ajay Kumar Eeralla + */ module Primitive::Keyless::Hash::SHA3::SHA3_256 = - Primitive::Keyless::Hash::SHA3::SHA3 -where - type digest = 256 - - + Primitive::Keyless::Hash::SHA3::SHA3 where + type digest = 256 diff --git a/Primitive/Keyless/Hash/SHA3/SHA3_384.cry b/Primitive/Keyless/Hash/SHA3/SHA3_384.cry index fffb5bd2..05f2b5ca 100644 --- a/Primitive/Keyless/Hash/SHA3/SHA3_384.cry +++ b/Primitive/Keyless/Hash/SHA3/SHA3_384.cry @@ -1,8 +1,9 @@ +/** + * Instantiation of SHA3-384. + * + * @copyright Galois Inc. + * @author Ajay Kumar Eeralla + */ module Primitive::Keyless::Hash::SHA3::SHA3_384 = - Primitive::Keyless::Hash::SHA3::SHA3 -where - -type digest = 384 - - - + Primitive::Keyless::Hash::SHA3::SHA3 where + type digest = 384 diff --git a/Primitive/Keyless/Hash/SHA3/SHA3_512.cry b/Primitive/Keyless/Hash/SHA3/SHA3_512.cry index d836e9a2..4c062802 100644 --- a/Primitive/Keyless/Hash/SHA3/SHA3_512.cry +++ b/Primitive/Keyless/Hash/SHA3/SHA3_512.cry @@ -1,7 +1,9 @@ +/** + * Instantiation of SHA3-512. + * + * @copyright Galois Inc. + * @author Ajay Kumar Eeralla + */ module Primitive::Keyless::Hash::SHA3::SHA3_512 = - Primitive::Keyless::Hash::SHA3::SHA3 - where - -type digest = 512 - - + Primitive::Keyless::Hash::SHA3::SHA3 where + type digest = 512 diff --git a/Primitive/Keyless/Hash/SHA3/Tests.cry b/Primitive/Keyless/Hash/SHA3/Tests.cry index 2de1dfcc..8347531d 100644 --- a/Primitive/Keyless/Hash/SHA3/Tests.cry +++ b/Primitive/Keyless/Hash/SHA3/Tests.cry @@ -1,26 +1,54 @@ +/* + * Tests of the SHA3 hash functions. + * + * Test vectors drawn from the NIST Cryptographic Standards and Guidelines + * example values. + * https://csrc.nist.gov/projects/cryptographic-standards-and-guidelines/example-values + * + * @copyright Galois Inc. + * @author Ajay Kumar Eeralla + * @editor Iavor Diatchki + * @editor Marcella Hastings + */ module Primitive::Keyless::Hash::SHA3::Tests where import Primitive::Keyless::Hash::utils -// Test vectors from -// https://csrc.nist.gov/projects/cryptographic-standards-and-guidelines/example-values#aHashing - - submodule SHA3_224 where import Primitive::Keyless::Hash::SHA3::SHA3_224 + /* + * ```repl + * :prove t1 + * ``` + */ property t1 = join (toBytes (sha3 [])) == 0x6b4e03423667dbb73b6e15454f0eb1abd4597f9a1b078e3f5b5a6bc7 + /* + * ```repl + * :prove t2 + * ``` + */ property t2 = join (toBytes (sha3 0b11001)) == 0xffbad5da96bad71789330206dc6768ecaeb1b32dca6b3301489674ab msg1600 : [1600] msg1600 = join [ 0b11000101 | _ <- zero : [200] ] + /* + * ```repl + * :prove t3 + * ``` + */ property t3 = join (toBytes (sha3 msg1600)) == 0x9376816aba503f72f96ce7eb65ac095deee3be4bf9bbc2a1cb7e11e0 + /* + * ```repl + * :prove t4 + * ``` + */ property t4 = join (toBytes (sha3 (msg1600 # 0b11000))) == 0x22d2f7bb0b173fd8c19686f9173166e3ee62738047d7eadd69efb228 @@ -28,12 +56,27 @@ submodule SHA3_224 where submodule SHA3_256 where import Primitive::Keyless::Hash::SHA3::SHA3_256 + /* + * ```repl + * :prove t1 + * ``` + */ property t1 = join (toBytes (sha3 [])) == 0xa7ffc6f8bf1ed76651c14756a061d662f580ff4de43b49fa82d80a4b80f8434a + /* + * ```repl + * :prove t2 + * ``` + */ property t2 = join (toBytes (sha3 0b11001)) == 0x7b0047cf5a456882363cbf0fb05322cf65f4b7059a46365e830132e3b5d957af + /* + * ```repl + * :prove t3 + * ``` + */ property t3 = join (toBytes (sha3 0b110010100001101011011110100110)) == 0xc8242fef409e5ae9d1f1c857ae4dc624b92b19809f62aa8c07411c54a078b1d0 @@ -41,9 +84,19 @@ submodule SHA3_256 where submodule SHA3_384 where import Primitive::Keyless::Hash::SHA3::SHA3_384 + /* + * ```repl + * :prove t1 + * ``` + */ property t1 = join (toBytes (sha3 [])) == 0x0c63a75b845e4f7d01107d852e4c2485c51a50aaaa94fc61995e71bbee983a2ac3713831264adb47fb6bd1e058d5f004 + /* + * ```repl + * :prove t2 + * ``` + */ property t2 = join (toBytes (sha3 0b11001)) == 0x737c9b491885e9bf7428e792741a7bf8dca9653471c3e148473f2c236b6a0a6455eb1dce9f779b4b6b237fef171b1c64 @@ -51,9 +104,19 @@ submodule SHA3_384 where submodule SHA3_512 where import Primitive::Keyless::Hash::SHA3::SHA3_512 + /* + * ```repl + * :prove t1 + * ``` + */ property t1 = join (toBytes (sha3 [])) == 0xa69f73cca23a9ac5c8b567dc185a756e97c982164fe25859e0d1dcc1475c80a615b2123af1f5f94c11e3e9402c3ac558f500199d95b6d3e301758586281dcd26 + /* + * ```repl + * :prove t2 + * ``` + */ property t2 = join (toBytes (sha3 0b11001)) == 0xa13e01494114c09800622a70288c432121ce70039d753cadd2e006e4d961cb27544c1481e5814bdceb53be6733d5e099795e5e81918addb058e22a9f24883f37 diff --git a/Primitive/Keyless/Hash/SHAKE/SHAKE128.cry b/Primitive/Keyless/Hash/SHAKE/SHAKE128.cry index df3ced77..e11d45a1 100644 --- a/Primitive/Keyless/Hash/SHAKE/SHAKE128.cry +++ b/Primitive/Keyless/Hash/SHAKE/SHAKE128.cry @@ -1,3 +1,18 @@ +/* + * Instantiation of SHAKE128, a SHA-3 extendable-output function, as specified + * in [FIPS-202]. + * + * [FIPS-202]: National Institute of Standards and Technology. SHA-3 Standard: + * Permutation-Based Hash and Extendable-Output Functions. (Department of + * Commerce, Washington, D.C.), Federal Information Processing Standards + * Publication (FIPS) NIST FIPS 202. August 2015. + * @see https://dx.doi.org/10.6028/NIST.FIPS.202 + * + * @copyright Galois, Inc. + * @author Ajay Kumar Eeralla + * @editor Marcella Hastings + * + */ module Primitive::Keyless::Hash::SHAKE::SHAKE128 where import Primitive::Keyless::Hash::keccak where type b = 1600 @@ -7,6 +22,13 @@ import Primitive::Keyless::Hash::keccak where type c = 256 import Primitive::Keyless::Hash::utils (toBytes) +/** + * SHAKE128 extendable-output function. + * [FIPS-202] Section 6.2. + * + * Note that the specification of `c` is above, in the instantiation of the + * `keccak` module. + */ shake128 : {m, d} (fin m, fin d) => [m] -> [d] shake128 M = Keccak (M # 0b1111) diff --git a/Primitive/Keyless/Hash/SHAKE/SHAKE256.cry b/Primitive/Keyless/Hash/SHAKE/SHAKE256.cry index e777df6e..ca8cb381 100644 --- a/Primitive/Keyless/Hash/SHAKE/SHAKE256.cry +++ b/Primitive/Keyless/Hash/SHAKE/SHAKE256.cry @@ -1,3 +1,18 @@ +/* + * Instantiation of SHAKE256, a SHA-3 extendable-output function, as specified + * in [FIPS-202]. + * + * [FIPS-202]: National Institute of Standards and Technology. SHA-3 Standard: + * Permutation-Based Hash and Extendable-Output Functions. (Department of + * Commerce, Washington, D.C.), Federal Information Processing Standards + * Publication (FIPS) NIST FIPS 202. August 2015. + * @see https://dx.doi.org/10.6028/NIST.FIPS.202 + * + * @copyright Galois, Inc. + * @author Ajay Kumar Eeralla + * @editor Marcella Hastings + * + */ module Primitive::Keyless::Hash::SHAKE::SHAKE256 where import Primitive::Keyless::Hash::keccak where type b = 1600 @@ -7,8 +22,13 @@ import Primitive::Keyless::Hash::keccak where type c = 512 import Primitive::Keyless::Hash::utils (toBytes) -type secBits = 256 - +/** + * SHAKE256 extendable-output function. + * [FIPS-202] Section 6.2. + * + * Note that the specification of `c` is above, in the instantiation of the + * `keccak` module. + */ shake256: {m, d} (fin m, fin d) => [m] -> [d] shake256 M = Keccak (M # 0b1111) @@ -62,4 +82,4 @@ property k8 = join (toBytes (shake256 (reverse 0b110))) == expected_result where 0xbddbe2cbd3a9a3ba3914da88e5853e70, 0x83630e6d51d7a009017d8176c3067329, 0xbec8e5f65591d65c5894c40132f1a2ab - ] + ]