From 7be54599c5658c8502d1f5a978db5fcd9bd7dd49 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Fri, 13 Dec 2024 17:13:20 -0500 Subject: [PATCH 1/6] mldsa: add keygen_internal #192 Much is correct except something on steps 5-6. The values t0 and t1 are incorrect. --- .../Signature/ML_DSA/Specification.cry | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry b/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry index de739df..3a9ee5a 100644 --- a/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry +++ b/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry @@ -278,6 +278,28 @@ type d = 13 */ type β = η * τ + +KeyGen_internal : [32]Byte -> (PublicKey, PrivateKey) +KeyGen_internal ξ = (pk, sk) where + (ρ # ρ' # K) = H`{128} (ξ # IntegerToBytes`{1} `k # IntegerToBytes`{1} `ell) + + A_hat = ExpandA ρ + + (s1, s2) = ExpandS ρ' + + // An element of `R` may be "typecast" to an element of `Rq`. [FIPS-204] Section 2.4.1. + s1' = [map fromInteger s1_i | s1_i <- s1] + s2' = [map fromInteger s2_i | s2_i <- s2] + + t = NTTInv_Vec (A_hat ∘∘ NTT_Vec s1') + s2' + (t1, t0) = Power2Round t + + pk = pkEncode ρ t1 + + tr = H`{64} pk + + sk = skEncode ρ K tr s1 s2 t0 + /** * Compute a base-2 representation of the input mod `2^α` using little-endian * order. From 7a13eed269f034527e8fd5e35adbbe0a841d385b Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 19 Dec 2024 14:42:07 -0500 Subject: [PATCH 2/6] mldsa: make NTT bitreversed #192 --- .../Signature/ML_DSA/Specification.cry | 20 +++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry b/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry index 3a9ee5a..f34de9c 100644 --- a/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry +++ b/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry @@ -1231,6 +1231,9 @@ private * that [NTT-Guide] uses different notation: their `ψ` is our `ζ`; their `a` * is our `f`; and we set their `n = 256`. * + * There is one divergence between [NTT-Guide] and [FIPS-204]: the spec uses + * bit-reversed indexes for the NTT representation, but the guide does not. + * * @design Marcella Hastings : This is neither efficient * nor obviously spec-adherent. We should aim to make it at least one of those. * Ideally we will consolidate all the NTT implementations across the cryptol- @@ -1239,9 +1242,13 @@ private * @see https://github.com/GaloisInc/cryptol-specs/issues/163 */ NTT : Rq -> Tq -NTT f = [f_hat_j j | j <- [0..255]] where +NTT f = [f_hat_j j | j <- bitrev_indexes] where f_hat_j j = sum [ (ζ ^^ (2 * i * j + i)) * fi | i <- [0..255] | fi <- f] + // Rearrange the indexes so that the NTT representation is in + // bit-reversed-index order. + bitrev_indexes = map toInteger (map reverse [0..255 : [8]]) + /** * Inverse of the number theoretic transform: converts from the "NTT * representation" in `T_q` to a polynomial in `R_q`. @@ -1252,6 +1259,9 @@ NTT f = [f_hat_j j | j <- [0..255]] where * that [NTT-Guide] uses different notation: their `ψ` is our `ζ`; their `a` * is our `f`; and we set their `n = 256`. * + * There is one divergence between [NTT-Guide] and [FIPS-204]: the spec uses + * bit-reversed indexes for the NTT representation, but the guide does not. + * * @design Marcella Hastings : This is neither efficient * nor obviously spec-adherent. We should aim to make it at least one of those. * Ideally we will consolidate all the NTT implementations across the cryptol- @@ -1263,7 +1273,13 @@ NTTInv : Tq -> Rq NTTInv f_hat = [f_i j * inv_root | j <- [0..255]] where inv_root = recip 256 : Z q inv_ζ = recip ζ - f_i j = sum [ (inv_ζ ^^ (2 * i * j + j)) * f_hat_j | i <- [0..255] | f_hat_j <- f_hat] + f_i j = sum [ (inv_ζ ^^ (2 * i * j + j)) * f_hat_j + | i <- [0..255] + | f_hat_j <- indexReversedFHat] + + // Rearrange the NTT representation to bit-reverse the indexes. + bitrev_indexes = map reverse [0..255 : [8]] + indexReversedFHat = [f_hat@i | i <- bitrev_indexes] private /** From ac70d7b6bec551ec75ba83cb435b9c2a2674782b Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Mon, 23 Dec 2024 16:35:02 -0500 Subject: [PATCH 3/6] mldsa: fix sloppy naming bug #192 --- Primitive/Asymmetric/Signature/ML_DSA/Specification.cry | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry b/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry index f34de9c..39c8fba 100644 --- a/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry +++ b/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry @@ -130,7 +130,7 @@ property modPlusMinusWorks m = inRange && congruent where * names, we define the following functions. */ NTT_Vec = map NTT -NTTInv_Vec = map NTT +NTTInv_Vec = map NTTInv /** * Wrapper function around SHAKE256, specifying the length `l` in bytes. From 59882dd589369e5af0ce418bcc483e0ef2e6e27f Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Mon, 23 Dec 2024 17:08:58 -0500 Subject: [PATCH 4/6] mldsa: Add KAT for KeyGen #192 --- .../Signature/ML_DSA/Tests/ML_DSA_44.cry | 243 ++++++++++++++++++ 1 file changed, 243 insertions(+) create mode 100644 Primitive/Asymmetric/Signature/ML_DSA/Tests/ML_DSA_44.cry diff --git a/Primitive/Asymmetric/Signature/ML_DSA/Tests/ML_DSA_44.cry b/Primitive/Asymmetric/Signature/ML_DSA/Tests/ML_DSA_44.cry new file mode 100644 index 0000000..ed90353 --- /dev/null +++ b/Primitive/Asymmetric/Signature/ML_DSA/Tests/ML_DSA_44.cry @@ -0,0 +1,243 @@ +/** + * Known answer tests for ML_DSA_44. + * + * These can be drawn from several trusted sources, including + * [PQC-KAT]: Kris Kwiatkowski and Roderick Chapman. Post-quantum-cryptography. + * GitHub repo "KAT". + * @see https://github.com/post-quantum-cryptography/KAT + * [ACVP]: NIST. usnistgov. GitHub repo "ACVP-Server". + * @see https://github.com/usnistgov/ACVP-Server/tree/master/gen-val/json-files/ML-DSA-keyGen-FIPS204 + */ +import Primitive::Asymmetric::Signature::ML_DSA::Instantiations::ML_DSA_44 as ML_DSA + +/** + * Test function for running a KAT from [PQC-KAT] in the "deterministic, raw" + * category. + * + * "Deterministic" categorizes how the signing seeds `ρ'` are computed. + * "Raw" categorizes the set of functions being tested -- in this case, the + * `{KeyGen, Sign, Verify}_internal` functions. See [PQC-KAT] README.md for + * more details. + */ +tryDetKAT xi expected_pk expected_sk = keygenWorks where + (pk, sk) = ML_DSA::KeyGen_internal xi + keygenWorks = (pk == expected_pk) && (sk == expected_sk) + +/** + * Test the raw, deterministic KAT with count 0. + * ```repl + * :prove det0 + * ``` + */ +property det0 = tryDetKAT xi pk sk where + xi = split 0xf696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68 + seed = join [ + 0x23f1c88bd0e65f2c891ce865bd3275a7ffdbe4f9036e75b9, + 0x6aad0412650e9cd2ea4591d4ab7131ea971b34c23a4ed245 + ] + pk = split (join [ + 0xbd4e96f9a038ab5e36214fe69c0b1cb835ef9d7c8417e76aecd152f5cddebec8, + 0xa1ac25f03b3643700dbf76eef49a324f93d5042e203f3c70658ad1ad13b917cc, + 0x1ed23f06a4dd1c543350525a9e2451dfe5f3969b1fa530488cc8903fdeb7718d, + 0x123b17843f82a838976c6596f4b18e7b1f15ab3c526b90118506f33338d539cb, + 0x77021f0ea75d424a7d90a9b689d3ffcec54e47d9f2d06f606d35868ee4fc3a03, + 0x8c29e1496592715ea8fb7a8a5e5340d8ba8ac8d81ee38f78161879a0564ded36, + 0x899e88f6be522e5463810dcdad14a9ec1a9994b1cd74601aefd31c9d3d009653, + 0xcfb8233c06d89b4c0d8c2560f8f6bbf2b8cdf37483710b87206fcb16f7b54720, + 0x33c6e9fcd81e05c284c168b82899532782dbf7897aecf7033e85512237371271, + 0x330ad1b29f613a5de56d54d5d78f50a41725601daaea33ad0bbd8fcb77ad6342, + 0xdf6c2890688bccea1c7d9d92c7c57a5c2196b346718381bc00072a62f8ebc31e, + 0x6d3bdd99d55d80e17d21163b61406ad4eaa70927e4fa74add922624d964725f1, + 0x1c9b7b52a5f9e3a6ec36e1f17d0ea61baf68ed8c04851a1a82730d39da1ad2e6, + 0x9e38288f55c13f75fc65dec5af6634ade84ee77459453a126f5a5902a806903c, + 0x7914fbfb25515be9e57aebb8ca258d281e1a06109d85ea687de74a40f14235bd, + 0x4d7541c05096800c47ad4d7f1554817c962d23840050c3f1c12966e586bcb6e7, + 0x1659168d96e6610ca391970581979aa40e6247b5c1661042468fa50e20e0435c, + 0x7e7159b12fb3ec2d06dba6aa40030531f48071f645f7838d9faef5ed83ec5676, + 0xcd4f5aa25e095cecceabc2df851488a5188ef9ef47b75ea42795d73b63800796, + 0x331688fbf6e0c2fc0a6193c729209e013af51d52d1805b5ef72dda8e7827d38d, + 0x92a70c4e09f6b0223dbc3e55c15ddb6aa5650d62078cfb6fe30668dd0c283ff3, + 0x20c75cc595ea043d063562058e2d5b80d0ec8830f4f0065acda05b4a132ffc6a, + 0x06ee439a62de3c46bd6526f7d788c2e0ed47da1081db163d58624ca8702c5568, + 0x07e721224b060702e7d7c49b339bfda25a631cc65a0185bf17f32fc444347bbb, + 0x5a43ec1e934aaae874a2dcfa1e1371d61f0b6a7b24b8eaf25a9e02f8fa38d959, + 0x6db39b5d8d4d245469de1eef739200c9309a01346268db557f18ee192640a57f, + 0x764304e4e0ca56d4cb3dc16be0ace079d6dd6c27d9b0c76a122614b6f423d586, + 0xae5bd1a8437b7efd0d69f2890de5d17252512d4c83a1b612217b15f594c7ff1c, + 0xa5aa13fa8abe19300085d807c7acb4caa80db574fa450684fe643581dbc7901f, + 0xc564d1d7d4d2b3a8956577100ed62b3804589aa7c30b27060b57586ae9563289, + 0x9fc81a6349ea674938db8facb975bbda16f185c5f5d8d3230d9d60a62fa0a258, + 0x5f95a6b26d6b3f3ed2555ef2e88e1488508499d6191f2cf05ad22ae44efb958a, + 0x6c0d172f25732636224f3b855158999ed5e8467ff7ec0c96666798a47aae92dd, + 0x55e209895d4e9defa1ef257ba07e290433f2deff707948b38b53c34be66becd9, + 0x0327f0894e42bab1033391a365295cdadb7c99fd0e0a4fe22efec6cf2df80895, + 0xa98b65b2aa03e7cd05918446165b177652dd5baf1e293c940c07bb620b4a99fe, + 0x98b1a42501181e66f161864758dd146c70e018793351dead59d9347b4e524367, + 0xb11c8d12d83682a922360c46fc524a5ecdd6aa3ee54c56cd6db930e5283d3009, + 0xc8d2541811d262d35513c22569ea1198ebb9353d6d26ef3417be145358adf63f, + 0xf243858a98bf53554a7ed4469ca8b09a76aec882db0c358e76da955ee26dbe17, + 0xdaf57a3a46aa208deaa1ce352dcb09c27067cabd233d5a251ccdc1ac077edb9c + ]) + sk = split (join [ + 0xbd4e96f9a038ab5e36214fe69c0b1cb835ef9d7c8417e76aecd152f5cddebec8, + 0xe9355a9ab1bcfbfc7d4decdf5ddd94b4359823a9578a19d161c4e9ad5afd7d61, + 0x746119a59589b3630773bfd350c45d029f1cd0b03163feac00f77d814cb89d96, + 0x3b11a8dfad7d0f31b0a542ba61044a2968d6cc435f00f5330f65063f5a46db23, + 0x23b1691c044d0cb28c2487014a9230dab8510802115848401928228a46881907, + 0x0c5c002a0b18109b3632493810c404428498048444259a323024a4259c062cd9, + 0x344454000018c58d64142113888020400c02a220811484823685d2086010a540, + 0x52b231a4a48c64000c11048522868954c609cab6845346898b101122038044b0, + 0x915ca00952a2288bb488612880120580c948668124925906429b280ed1300501, + 0x9631dbb804e2c63011024ccb406549088e0a470d53c08919b8711091651a3112, + 0xca125080242e24134a22014c1c48100a274e03354801c0819098845908851489, + 0x115b400ee09885d93462c48440e4a8901b418d444031d0b420008665a2b60464, + 0x964d4b1802a130660a020ee4862dd2162a9c186103220c5b3228980445d93465, + 0xcb18521b11444c8084124470dca201920851100912a4880c109708c2b0290ac0, + 0x48e2260cdb344d9b226e030951149160c0042a1819884202665802321a366ed3, + 0x127298b82914034d90b200a1c6841c121102c6015004525842685a160c032046, + 0x03a40d04480c52426821271291902cd92489cb088de30481a18270c1b8280848, + 0x310c499023079049b04c883422118009138225189204c240061ac18422b270e3, + 0x36904bc60081b83152a04923c3215206318b2605cc306a581626641080532272, + 0x89348cc1288c1a118a98406008098dc9246ee4840054140e4ba00543826da018, + 0x8d03922d10852519072c6440908a107064c66c51308219b56122b420540866d4, + 0x1641089828c3160a60286841002e492206502205ca262ddc380582203004c165, + 0x62a660da0620098510888844e1c011432466c394711c47324c28125904625b80, + 0x49db40211915490b3184e1206600c588c4264542c871c4263120050549127049, + 0xb66dd4b66884c830c44406c1826123874dc9127018116e8b10915c0291cb8485, + 0xd032620a8160423820c91820003544982886020331c120818030280c0551cc86, + 0x890022065c388e24264da42888188701c2c06dd4368904b16404278ada448120, + 0xc128a4a80114350e530031624651d9126d0b88040b856904c96d429050808881, + 0x004b402ec8f9a63ad7db8f6c580a15254857376b862730d93f80c4976e1ef194, + 0x7efa8513adc92867a377e74969510fd7417fa21bd3d773f60d20e4b2ba56cc54, + 0xf7671e087c16d996c25ec97259cf8e0a4a5c823bcb4ee3ab5aa58ece39111e15, + 0x13c30cb90a6453d09d79e35e7bc77a3875efea5a2f0f8e070dd14cf4fcb75f13, + 0xd61ee24dbc6b9977fe0c44f17166b06d4e2425524e4ee455ced586033641c2c8, + 0xba5e9c0a8317ab418233d9ee411ef2bb013bb1d4b12d1ef8a82bc591218c3e5f, + 0x7ffeb2f7b95a643b8cc46e49fdbb83656be0167b0afd3ae9205c1b02694f7df9, + 0x39eea45529189cd8c6ac518cdfdd0e7d0a04e521ad366d99b65b9f389dc774b1, + 0x5168907fba80ad2e6f540f8c36d81407f12d3dbb83ba0ef403a9db8453374c2b, + 0x65aa76fb31ce475f4a857e4d155e929a77086dd169c0657c9306465910dc1596, + 0x6a9cde2923d9c36ecf9a82fb6ce8ad6e3362f2dfe4a6b6ff54ef1bda398d3ae0, + 0x32590e81923b1c5b287ef18e6d480f06d4f57552c6c74e329eb7f1326f663893, + 0x5afc9a87d08147f6a3c081dbe4b7660d3bf7cc2a86bfb22cdc2a3932ecd9b20f, + 0x770088c5d4a409950c3d91b5c0a87017f394af3d26d083986355553b98757202, + 0x04e03eb2a8a1abc9f486ad1956717ed7d12a11a34b30b69eb3945f575f16f783, + 0xe395bc63d757e0ee19e57e0fe999edc75c8ceb7d3753a1172e31255f383371a2, + 0x3e9914d373278d8437aa45c6cf55c188a7559659742fccf775150f8290e7faa6, + 0x9dbe48b09960db647c9a58c87668b534d0a3f621a7054aa67dd8e5ec09fef842, + 0xad1629d9f85462c9461afe770926bcf939769f939e8c35f61e4300a4db286463, + 0xbf34eef5f4282d6b0b18be8d8eebae6863f3eaf0b0adaf8468d7264e44af2652, + 0x216291ede5689f9a153e886486cdc5538ecbe575926c362f2c0c2ac473c144f9, + 0xe7ccb620cee886df07fbfd812ec65f19f8d3bca0de9c999733973b3f42b354ca, + 0xc27cdbcb39c0988f9aedbfa3f0f772306c51260810ed526aa061ed7df06d1f90, + 0x50c8efbc872e71ba80b8266b5b3da89c6a6adce973945cf6a8c25af71247bc35, + 0x6b92b35ba82d9cdfa189d5f1c60fece7246cddad8e3856ecf048487dc5c05cf0, + 0x47296b35b3d81ef889948e0a2fcd1210bb4511a5ce15a0a4d81b635b024fffcb, + 0x63c3f97ccbf418fb8ab815a565a82e8065d256bd803d5b176e86c46eaaf85066, + 0xe598f9ea2b7823c09c4dcdc281cc0593f2c45eafd439f067bb03712d5f2d0c44, + 0x07538d9f15873474e1aac69b8bbcc4bd7fa9cda8cb20e4a551b9598a41215ae2, + 0x2e0d04069bffe26f338b6dcf4e25c8a36a8fc79d8abb424e40ea6e56b8549de4, + 0xeca8c27151047953a5048d73d13bb718185cfcab1e85ea2ef8757306ff964c42, + 0x28a004d4aa709eddd54a11cf25ca6c1c6cd70dd7eb5f8721e9f0a7d8f4a71d85, + 0x9b31d421099b49c393ba3044254935aba5cc5222bef7cd7e7068cee47c416579, + 0x4e9c0d6f6416bb51476460c0e104cf883f482c97c2aa6ec3cfc5ce68eab2a06a, + 0x1b97024cb62b4ea046e07727c328b0eda1bbda3a7a635c64a4638f93fa3efbdf, + 0x757fbc9be9029bc132f296abc3b9a44224faf6bb1a3974763d81b0a1fb91472d, + 0xae04ec26ef7255e449ae6e628532b912d827ad44897ee7fee066ac6062e20cd5, + 0x9f5481751f2751ff2dc3e117b5059e5403fd61fb36083d7ee07d053e0c52a43e, + 0xcd1884a5c279364bd29f04856e92427b45cfc5b6c3d345725e0887a1b47c9f8d, + 0x8607bdb88bf0321d70cb33be6fe1c002865150aebdf3b9c5d1e004df937c565a, + 0x7d3883158615e7eb13decbd2dd89a04390475e1d214eb60b7ac7ee220e3f980d, + 0x1515247e0910b55a3cfab29142ebeea1e2eb8a420f33ecb1c25fa3d430ba2f47, + 0x13d4cbf5a71389f96caf42943a15de969cf972bface48699a57596076f8eceb7, + 0x6070174d39decd0bd5866116e1a67e57d61b6b1da5c4eb830c34bce3919cd70d, + 0x446da248169deacb42a5f14f4f0d12ff7575f1dd91cfcf8304b286aa4272ff32, + 0xdad6156b21c3ce56a28455c88ec4b5a8003a1baa074d6a38af77c07d29854e1e, + 0x7bcc6f5ef1948212831f93128b197e0383a3d2cb5ca528b16d35728fc63e41e6, + 0xc5b8730e4fe3905f7ceb914d5eb239fcdc0fbe6d9d3de141129a466d68ce2622, + 0x4aa997d36b2eb089fd653d9efe3ba91e0fa64d5b3e495fdfab2af2a4ca04dee4, + 0xc948b75cdc3fb6ec3afdf4901d53b96fae5c5a8f7fd97b4e38e09b11a41594a3, + 0x3b057a150dad19abc9f6541c30fcfdf73b97d10c641eb2b8c08cf2c3cb333ea3, + 0x07094ac5409babb3d42bba60cb4941cc63481122177421e07a99d4710f471569 + ]) + msg = 0x6dbbc4375136df3b07f7c70e639e223e + mlen = 16 + sm = join [ + 0xa8bb75e2f0902b5a2330d586ac172f8a09f66d9b83867b705dbb40c8d032df0e, + 0x56029a5b7a6701b50bd9f0c28a9d1cf0f64c2f3e01d6cbd7fd358c2de8d34de1, + 0x328693586ee45861b3142a80f9e2039bc53719bdead3ed17c760770c8c542154, + 0xc351f13a480f14d4e5683deb9990b6ca20a0093f28d5d9905863497b2ae319e4, + 0xd0d5621479a28c03e0c370837e1cd1827fec8e502c9c3b4e40bf82e7c4be1843, + 0x5d9d125bb5a8a6f37aaa7b26842d02c63a5eca09900a3a6f9cae5c08dde68f89, + 0x15ae64a91887466f6f97330c98f36b79a64db44d8d785d71c37756a348c550b3, + 0xf205427eacdbda08fa6b94bf013fd5e2cc780086687be61c26fb07fe428c9538, + 0xad022f2da58fa83a93623e2a9067e9ba8b7c1f637edab43198d12e3e01a3c40f, + 0xcfa9bdb1345d006969af85aa1323670dc2ba9b38f9d11afa9b5d4baf5f27803d, + 0x7d7e33b3b4e4649cacf88891405b80360316f1174b06a3ef356f4f25194b6243, + 0x57b1860684e57c0280ccb011651f7003e458a58ab401e6e550844c0e85beb1c6, + 0xd7e7971fcb0617132d4c6f7961dcab500ab77de23a6906e2cdc107454e98025b, + 0x1b8dcfcd7685d33c9e8269ddc685bb6b47ea4f6490cfbc6f78f35ff881cad61a, + 0x2f2a61e3728f59610b0151e9c271156d5e3834d48e9c69094e9f8141d469f73a, + 0xb9f5d962a96c1d5889fd49738d2000c4050bec944a54b87cd7c192dc4e87157a, + 0xc1f9f4136d8540c7adb7f4492bb9096d2c35395d7e31ef0bf81736c1d7348aa9, + 0x43eb81d6336dd3a975db138bd6e2cf41b8cc8b96b9bedda752edea5b4d9c2e55, + 0x9b85fb9c09b1ccfa92d249917966e8046ad97e6ab249a47f8617885081abfd87, + 0xf668f06352e6702b22cb47a005dea5ab5df334bf64e88a49cf6053a907f77b43, + 0x0608aaaa8d564e7d44e69993ff1c4966a4e30c1235dc24cf219000a3320061a4, + 0x23a58da214d62d4ae1c44e2d820ecef60c34c5475bb8fcc9272e32cef5762014, + 0xf5a34110cc0e28904bd98dbf377ec24614cbdc09f987a6e407081e48a57065ca, + 0x46d8d020036e91411034770588330d37e2e591ae080e1c7cc338922d81bf331a, + 0xcd1415bdccf9595523004666381755fbddc73ad53698f52a008c6f0551b4a6d9, + 0x4122b7484ebefa247a1442d523181b2febed23d001c82c51daf62ff91d322f13, + 0x75318f1feaa504936e59c444d8f83720ea2189c289baaf3b754bfe3c8d50dc09, + 0x7a6f612c3254e578d3b14cd37d5435f0e4df1899e71375da950e14b0a73a987a, + 0x86be5dd19bbf045462425d69f9910eab1de3434775033eb4bb3b0eb65d289cf9, + 0x46c12c8bece01c6a600db30824dc7bd0294dfa76612359f55578699e9287b9de, + 0x0354cb2e5243e8f2d79839d59703a763dd1000b5d006c7a35d6a1858092f9d7d, + 0x44d750680998eb7db2712c7ae035affcbc27d5dd3b30c38bd879d63d003c49f8, + 0x147b9c6c066b368ae94184fd4d41075eed2f93497d0cf4eda2ebd2a4fbf45ced, + 0x3f9f5de79995b5667963610ca74c57aefd35bbe335ee5540eb52436f06097d32, + 0xbdfe5aed560ae142ccd37cdd726a40fb978f3e7a6db69c19419626659d0a72b7, + 0xed8d138cb23bd0eb12965276a0728a4b573d24c871e4af81798d8c96ac2e0586, + 0x9def247cd85e70bb819e3689428a9409a31c58cf64f1d69f5c4d0ca28466fec7, + 0x9550a8bb3b7fb2b055d729a421aea514c1f13b97cf7fbb4a6249a3e11969024e, + 0x52b2e1fa5ae11086e6c900f0d784b61cf2f40e8f1ddad6ff4c02bbb6089d6f6e, + 0x10470aac8fedffbff37432c9d4fa7d5936952d011b4104c2de2ef76d1c9c5891, + 0x0b9624ed174e189ddbd2c0ec980c88324895ff3b048c7ff529645f115e443ea1, + 0xcd816e7fa1b33e1cc9b3f02de31263bd0d700bcfed28e8a4c9420c3a54420fe9, + 0xcb4c819c5662d53d62a58cf4db69d9618d74f4b017077530a0eb7b49422530b9, + 0x163d10da12f05ceab61ee8459f0c22950aef44f31a6cf959dc74e0b5281ab3fb, + 0xbd1ed9f75d7fe768d07fb35114a3f81cd6e2e48d2d3a7a7df4ddbcd7d4f92845, + 0xa637be39fc9857646ab4d4b680f5a42d0815f7edf9ba31c050056ad05effa19e, + 0xef2c1a78bbae58d3b768389cad6398a2748d21f12f3a681d5c5ea54b8b061c20, + 0xf40d1cbea4d2748e28d8dc0c8d4e6364151beebcad1ee7c725b404c29b3e40e9, + 0x862d70039e1beac80eb4e208f8dcb4890a16fb5a98a4224e825b6ac8014a1885, + 0x2c1a89582bdf1d82a71ef7c0b510384ed76f2654078ba42dff5a35aad7c1bf39, + 0xbd74be7f44e289566a74835a455de3c24d78901dccbf650c822c402411772283, + 0x863e66905cb7860acab853a08a13369e06d81b937b351c38c1e1237606abace4, + 0x9dde5fdf1a3d73ccb6749559d30418612423b470302f4610d5f0d7c0bf77fc50, + 0xd50d5803c4d2226787b85b4892b5cd99aa38d8ac2bdde40168077d3e7dc61968, + 0x68b924152b536cde4c33aae54a15f42f4d73836ec26af66c098f7ae57c1c0726, + 0x43abadcf477e01d774ca80969d1c1c977581bdc017c350a0d6a93a5b82b3bb55, + 0x3ea1c142f20374da7e0bbfaa8fb6f37182623feb4daae6b309115656f9b06ff3, + 0xd3c57cf2149466548b61fbe1a0b4921dd4dd991b6b3ca4545f4215620c10d3f0, + 0x04a003fe13db83f061fbf31972ed26b5f79b13f3be4453bccd0b84e9a80b74bd, + 0xd32dcbf248a852c3ffd1784e82bb22c33c1b1814e0ba71d71becea62974fc0d4, + 0x43442a8677ddb917ab9b618c5ac154b55a92d833b80464aba1d86d6d2f5f4099, + 0x0098416f6990a93a47db5a582e306cd7b058281c173c0346680c6d3e967d74dc, + 0x87ebb2ba71869f768f7118f6eadfd1a66080fc2acd736948780fb36cb9e3021e, + 0x25238966c8488762c2eaf3fbb7959e0c339bdcfeb8dd549a6c9af2881369081a, + 0x77d6e3d2024cb078de0aa1df106e87e3b38e4965aab8f5a0e2410c30250fb443, + 0xa25392f145b37f44f64c9674c6f3626847b9bd7cdf4d9f9de61cfad68dfcb67f, + 0xcc313e0a37f7fc8a3bd09fbed64aa0267ab9358c6450fb5ce98c9db71bd61eaa, + 0x64ae4f4e6ac626c4ff5c46f0ce721667623fdb9057fc6183a5c8621bde5e4950, + 0xec5b7c92e82474c2d2d6ed5b909b1cbb4b258e995b1ed2152c4f4e813941eb34, + 0x1c1311b97a5d1f2d2cf7faabb4ebbba9b5951b5c417437f702238bf63a310252, + 0x8b83ea486b0de8903ff04963c76d0ac8408da90cfe083f90d270e1ca395c04f7, + 0x40289a51c164842f7693464f7c2e8e0f3b6eb190b32db1abcb5d872b2af96cd8, + 0x573ca6df1d0b05c95d5e4296320b180a8b6708eadd4d3339d84f842d1a24ab15, + 0x090e32537987888f92959e9fb5cacdf2fd020d1f48556168696a72a0a5addce8, + 0xeefcfe1b275b7b829daeafc1c4d1de193e43474e4f6e7f96adb7bfd200000000, + 0x0000000000000000000000000000000011232f3c6dbbc4375136df3b07f7c70e + ] # 0x639e223e + smlen = 2436 \ No newline at end of file From f4575e5256c5a7a73803b9bb6db919d02144878e Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Mon, 23 Dec 2024 17:13:22 -0500 Subject: [PATCH 5/6] mldsa: add copyright notice --- Primitive/Asymmetric/Signature/ML_DSA/Tests/ML_DSA_44.cry | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Primitive/Asymmetric/Signature/ML_DSA/Tests/ML_DSA_44.cry b/Primitive/Asymmetric/Signature/ML_DSA/Tests/ML_DSA_44.cry index ed90353..691cceb 100644 --- a/Primitive/Asymmetric/Signature/ML_DSA/Tests/ML_DSA_44.cry +++ b/Primitive/Asymmetric/Signature/ML_DSA/Tests/ML_DSA_44.cry @@ -7,6 +7,9 @@ * @see https://github.com/post-quantum-cryptography/KAT * [ACVP]: NIST. usnistgov. GitHub repo "ACVP-Server". * @see https://github.com/usnistgov/ACVP-Server/tree/master/gen-val/json-files/ML-DSA-keyGen-FIPS204 + * + * @copyright Galois, Inc + * @author Marcella Hastings */ import Primitive::Asymmetric::Signature::ML_DSA::Instantiations::ML_DSA_44 as ML_DSA From 1e4e7df497e1881987c12a3c40a14d8e9337ebbd Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Fri, 27 Dec 2024 14:22:34 -0500 Subject: [PATCH 6/6] mldsa: add docs to keygen #192 --- .../Signature/ML_DSA/Specification.cry | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry b/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry index 39c8fba..6e42bda 100644 --- a/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry +++ b/Primitive/Asymmetric/Signature/ML_DSA/Specification.cry @@ -278,26 +278,33 @@ type d = 13 */ type β = η * τ - +/** + * Generate a public-private key pair from a seed. + * [FIPS-204] Section 6.1, Algorithm 6. + */ KeyGen_internal : [32]Byte -> (PublicKey, PrivateKey) KeyGen_internal ξ = (pk, sk) where + // Step 1. (ρ # ρ' # K) = H`{128} (ξ # IntegerToBytes`{1} `k # IntegerToBytes`{1} `ell) + // Step 3. A_hat = ExpandA ρ - + // Step 4. (s1, s2) = ExpandS ρ' - // An element of `R` may be "typecast" to an element of `Rq`. [FIPS-204] Section 2.4.1. + // Explicitly typecast vectors in `R` to `Rq`. s1' = [map fromInteger s1_i | s1_i <- s1] s2' = [map fromInteger s2_i | s2_i <- s2] - + // Step 5. t = NTTInv_Vec (A_hat ∘∘ NTT_Vec s1') + s2' + // Step 6. (t1, t0) = Power2Round t + // Step 8. pk = pkEncode ρ t1 - + // Step 9. tr = H`{64} pk - + // Step 10. sk = skEncode ρ K tr s1 s2 t0 /**