From e17c6f08851024f4b29994d64e153831162cfa66 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Fri, 4 Oct 2024 09:41:14 -0400 Subject: [PATCH 1/6] mlkem: rename files, fix directory structure #148 This fixes files to be capitalized, removes an illegal dash, and adjusts things to sit in our newly established directory structure. Note that this does not build because the module names no longer match the file names. --- .../ml_kem.cry => ML_KEM/Instantiations/ML_KEM.cry} | 0 .../Instantiations/ML_KEM1024.cry} | 0 .../Instantiations/ML_KEM512.cry} | 0 .../Instantiations/ML_KEM768.cry} | 0 .../Cipher/{ML-KEM => ML_KEM}/NIST.FIPS.203.ipd.pdf | Bin .../Asymmetric/Cipher/{ML-KEM => ML_KEM}/README.md | 0 .../specification.cry => ML_KEM/Specification.cry} | 0 .../Cipher/{ML-KEM => ML_KEM/Tests}/kat.awk | 0 8 files changed, 0 insertions(+), 0 deletions(-) rename Primitive/Asymmetric/Cipher/{ML-KEM/ml_kem.cry => ML_KEM/Instantiations/ML_KEM.cry} (100%) rename Primitive/Asymmetric/Cipher/{ML-KEM/ml_kem1024.cry => ML_KEM/Instantiations/ML_KEM1024.cry} (100%) rename Primitive/Asymmetric/Cipher/{ML-KEM/ml_kem512.cry => ML_KEM/Instantiations/ML_KEM512.cry} (100%) rename Primitive/Asymmetric/Cipher/{ML-KEM/ml_kem768.cry => ML_KEM/Instantiations/ML_KEM768.cry} (100%) rename Primitive/Asymmetric/Cipher/{ML-KEM => ML_KEM}/NIST.FIPS.203.ipd.pdf (100%) rename Primitive/Asymmetric/Cipher/{ML-KEM => ML_KEM}/README.md (100%) rename Primitive/Asymmetric/Cipher/{ML-KEM/specification.cry => ML_KEM/Specification.cry} (100%) rename Primitive/Asymmetric/Cipher/{ML-KEM => ML_KEM/Tests}/kat.awk (100%) diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/ml_kem.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry similarity index 100% rename from Primitive/Asymmetric/Cipher/ML-KEM/ml_kem.cry rename to Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/ml_kem1024.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM1024.cry similarity index 100% rename from Primitive/Asymmetric/Cipher/ML-KEM/ml_kem1024.cry rename to Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM1024.cry diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/ml_kem512.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM512.cry similarity index 100% rename from Primitive/Asymmetric/Cipher/ML-KEM/ml_kem512.cry rename to Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM512.cry diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/ml_kem768.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM768.cry similarity index 100% rename from Primitive/Asymmetric/Cipher/ML-KEM/ml_kem768.cry rename to Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM768.cry diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/NIST.FIPS.203.ipd.pdf b/Primitive/Asymmetric/Cipher/ML_KEM/NIST.FIPS.203.ipd.pdf similarity index 100% rename from Primitive/Asymmetric/Cipher/ML-KEM/NIST.FIPS.203.ipd.pdf rename to Primitive/Asymmetric/Cipher/ML_KEM/NIST.FIPS.203.ipd.pdf diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/README.md b/Primitive/Asymmetric/Cipher/ML_KEM/README.md similarity index 100% rename from Primitive/Asymmetric/Cipher/ML-KEM/README.md rename to Primitive/Asymmetric/Cipher/ML_KEM/README.md diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry similarity index 100% rename from Primitive/Asymmetric/Cipher/ML-KEM/specification.cry rename to Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/kat.awk b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/kat.awk similarity index 100% rename from Primitive/Asymmetric/Cipher/ML-KEM/kat.awk rename to Primitive/Asymmetric/Cipher/ML_KEM/Tests/kat.awk From b74789205f09c5add4d685d8ddc9e41c4946a8d9 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 3 Oct 2024 13:49:08 -0400 Subject: [PATCH 2/6] mlkem: rearrange directory and module names #148 This brings module names into alignment with our standard (capitalized, matches the directory path, etc) and the directory structure in line with our recent changes (`Instantiations/` and `Tests/`) --- .../Cipher/ML_KEM/Instantiations/ML_KEM.cry | 5 ++--- .../Cipher/ML_KEM/Instantiations/ML_KEM1024.cry | 15 ++++++++------- .../Cipher/ML_KEM/Instantiations/ML_KEM512.cry | 15 ++++++++------- .../Cipher/ML_KEM/Instantiations/ML_KEM768.cry | 15 ++++++++------- .../Asymmetric/Cipher/ML_KEM/Specification.cry | 2 +- 5 files changed, 27 insertions(+), 25 deletions(-) diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry index a2747887..8f116605 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry @@ -1,4 +1,3 @@ -module ml_kem where - -import ml_kem512 \ No newline at end of file +module Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM where + import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM512 diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM1024.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM1024.cry index d4ca1ee1..51d5afc2 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM1024.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM1024.cry @@ -1,11 +1,12 @@ /* -@copyright Galois, Inc -@author Marios Georgiou - -@copyright Amazon.com or its affiliates. -@editor Rod Chapman -*/ -module ml_kem1024 = specification where + * @copyright Galois, Inc + * @author Marios Georgiou + * + * @copyright Amazon.com or its affiliates. + * @editor Rod Chapman + */ +module Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM1024 = + Primitive::Asymmetric::Cipher::ML_KEM::Specification where type k = 4 type eta_1 = 2 diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM512.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM512.cry index b99906d4..fa4f4d12 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM512.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM512.cry @@ -1,12 +1,13 @@ /* -@copyright Galois, Inc -@author Marios Georgiou + * @copyright Galois, Inc + * @author Marios Georgiou + * + * @copyright Amazon.com or its affiliates. + * @editor Rod Chapman + */ -@copyright Amazon.com or its affiliates. -@editor Rod Chapman -*/ - -module ml_kem512 = specification where +module Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM512 = + Primitive::Asymmetric::Cipher::ML_KEM::Specification where type k = 2 type eta_1 = 3 diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM768.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM768.cry index f75b5001..8d78e852 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM768.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM768.cry @@ -1,11 +1,12 @@ /* -@copyright Galois, Inc -@author Marios Georgiou - -@copyright Amazon.com or its affiliates. -@editor Rod Chapman -*/ -module ml_kem768 = specification where + * @copyright Galois, Inc + * @author Marios Georgiou + * + * @copyright Amazon.com or its affiliates. + * @editor Rod Chapman + */ +module Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM768 = + Primitive::Asymmetric::Cipher::ML_KEM::Specification where type k = 3 type eta_1 = 2 diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry index e039b37a..1e45054a 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry @@ -7,7 +7,7 @@ ML-KEM cipher with a fast NTT implementation. @copyright Amazon.com or its affiliates. @author Rod Chapman */ -module specification where +module Primitive::Asymmetric::Cipher::ML_KEM::Specification where type q = 3329 From 38834ecad2a854b396fdb70a6f455f85f1b002ad Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 3 Oct 2024 15:29:50 -0400 Subject: [PATCH 3/6] mlkem: add KAT for ml-kem 512 #148 --- .../Cipher/ML_KEM/Tests/ML_KEM512.cry | 137 ++++++++++++++++++ 1 file changed, 137 insertions(+) create mode 100644 Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry new file mode 100644 index 00000000..b6e9a64e --- /dev/null +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry @@ -0,0 +1,137 @@ +/* + * Test vectors for ML-KEM512. + * + * These are sourced from the Post Quantum Cryptography KAT repo: + * @see https://github.com/post-quantum-cryptography/KAT/tree/main/MLKEM + */ + +import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM512 as ML_KEM + +/** + * This takes ~20 seconds to prove. + * ```repl + * :prove t0 + * ``` + */ +property t0 = keygenWorks && encapsWorks && decapsWorks where + keygenWorks = ML_KEM::ML_KEM_KeyGen (z, d) == (pk, sk) + encapsWorks = ML_KEM::ML_KEM_Encaps (pk, msg) == (ss, ct) + decapsWorks = ML_KEM::ML_KEM_Decaps (ct, sk) == ss + + z = split 0xf696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68 + d = split 0x6dbbc4375136df3b07f7c70e639e223e177e7fd53b161b3f4d57791794f12624 + msg = split (join [ + 0x20a7b7e10f70496cc38220b944def699, + 0xbf14d14e55cf4c90a12c1b33fc80ffff + ]) + pk = split (join [ + 0x80b70100831d7ee168f47392483119f93863ecb0bc605312d3, + 0x5728876b00f5f57af4c85eda97281d574390bc7256193668dc, + 0x98625354ab52b9bce781c5771cc26099f6fbacbee1784d1948, + 0x87731f097c87e082cbeac57d30b7b9a293872c841466f2244c, + 0xc65ff4ba653d6751dfa22051d553369942c31c29f91307af57, + 0x3292d697a8c31612e07b5335cf08329fd246bf2a32200a8cb0, + 0xc4b03b9d09c5ba1c3919539e9229c696924348282f696b1525, + 0xe5603806b4db618b3dc8630cb286e4311721bc5031f257aa92, + 0x5bf80960445aa8d8e69788e99da95c1d10cc3be858528db0cf, + 0xea003c74693780a65a36e62843b3be15406543d22d83507c87, + 0xb2786792c80fa5628454a310394dda4c2ab59493850257d6d3, + 0xbc107186d9062707f354e81a1a10fcb763d31a4ec409aa243e, + 0xd2e59bb189855eb1656266bb37500785ea08cd88c222a8c53a, + 0x8777cab42c9c238a00d59369425026e99d2ae6040af6709029, + 0xca8789c897b329fba748d69c8a7148c95abb0c71787c58f12f, + 0x21f2213e389242aa7fbd320c12ac42c611606cb8c1d1b46258, + 0x86a145a535bd65bd0d996b330c1657d61a87e9041700322575, + 0x9820a3bbec505cdaf11193229aae173cd12bad22a7a30a76a9, + 0xfa7636c3d5aa48e1784012a012f14168b7853d2a16f90ca02c, + 0xc33b2006c08f26c15fca29612cc792e1cf02e1321a75a81089, + 0x1986667d4148af36e65e1a592589029617734c315c0e39b751, + 0x8c8660cdc265d0c813ef20a043317fae5b8e40546eecf71d6c, + 0x054fa66b49401309bef30fd51a5519755da9104689b26f0839, + 0x154c847bef2365943c0249483aad9a7367c980a3d1ce46d200, + 0x8a15275ca3bca4834e6f9a3036c0cd80ba228d34b9780244d5, + 0xc0cbe907c6fb43824a9c0746471639cb86188c60c3b253215c, + 0xc91692bcd1493d6a444d536446e02968138001cc287e0e518f, + 0x3aa25d8c3b95b3c35c59f4819d484976029af05a263c35336b, + 0x261f77b2cdc29389f084c04cbb370c48562b5b50771c0fb816, + 0x908e198dd6d53f76e48bf042c2b1f82a3a40b8daf51f46d76f, + 0xa4bcc9d3c894ff850c0faa32e0ac33901a4c79139f5f20417e, + 0xc1a190607044f18bb824cf350c78ab3ddf3c2c86ca5543f715 + ]) + sk = split (join [ + 0xfada6a79a379d2cb36c856450c446f4484b86a560c6170564d002e4b74073f66a6fb, + 0x6a57bce1be92a1a1b531c61f50882a0084508542a1e1c3b3a950f2072e9a16544e46, + 0xca20284b6012a62c697ac858615e181e1ea0b55b002119090b7b871920e9b894b07a, + 0x281269dca15faf4a09b0004cac61a2cea73f28057dbf1219d07747b381cf0de52aba, + 0xd30ca0f57873b2bfa012bd5bc24805f3657ad0ba6bc4988cd9c6de492c0d433ce5aa, + 0x328bd6c6cb502463340dc5e029d2c8713d780f31f441c24c4000e56799a6bc66b4a1, + 0x93c73ced560f8ae43f9b2075ceb778976b7f111acb38a306f2b70a2bd8752e828086, + 0xba0f3e811a8c3b0d5f8b9072159e56ba1e1008009195af58a85a3e271f00ac25ccf3, + 0x233cb8716768ad98e7b1f2890db6170f2b614f56c1933871ae1a413024ca9a213779, + 0x5c8a2e9e15280ff108aee328235751e569ca63a7821f29ad26706b231224d95160bd, + 0x7522dde0bfe6e0a8261974885a2fdf217f8c16c4f67c0e9fb2a2f7030caf881d2c8b, + 0x2e6a6863906192108b004260b0adea07c0b349d588110a9cbb699b3952bb112cc7c8, + 0xd9a759b9554c1f991ea1f51f4c6178e43827c5149bda077fbd769a3b818df71a4286, + 0x0783fd233d1b26a96a573e99eb915f6bc18d813ded14a304c1358e470570d25478a6, + 0xb6ba2ac5612890b5a569e5263342459cb9ca7674f228396954af748d9d5013534271, + 0x3904cc59106e0bb21942b4066f86bf5d9c3cf1b6c08692c5b9881b29971088a8b415, + 0xe26c4a2567588b2ddfb68d11146fcff0b4cb79c57487018c25541d3267a10640e430, + 0xbfebbb4f45a799c9f554d1b69d70c79d17124f9c01cf3ad6569e77a4e1b657047010, + 0x06452f45a72f3298c660820f1c206af700c9a621923c3911cd518e022404c870c3d3, + 0xb3b6831a82536a3170334e3159b0c959036c432cf5b484b12c75ccc3c96ce328fbba, + 0x79e2f724789a8d27f7af8bb08645d2c9a3e87f8042c36227194a3c0e14d09129d069, + 0xd5379dbd606565d915a3bc9882e87423a062000a5f4c5523ec9447cea1643a97ad33, + 0xc1986246ad91e273ce32acaff45335996537072180b70100831d7ee168f473924831, + 0x19f93863ecb0bc605312d35728876b00f5f57af4c85eda97281d574390bc72561936, + 0x68dc98625354ab52b9bce781c5771cc26099f6fbacbee1784d194887731f097c87e0, + 0x82cbeac57d30b7b9a293872c841466f2244cc65ff4ba653d6751dfa22051d5533699, + 0x42c31c29f91307af573292d697a8c31612e07b5335cf08329fd246bf2a32200a8cb0, + 0xc4b03b9d09c5ba1c3919539e9229c696924348282f696b1525e5603806b4db618b3d, + 0xc8630cb286e4311721bc5031f257aa925bf80960445aa8d8e69788e99da95c1d10cc, + 0x3be858528db0cfea003c74693780a65a36e62843b3be15406543d22d83507c87b278, + 0x6792c80fa5628454a310394dda4c2ab59493850257d6d3bc107186d9062707f354e8, + 0x1a1a10fcb763d31a4ec409aa243ed2e59bb189855eb1656266bb37500785ea08cd88, + 0xc222a8c53a8777cab42c9c238a00d59369425026e99d2ae6040af6709029ca8789c8, + 0x97b329fba748d69c8a7148c95abb0c71787c58f12f21f2213e389242aa7fbd320c12, + 0xac42c611606cb8c1d1b4625886a145a535bd65bd0d996b330c1657d61a87e9041700, + 0x3225759820a3bbec505cdaf11193229aae173cd12bad22a7a30a76a9fa7636c3d5aa, + 0x48e1784012a012f14168b7853d2a16f90ca02cc33b2006c08f26c15fca29612cc792, + 0xe1cf02e1321a75a810891986667d4148af36e65e1a592589029617734c315c0e39b7, + 0x518c8660cdc265d0c813ef20a043317fae5b8e40546eecf71d6c054fa66b49401309, + 0xbef30fd51a5519755da9104689b26f0839154c847bef2365943c0249483aad9a7367, + 0xc980a3d1ce46d2008a15275ca3bca4834e6f9a3036c0cd80ba228d34b9780244d5c0, + 0xcbe907c6fb43824a9c0746471639cb86188c60c3b253215cc91692bcd1493d6a444d, + 0x536446e02968138001cc287e0e518f3aa25d8c3b95b3c35c59f4819d484976029af0, + 0x5a263c35336b261f77b2cdc29389f084c04cbb370c48562b5b50771c0fb816908e19, + 0x8dd6d53f76e48bf042c2b1f82a3a40b8daf51f46d76fa4bcc9d3c894ff850c0faa32, + 0xe0ac33901a4c79139f5f20417ec1a190607044f18bb824cf350c78ab3ddf3c2c86ca, + 0x5543f715ca875d7c7e8501256071ea518d2f185b05626aa3d1c38cdbc2d006ed0051, + 0xaac6f696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68 + ]) + ct = split (join [ + 0x917e59d1e182a29648a61955a154b304a842f458eba593f3065fb7d744fba24f, + 0xa3a0d538854e32844db248d48100c389c4c4b3ca6c234f2f61a67932aeee808d, + 0xbfe98d896d1e9668820965c6343bbb4a4de64b7a99fb53b5264e3199d587ffa5, + 0xe0479f6b7386b23cb9c243fa6f5457fc97dbc96dcc039bd6c4e7e85a90b5c523, + 0x2416434ea942cc71134bb9a2f4991e0595e3487feabac479cab9510d57b86250, + 0xee7c96a67a9f2c6121f7daa02c5cfa3b23b0c732c2b15694e1ccbac82b787cf2, + 0x118d08425cbba121882217940c894cbe47aae2541f5c6e0bd1baab31fd2b2ecb, + 0x34b9e693f6fc0fdeea906716d08818f51df0c4694029e8c3234be0b62471b276, + 0x9d9ac4ceb947602380f3a497b2a01ff7b8746c1c7ae81983e016bd65c7cd1762, + 0xc191857e41c2321981f6c7aa8d7afaaa9fa0b557ec1ec1285f8b4d6c788aff15, + 0x9ea5862e814d0825c8834b7ca45db7c8eda3fa6a6a7b8a40519529bf74b6a0f8, + 0x0c484917f40c107d182bce3e344fd36d1b377a982f6bf2361b8d662875c166dc, + 0xca73240b86df5ee0fa4231b356f0cdd6b3170ff89113db0b1b9dd26433578322, + 0x2cbe7be844642b0b1988d18b268da6f78cc944f43b827143c4dc5ee1f0d658b8, + 0x7b9c00862f263d6f5798fc82e8be079a1108defdd4c7863c3147e9bdf0fbc84d, + 0xeba215fdfb9ca4237a8419b26fdeff63a7f95c442bce67966ebe6b5f9af1fd2a, + 0x7cbed648ea7276db742dac3e470f6cc741d82e77e9c0dd019b5458177551975b, + 0x59633be67b35c0d430b725524deafdeba6d3643c5c82ebb52479669c411bb56b, + 0x397f8d37b8f7fa4ced0316546caaee419c0e7f1d96a0ec614c6c9c8e03e01003, + 0x1765121f1eb8fd549fde046a50443ebab9fea2e78a29f4964455928db1f9e782, + 0x0e533c5712989b3a3637ea00a1de3e469a800c431d4df243c1dc7d6a89ba7900, + 0xd52b78bcc103474f9d2c2128025c3193c4d1a09f50905ad2de7fe8e09f047e0e, + 0x72e6dab0edf7e3b08ed1316acf857254b6c1fbf64ce582f2990ccecf9505fd7e, + 0x8517998aaf583be1aa641e9b54dbb91ca9d0700913967fb0349201b5d679b32d + ]) + ss = split 0x2b5c52ee72946331983ba050be0f435055c0547901e03559b356517889ea27c5 \ No newline at end of file From af48a954f52048afc8e1068dd9b86b223c02a39c Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 3 Oct 2024 15:46:06 -0400 Subject: [PATCH 4/6] mlkem: add test vector for ml-kem 768 #148 --- .../Cipher/ML_KEM/Tests/ML_KEM768.cry | 179 ++++++++++++++++++ 1 file changed, 179 insertions(+) create mode 100644 Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM768.cry diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM768.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM768.cry new file mode 100644 index 00000000..10e81e28 --- /dev/null +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM768.cry @@ -0,0 +1,179 @@ +/* + * Test vectors for ML-KEM768. + * + * These are sourced from the Post Quantum Cryptography KAT repo: + * @see https://github.com/post-quantum-cryptography/KAT/tree/main/MLKEM + */ + +import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM768 as ML_KEM + +/** + * This takes ~35 seconds to prove. + * ```repl + * :prove t0 + * ``` + */ +property t0 = keygenWorks && encapsWorks && decapsWorks where + keygenWorks = ML_KEM::ML_KEM_KeyGen (z, d) == (pk, sk) + encapsWorks = ML_KEM::ML_KEM_Encaps (pk, msg) == (ss, ct) + decapsWorks = ML_KEM::ML_KEM_Decaps (ct, sk) == ss + + z = split 0xf696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68 + d = split 0x6dbbc4375136df3b07f7c70e639e223e177e7fd53b161b3f4d57791794f12624 + msg = split (join [ + 0x20a7b7e10f70496cc38220b944def699, + 0xbf14d14e55cf4c90a12c1b33fc80ffff + ]) + pk = split (join [ + 0x01f60af1dc8e6360ae78b59d4a5042eb9145a269046d6236b8304f305c2d9dcb, + 0x189fe5a62df89b2f5a7bce3bbc753c1e78f730a99869f809aba856b676b707b2, + 0x6601d1d909bab32451494eb7d0a2153a6350b79789a9b115f83ea12037256562, + 0xf06a1d5aba378da77039d3bdecaca8e6a22a49050a76300a0267cdb38b7ac779, + 0x03c50ca53b99283cac6b95fba651b11a4d1a692e4072965060587669f253b1bb, + 0x182e661446168ac60221894660020e9bb5f5b7124a0303e2543ea3ea6ce97a24, + 0x82b255ca346fb27a847b33b93f3ab2d33064c6e6632d1a23f1144e907b246b47, + 0x9f4a5c928929a1e24150f5241258a5b67766a66f6a33846495907828ebe44ecc, + 0x5b73124071ba479073910410a16d5d5696b48b194752979795772a91c348f502, + 0xb37aa650983ebb89bf3c081ff273544129c9137a6e1834c8f2e7ce14c7870c53, + 0xc05b9b94ecd38e6645911b0912336863ec168831f811881075cf38a59de4b5c7, + 0x38aa6ef03d779b295588cfb62491cc7b3e08b48473354f9ac8061c152a9e2059, + 0x97499b970b69bce66fe42bca2924ccdf0103d0a4c39193c2df25118d72b17aab, + 0x26b0c60d4cd2c306ca4696c185de05035f4a09cf970aecc8cc93436f83b1aeaf, + 0x452c41929a2eabc151938f74c93b858546df2264eeeab602e04a85c522f8fb1a, + 0x5214afd8d4cae57a47b6f381a23126bd9917173128af917f1d483691c450d115, + 0x1cfe9a1492d473ed862e27da92500c86a20019e9f975e4f54ad319ba2c5630c4, + 0x014219d7ba235456fe530140193d662445e6a941d1e238567ba8d4d95ab1c744, + 0x7d690821876d017270cfb169f2d792f03c800720697b410ab41c66f2b2458512, + 0x5655eb10aa1087ffcb7750cb887ad4467377500a6a7d3a82976b415a54469577, + 0xb4138d919b03f4c9a4d3390bdcb6f1717a5fa4ab25a34f4ba5039bb22c7f3c23, + 0x4ea4427347aa7251464e631904d7cac4784f78b49d5f4a104a301809a779f646, + 0x6131f9c62bb67147f4cd4973a6aa1c29ae6a8647b6268be089fe048ce990cd63, + 0x8743d285c889a707f581b63af41731f0246b054bc4b47aab01b6842a2709d02e, + 0x8158ab90f48b69d136082b34cb0673b74aa3f54508ed029fb8f5045ee0639e15, + 0x0ee3b3c85f68a310ec0441980100b42abf2bad10d4a9e0c7b2bc5bbcaf73cbcd, + 0xc49dc2c949111936779b178974a0392947745a47189bc3fa8a679c80af964a9f, + 0x9b1b56577274a2a669d2da6704aa496af407fa1aa964cc3dc3140f5f959a7ea9, + 0x74bdb1b83e48a99c0a3e2d75b0669b5c1278962540609166266da18886fc237a, + 0xf30cefd569dbe399e6652e45f06a5dfc9a758a4987088ff8e38a3cf36b9d988f, + 0x0e070b68d0b88f7bcc41306080d889780c7e238895ccaa4f3577225cca4c8a93, + 0x30ce613e717798c9670924b271ac402b51538b8b5967ac490dcab5300e6c54d6, + 0xa3632f3b973e4186ee1a7e2e85649185b26370c387235c4df28a9937a49d4078, + 0xbf883f4e6346cb3251d9e13f1bda087b285afaa80e262641c5527b0a184b8bc8, + 0x4a62e577314658e2029d850064f7a7b81f253e7cc124a9c5b039dc9b179a80c2, + 0xf6aee6ea0815172537331a57b505baa76ff5b4c1f0da754b6194f4b39a9b1873, + 0x0d3cdab925d691ed77a8db9927ea233ac2a12744fdc27e5d221b9369adb325d8 + ]) + sk = split (join [ + 0x9c700fe444904db5708e16b1ba7650fbe94f24a6abba262ad7acbd1a13877565, + 0x66e1ac7a1e545b236c548e8661c5f468c58c3bbc49cccafb7a66a3b616786107, + 0x84a88a8872255139d979bdb140649b06acbcc91c74d3bc791591b0f31f2c9ab2, + 0x4d329934795405b7570a994e0d128aa08681a3cc58680937401a563bfb4e621a, + 0x4193416ccb1c3c9d9b23dfc9979f91140b37c6e7a517ae6c8f268b3346e52ad0, + 0xa311f79acea0a56cb9291ca0161a98aac43ef2ba55618312910012ab603ac4c0, + 0xbe64a498e58ecb217e2a102b8a518bbbf9c457412f030c1a82cc7ea67c8fd145, + 0x11e55436daa7383ee2c942da15f67581f069563e8ba3752ba159314973dbc737, + 0x4244ed486c6ad77abbd89cab1c1934153439b58f586bcf00813b050744debb78, + 0x9dc4b3a1d054e710905f066bc2ab7643d2883e096e749988a0612667633a9b98, + 0x748c23c708d29891e84edc8c4cbc43999ec88c8a854d69402b8ebaa4d6cc09ab, + 0x42220b8413da34b7cfaab2c6b47f1610cbb1d8b080051fa7d974ff53b71c8726, + 0xaaac2f3daa9c6a68932d0172f2174d989090b822bacf105b7ae70fa59296d6b2, + 0xc7614900a9f869db16600939bb1e116b1ce913ceea4ce60a2cd98cab92e28800, + 0x70866fe04b0423c0dcec04d3f921fb8c0ad5c16a077a3f2484212d90ab2bdb14, + 0x29ca837af87d29d63438440a273c3e9484a1481b54e68712e3fcc1e562799243, + 0xba3f339bf1025c5c1b29e1294a0a7a3efbb75e47b31c12fa65c90a7adbcc2aea, + 0xb0278c96513b25945dc32b9f382d2751a27ca572524127695765f9b45c88f923, + 0xc28869bda5c7af4060042913f4d330c0453c985442dca58ee28a94bfeb85f2b4, + 0x9c21a556fff04e09d66aba875a4819390bba7586f77bdfc0b1f639b586fc591a, + 0xb9250c8951e143c2f9c790697ac51a9c153b493315644a73274674fb083c852a, + 0x1072b80181be1ecb8f59769ee0903757326625376f9fba3380a55cca42786e11, + 0xa4769c7b4761c5f5db112df69839579d82ab0340a34dd62c15165bcd67b66f04, + 0x65546af56b6a637467393b28242c40c387000349a60a730237250709b208956d, + 0x00fd715b239af96c418ac0147d0c63f8f9af30a272cbd629293395cad10937c3, + 0x2e7454815f93aa9a4c0661dba4dbb1069fa4b59474cf8f10ad45563c983906ed, + 0x324b5f776e5725be938696c0f6799e489d8b80656913c687374dfeac8adb3153, + 0x6c90c6079069ee142fd800b3721b0aea35220dd04d85b19b872548e7005e92e6, + 0x74a235164d6a2e53b6774af42d211c77bd6454c2445f68d04f357106afc8c0a2, + 0xbc8e4fa467676a2957b060f0e9923a639274977216341b1aea876a0b7dee4013, + 0xbde2459c957dcc2b5263b02e2ae3a6904cb856c49bdb5699c16997953cb1056a, + 0x4cfb362ad3646fb5d7393418b8fe556f1dc924cc74b3f9d7876473355e2751f3, + 0xe98ef5eab3bb974fbe884d0bda85b8fc4dce0c852853ad7a62528c3bbc32002f, + 0xa469bb89895621944ffa29429c106c3946320ee9bf3c822115d53e968a76c258, + 0x1e00f906e60ca372a22686d74c9ffb52a24abee52b788d015bf6a5c757549352, + 0x7c97f927561df15d47f558b5466c8247277ab35c0170c6c05a8af8e67edf524a, + 0x01f60af1dc8e6360ae78b59d4a5042eb9145a269046d6236b8304f305c2d9dcb, + 0x189fe5a62df89b2f5a7bce3bbc753c1e78f730a99869f809aba856b676b707b2, + 0x6601d1d909bab32451494eb7d0a2153a6350b79789a9b115f83ea12037256562, + 0xf06a1d5aba378da77039d3bdecaca8e6a22a49050a76300a0267cdb38b7ac779, + 0x03c50ca53b99283cac6b95fba651b11a4d1a692e4072965060587669f253b1bb, + 0x182e661446168ac60221894660020e9bb5f5b7124a0303e2543ea3ea6ce97a24, + 0x82b255ca346fb27a847b33b93f3ab2d33064c6e6632d1a23f1144e907b246b47, + 0x9f4a5c928929a1e24150f5241258a5b67766a66f6a33846495907828ebe44ecc, + 0x5b73124071ba479073910410a16d5d5696b48b194752979795772a91c348f502, + 0xb37aa650983ebb89bf3c081ff273544129c9137a6e1834c8f2e7ce14c7870c53, + 0xc05b9b94ecd38e6645911b0912336863ec168831f811881075cf38a59de4b5c7, + 0x38aa6ef03d779b295588cfb62491cc7b3e08b48473354f9ac8061c152a9e2059, + 0x97499b970b69bce66fe42bca2924ccdf0103d0a4c39193c2df25118d72b17aab, + 0x26b0c60d4cd2c306ca4696c185de05035f4a09cf970aecc8cc93436f83b1aeaf, + 0x452c41929a2eabc151938f74c93b858546df2264eeeab602e04a85c522f8fb1a, + 0x5214afd8d4cae57a47b6f381a23126bd9917173128af917f1d483691c450d115, + 0x1cfe9a1492d473ed862e27da92500c86a20019e9f975e4f54ad319ba2c5630c4, + 0x014219d7ba235456fe530140193d662445e6a941d1e238567ba8d4d95ab1c744, + 0x7d690821876d017270cfb169f2d792f03c800720697b410ab41c66f2b2458512, + 0x5655eb10aa1087ffcb7750cb887ad4467377500a6a7d3a82976b415a54469577, + 0xb4138d919b03f4c9a4d3390bdcb6f1717a5fa4ab25a34f4ba5039bb22c7f3c23, + 0x4ea4427347aa7251464e631904d7cac4784f78b49d5f4a104a301809a779f646, + 0x6131f9c62bb67147f4cd4973a6aa1c29ae6a8647b6268be089fe048ce990cd63, + 0x8743d285c889a707f581b63af41731f0246b054bc4b47aab01b6842a2709d02e, + 0x8158ab90f48b69d136082b34cb0673b74aa3f54508ed029fb8f5045ee0639e15, + 0x0ee3b3c85f68a310ec0441980100b42abf2bad10d4a9e0c7b2bc5bbcaf73cbcd, + 0xc49dc2c949111936779b178974a0392947745a47189bc3fa8a679c80af964a9f, + 0x9b1b56577274a2a669d2da6704aa496af407fa1aa964cc3dc3140f5f959a7ea9, + 0x74bdb1b83e48a99c0a3e2d75b0669b5c1278962540609166266da18886fc237a, + 0xf30cefd569dbe399e6652e45f06a5dfc9a758a4987088ff8e38a3cf36b9d988f, + 0x0e070b68d0b88f7bcc41306080d889780c7e238895ccaa4f3577225cca4c8a93, + 0x30ce613e717798c9670924b271ac402b51538b8b5967ac490dcab5300e6c54d6, + 0xa3632f3b973e4186ee1a7e2e85649185b26370c387235c4df28a9937a49d4078, + 0xbf883f4e6346cb3251d9e13f1bda087b285afaa80e262641c5527b0a184b8bc8, + 0x4a62e577314658e2029d850064f7a7b81f253e7cc124a9c5b039dc9b179a80c2, + 0xf6aee6ea0815172537331a57b505baa76ff5b4c1f0da754b6194f4b39a9b1873, + 0x0d3cdab925d691ed77a8db9927ea233ac2a12744fdc27e5d221b9369adb325d8, + 0x6ff694a73b6701f2a7408773f9909118ef52e1c89285b2cde465a0b04980120a, + 0xf696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68 + ]) + ct = split (join [ + 0x16a61ff84787fd4a5f19ca59b3657db3a106a7329e2d62747a2ef85149163109, + 0xbefff6bcb33df66230b8f6725ce719f58f71196e895befc9754d9f042494648c, + 0x88a6ed4c4cf13f2faf9f651de79dae077733cb235f9dce448977fd42d5486b7d, + 0xfdf6d7bd9172b14247655d34f10524d469478d9a9639f34d2acde6e3c048d52b, + 0x308b66245fe9a28cde7983b9d14c03b37715fe3970cd35734771add7aa9b58cf, + 0xb0adf8c613deafb2b31f6e5c8364d4334e93af8e4943fa947cc67667447cffd0, + 0x36235afaea7f603cb2ea277b97dadf82ea746f6b27396dd08c85cff9304a2e5c, + 0xe0571fde2e926716bc9f8e4d474b4e8fd34b0dc28376204ea306d30e9a6dd882, + 0x50b79823e77319f2ef3a77704f409dde8beb6db1be4a9f25ae2e15939dedf1b1, + 0x1a5aa51fcff04068b46d42fbbafd2498264cca4fb78b0f2ab162c7ef569875a1, + 0x3148b9a4b0b9da1787ca0a7033e3eca13471dbcbbe15e34f2b5065b995fe221c, + 0x2b7ac150334d14e68edc5e049663de362fae8d35e24c202c5fad2153cd044ea9, + 0x62a388f030cdc5dec1c3423183b173c32b22f5800ae45e8e89c8ee4617ce24e6, + 0x0f278bfd1ea0f8fa92486b6f849127da99be7be4c661e2ba26669d6acf619a33, + 0x056809683e24a2f29e33be7f5f9ac668697e59488e9b8685956cd87b7c47109d, + 0x603202c201472ec829ea64922e4d0eadd4a4b5a8fb06e0f4bf25a59ced545573, + 0x88dcd91b387cb6148597edf84a22595801851ca4b9e9e096fdfc96f2444ac9f1, + 0x247a5e640787fca23e3eb21ec1059c42a65803441df01279013c448dfc3eedfc, + 0x3355eee1f510086a115f854c36db797a85ede19a473a33e79a80f6f7f6467e1b, + 0x0d866fe0e57a8abd379934a6a6a492f5f32594d43de2ec2eea81487981bb6394, + 0xbfa6df5498d74c6db2202a6348a325fbc906b8e820bb00659a2ee12740b14b2e, + 0x36f4c5dab411c0cd096c5e63ba4d48aa9e92b31f44dc97c0fef661bcf4db895f, + 0x174613d9d5ed9e836657745ec9deec7af273cec87ef0eaf805da1bc840160881, + 0x0b8a86f952c6326d09fc8d1d7fd83b4e862e05058e877c056cc5465ec3192b03, + 0xa4c33cc6b16558d2482d5f84518cbbc526aae6e8840317efb3a1982c3d1719ef, + 0x15d10f8b077c5c68680be6d3d92e86aaa6eb378cf0559d493257147b55730f49, + 0xa042325af066b4f9741b9fff5d47972d5acaf52b6bea4e9e354ef9448b62f6d2, + 0xa1317675a922e14e31578d6cab5a09a71ab270d865151b8ab4c612b5fd5dcc97, + 0xe45419a1cfb6b8b9aec60f62602098f91f07c238186657941c7a18e4d7ee220f, + 0x022d5fffd291853b9c063e561b7176f7a235ce45bc86ce4718086df9536c5a5f, + 0x0abf04c0a84d82bdf69552ade3135433c10a1ba69d688969e6d9dce54d3b3aae, + 0x3a7f2ab904e657e3fb05241fac110aa07e62cc3991d7d0d6329b5ab9d69d7336, + 0xc0d148588c9f0921325b85df5fd30db80a56a3724372153641961aa7e042bf26, + 0x46ff46022c059d5794c3a4b7f90c410de71a5231dd9b83bbd0e6bdab1bf9e62f + ]) + ss = split 0xb408d5d115713f0a93047dbbea832e4340787686d59a9a2d106bd662ba0aa035 From ac63f6599add4db50614a014e5599c6d11c46830 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 3 Oct 2024 16:16:23 -0400 Subject: [PATCH 5/6] mlkem: add KAT for ML-KEM1024 #148 --- .../Cipher/ML_KEM/Tests/ML_KEM1024.cry | 227 ++++++++++++++++++ 1 file changed, 227 insertions(+) create mode 100644 Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM1024.cry diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM1024.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM1024.cry new file mode 100644 index 00000000..a4ef0318 --- /dev/null +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM1024.cry @@ -0,0 +1,227 @@ +/* + * Test vectors for ML-KEM1024. + * + * These are sourced from the Post Quantum Cryptography KAT repo: + * @see https://github.com/post-quantum-cryptography/KAT/tree/main/MLKEM + */ + +import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM1024 as ML_KEM + +/** + * This takes ~50 seconds to prove. + * ```repl + * :prove t0 + * ``` + */ +property t0 = keygenWorks && encapsWorks && decapsWorks where + keygenWorks = ML_KEM::ML_KEM_KeyGen (z, d) == (pk, sk) + encapsWorks = ML_KEM::ML_KEM_Encaps (pk, msg) == (ss, ct) + decapsWorks = ML_KEM::ML_KEM_Decaps (ct, sk) == ss + + z = split 0xf696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68 + d = split 0x6dbbc4375136df3b07f7c70e639e223e177e7fd53b161b3f4d57791794f12624 + msg = split 0x20a7b7e10f70496cc38220b944def699bf14d14e55cf4c90a12c1b33fc80ffff + pk = split (join [ + 0xa8122f376b3f5d355263eba522c43995044beca78b9ba9924b87035490ae78a9, + 0x4d523c7ba588a386eb49bf652fdf12716373187a1ca047cc6138627aaeab8f6c, + 0xebbf87a176b86c9f7f093c8f5b0bdc147399e839ae737038d0bd0142369f9c9d, + 0x46b25b9ae540b80023d5d757e76b3fdd3064dd2b44cd06b44369277147b61565, + 0x4b325044e1bc606fa629055a2e6a4b02b2f1b1aa98a69391c91bd98f1058aa18, + 0xd9019ddbb6dce60a070bad4bec3df37a0d4dda8410288830e9ae509880a02b24, + 0x8e1bba8edb1cc520517c11b64d68cc00c69475a2a2d9c56a2773a02424b2bef1, + 0x7ddfb4c4cc503d05c888946579e4027dbf8a89370c74fa66c8a325c234296399, + 0x4c202fa05179352f92a18630822892151a7b8b163eea685c2c4f026015fee782, + 0xf1c53ca573807afc6bc766be008796fbb906e9e1abd1cc845f60423f0978df89, + 0x924aa118a2b41c7f458308e87b190a27002ba7f773cb65ec87165a6530a0971a, + 0x752069a42afbd271e1e236fc155aeff759ec762551e5bcdf3a66d6a9af92b4ce, + 0x14a29ed410cf72a808e90c81a46074611059802391006c52c5994519718a84f4, + 0x45e8d9c3c6616e0268b2e1d5af48b091c6053b7477740fea361853364de642a4, + 0x4b83364235b6a865037878074b37400c82591794a09055d5b34a9f186e1574cc, + 0xb3848f4b620016d807b945485bc4c9e17644fea65f5345c862d83aa1a4cd1b67, + 0x6409fa545c5712613c267b80447df08c87e532bd77500c14b08d7ac00dc7c2fa, + 0x50b1b5c26d27dca74ad41f9b0761426321a9b3a992a4c3fa151021bc2d17c88f, + 0xaab7274e65cc23d283ab55a951495872455bcce806a9e803c2d9b566a6addebb, + 0x78120ba9361ca9b8b10323f682cc5b9131d44f262501ed861c866c9e31d09789, + 0xf81dc3c773a4464c4cc9c4cb838b9bdb16ff26227a9871c57734b5c59c27e77f, + 0x061a7b56963296f48ae58a85e34063aaf644fee4178b3a9647191c4f022356cc, + 0x5b17e247644a809be0c04ca57df1dbbcaf1c2b1645217a615b98aa048ca48ad7, + 0x254f5b859249066abf6a33d59521b07cc684a1ac23089101c80dfacb82094445, + 0xd3358e6eb6461cf614cbc22248259ed19ab0d6498f3f20c660e9aa5ae877d297, + 0x3611a377b14860f9398408575af51819936883d080218ab0acafbb639a3019a3, + 0x8878a45a1264b30f709c46a3fa5e2d571f8f594d3ba90c432813b78005e1d20b, + 0x72551f87e978fcd8487bb584a4e97a66a058a9a750d15c479919c81ed235803b, + 0x8a657a8e08804f8c109f8dd16074124df22b0c4b276d2ac865b55a538d738262, + 0x26216ba21ec7368f30c638e3f201288a23c2861c3c88599f9027120b0dd7575a, + 0x8855c5411554f699b47ec667a3b2a62f828b2458965130126f29b7525205ef33, + 0x5d4740020a61c9c742aa3be0048eac3aa69b7d9a18846e5498e66b8ed550cdbd, + 0x91bbe0d0482347bfc39964f3f63cf4967ea9321418c377b8262e63225e17621f, + 0xfea466a6335e822059e46a8a5eb16ff321b3a043588c0bb6e5d2b4f3a8c100b0, + 0x5bf2715523433dbab50491216b9cdc2d526aae3bd218404c33beba959719b48c, + 0xc9ae4753512b171c75763b38fb4ddca82750abb505b8c3fc519e7536560d639e, + 0xf2476953b7bd7966c13bd09e8af17a542ab4927151ad4a46e8843c055591e78c, + 0xa8b4e5956822815a3c98eff1b9cc49aea06bcd24f9c70941a3d3f0810de25afc, + 0x154dd76069f2c2c367bb52a2c309ccf1708d514d3f871cc4e3bafe91549b44bb, + 0xf4b24c5525a19bb6abd50c693407851e1a7632883f783a08e5483e7ca7876e4b, + 0x2889417d7ec147e8624e4c83b8bb56bdef29aa47a5735034b48beb8c36c6223f, + 0x184502ecb3f8072d61e41cc8a21784a24be3c652f2d697a5a28ad605cbf0cb1f, + 0x928a25a13a9933700481f341b2a3c279021ed2d701303699aab12df4886303d3, + 0xb3e2949341b577f85ac326284a85f2494976790e762ec51c1a88faa2f5e03c0f, + 0xab44e399735374502f0029cfdb74e9e1517263654262320ff3c15ff48067c701, + 0xdf8436507373fdc7a475f13d961a45718ba1a4b56f02d0095030194a5cb34838, + 0x728387a33a310561e73d18c2af34116384879cfd2c70aae0400eec2bd667c2a4, + 0xc5a051e643c7d8ae8d1bab4352b9bd27b3e647259bb1cccb2304d725cb2e73c6, + 0x718b5abc88800949b2c1d03f159fbf396adca8526f1b476f80fe91c13308d645 + ]) + sk = split (join [ + 0x4b8ac400218a249150aff2339367484a6bcbf637646cf750156a7b35a936d05a, + 0x25647a3368e4891a030beba99ff9d550ca830ebf9b4aae231fc2dc4073aa9841, + 0x1a188bc2442c5349f20140c5a378037679840b23a795bd0ed5949d0b5d663bb0, + 0x1c575d7ff34594f4007053194ca6c4ecf90458e64f80e98ecfc9b062945eb129, + 0x22c5813fd1b9370b7ace2cb5707d72846274af203cc6bfb18a2fb35265b1160c, + 0x33393ab658d712434a9149616bca8b839c8ffa85c7054d6e697e6f181b310858, + 0x774c94fb4089804b989cc91cb3dca5da8b31b4733271b412cc38477b46836b08, + 0x8373a5338d6816e7f8993ceb16e260086203c465a769be7968a9189c5e0283de, + 0x590d5c61c5b1a383d1635bedd47ba4c86d803c625f22ba8a86093f03baa8c638, + 0x958805b5367e1b793705d0c5aaf36f2a52c01c803516b0c38e8407b3e6133245, + 0x3cc37b73ea629117d069b937038fe99f3e069766b491a503540a585382619d25, + 0x590f2ba31fd125a24fe066b63a215cb6cfa581381b0b91c3ec4ee5e15f6f5663, + 0x30da146f32652343afcbc56293b30ebe399bd08327b1f656b15baefde61f7a55, + 0x1932c9b4d2c88eef799b3bf85c2886b7dc31b81cda27c0b73bf4cb2271548297, + 0x9974887aad36297f3e0365d8c6164ae974d0ecb0997250a7e92a74fc3d5abc3d, + 0x78d23076639f9dd74374ec54ec0a32f6bac11ce8acc2eb70ec4c93ace48688e6, + 0x5b084725fc3899dc7ac1469cbb00588782e2792c30c4fee8ac44168d8abc8c53, + 0x5a3987970c9c706aef78b8de590569791cc1c9b3e8f72a49cc478ff2abb0e561, + 0x6132693dfb7cb5386fcf6ac7747ab328d12d88496764fcb8ee682c886462da1a, + 0xc8b028aeb65b6c77fc94f6511ef6c20f66485ca6ea27b7ba339f8865fa10957e, + 0xf2c7efb46ca5841976d6b3dccc7537152f8e142cb18c93e232124a426f0b0288, + 0xa3045c94f5a9450156d8f590a497995f68c7b23799be486163b261e933b1c161, + 0xb148db3d0634241810b92df78d18989f25c79f9d081fa13b2607e099cfa15567, + 0xe83faa94b4dd5c3aaef8672f533e1d643c19500b20b55fb4107b97e64409e891, + 0x0ffc052a91b55a90206aa23901761be9e8577ff6277d087c10d54cc611259dc3, + 0xa5bf094556a6542d5508de81a528a2c1c2da3bfc821894f22de933007a4b0291, + 0xa46b655986859b183fa5393c4c6acb74876159a86a797f14646bb85612bbc3ba, + 0x9af491b180b3097896c1ea7164e148b3a2b37fbbc049c2cefe8863faf4779bc0, + 0xa3d2203c4d6578b4680ed2510f7039783a6a771a7b97287a511158c4eb6455a1, + 0xebb8fc983c780bb28891644f360a98b4b954b8a283470f472096360703ae9a63, + 0x358703a00365da3ba05e0244820663d15784ae793772116b24f3201ec799a030, + 0xaacdb433d11409eb98b1db93a04a9c654a6188cb8474c280b4dbd43f386a3f44, + 0x99ab7529556a38449d30181088aa323846c2db45a1d9359ed40d0429a250b660, + 0x15173b2aaa532523606737a1f823258529393d28c9fc213b376207d9c539a2a4, + 0x908aa96230f2c13801a6b36925b4166196373ec7f743031acd723b631232458a, + 0xbaaa019365d48915d62b4f30a1bcee39334cf9959f168e0b6baf63519cd2584c, + 0xe780ca7c280f3c395725b03a0a518353d2b2fddc563ba28ebcc2101153841e5a, + 0x17ae302bbde2b800dbb2bd60ad294439384154967274fe142b437b64a4f0a6a7, + 0xa06c96ac837d488d9868ca00f3bf189ac2172873d65b284a07c3d88ac626da31, + 0x9e534031ccb825ba60c55210638b74a57ac598c550ae17ab4ae272eae28e3b56, + 0x0cd2622734e3661ec325bad6451ae1abe5e748a34c3b14ba7d13fb9bb3705a17, + 0xb704e6d49ba064641bcccb29d27e1544cd1878b37b4944e56527ec854c8d06cd, + 0x30da9614032779b705c40216b4b76333c757b09c8ccf1190471397600356dc74, + 0x22f2f5569de11f6a6542b1e12a8e7277172402204571230a0885c41dc89004e7, + 0xc5cbc2973b9640cf710b72bdf3acfc0550788b296c4249ce30a0be86632b9b97, + 0x3a77b53d363133d007d04a99a879587d155073171bf4992e2d989fab06aa6799, + 0x493b7868c92a58b68b7df4238630da07fe443c49c149beb058d0d6403957be71, + 0xc5475c46c866c1c1859a14301681f772cd780962534153d7e91e39862466e99f, + 0xa8122f376b3f5d355263eba522c43995044beca78b9ba9924b87035490ae78a9, + 0x4d523c7ba588a386eb49bf652fdf12716373187a1ca047cc6138627aaeab8f6c, + 0xebbf87a176b86c9f7f093c8f5b0bdc147399e839ae737038d0bd0142369f9c9d, + 0x46b25b9ae540b80023d5d757e76b3fdd3064dd2b44cd06b44369277147b61565, + 0x4b325044e1bc606fa629055a2e6a4b02b2f1b1aa98a69391c91bd98f1058aa18, + 0xd9019ddbb6dce60a070bad4bec3df37a0d4dda8410288830e9ae509880a02b24, + 0x8e1bba8edb1cc520517c11b64d68cc00c69475a2a2d9c56a2773a02424b2bef1, + 0x7ddfb4c4cc503d05c888946579e4027dbf8a89370c74fa66c8a325c234296399, + 0x4c202fa05179352f92a18630822892151a7b8b163eea685c2c4f026015fee782, + 0xf1c53ca573807afc6bc766be008796fbb906e9e1abd1cc845f60423f0978df89, + 0x924aa118a2b41c7f458308e87b190a27002ba7f773cb65ec87165a6530a0971a, + 0x752069a42afbd271e1e236fc155aeff759ec762551e5bcdf3a66d6a9af92b4ce, + 0x14a29ed410cf72a808e90c81a46074611059802391006c52c5994519718a84f4, + 0x45e8d9c3c6616e0268b2e1d5af48b091c6053b7477740fea361853364de642a4, + 0x4b83364235b6a865037878074b37400c82591794a09055d5b34a9f186e1574cc, + 0xb3848f4b620016d807b945485bc4c9e17644fea65f5345c862d83aa1a4cd1b67, + 0x6409fa545c5712613c267b80447df08c87e532bd77500c14b08d7ac00dc7c2fa, + 0x50b1b5c26d27dca74ad41f9b0761426321a9b3a992a4c3fa151021bc2d17c88f, + 0xaab7274e65cc23d283ab55a951495872455bcce806a9e803c2d9b566a6addebb, + 0x78120ba9361ca9b8b10323f682cc5b9131d44f262501ed861c866c9e31d09789, + 0xf81dc3c773a4464c4cc9c4cb838b9bdb16ff26227a9871c57734b5c59c27e77f, + 0x061a7b56963296f48ae58a85e34063aaf644fee4178b3a9647191c4f022356cc, + 0x5b17e247644a809be0c04ca57df1dbbcaf1c2b1645217a615b98aa048ca48ad7, + 0x254f5b859249066abf6a33d59521b07cc684a1ac23089101c80dfacb82094445, + 0xd3358e6eb6461cf614cbc22248259ed19ab0d6498f3f20c660e9aa5ae877d297, + 0x3611a377b14860f9398408575af51819936883d080218ab0acafbb639a3019a3, + 0x8878a45a1264b30f709c46a3fa5e2d571f8f594d3ba90c432813b78005e1d20b, + 0x72551f87e978fcd8487bb584a4e97a66a058a9a750d15c479919c81ed235803b, + 0x8a657a8e08804f8c109f8dd16074124df22b0c4b276d2ac865b55a538d738262, + 0x26216ba21ec7368f30c638e3f201288a23c2861c3c88599f9027120b0dd7575a, + 0x8855c5411554f699b47ec667a3b2a62f828b2458965130126f29b7525205ef33, + 0x5d4740020a61c9c742aa3be0048eac3aa69b7d9a18846e5498e66b8ed550cdbd, + 0x91bbe0d0482347bfc39964f3f63cf4967ea9321418c377b8262e63225e17621f, + 0xfea466a6335e822059e46a8a5eb16ff321b3a043588c0bb6e5d2b4f3a8c100b0, + 0x5bf2715523433dbab50491216b9cdc2d526aae3bd218404c33beba959719b48c, + 0xc9ae4753512b171c75763b38fb4ddca82750abb505b8c3fc519e7536560d639e, + 0xf2476953b7bd7966c13bd09e8af17a542ab4927151ad4a46e8843c055591e78c, + 0xa8b4e5956822815a3c98eff1b9cc49aea06bcd24f9c70941a3d3f0810de25afc, + 0x154dd76069f2c2c367bb52a2c309ccf1708d514d3f871cc4e3bafe91549b44bb, + 0xf4b24c5525a19bb6abd50c693407851e1a7632883f783a08e5483e7ca7876e4b, + 0x2889417d7ec147e8624e4c83b8bb56bdef29aa47a5735034b48beb8c36c6223f, + 0x184502ecb3f8072d61e41cc8a21784a24be3c652f2d697a5a28ad605cbf0cb1f, + 0x928a25a13a9933700481f341b2a3c279021ed2d701303699aab12df4886303d3, + 0xb3e2949341b577f85ac326284a85f2494976790e762ec51c1a88faa2f5e03c0f, + 0xab44e399735374502f0029cfdb74e9e1517263654262320ff3c15ff48067c701, + 0xdf8436507373fdc7a475f13d961a45718ba1a4b56f02d0095030194a5cb34838, + 0x728387a33a310561e73d18c2af34116384879cfd2c70aae0400eec2bd667c2a4, + 0xc5a051e643c7d8ae8d1bab4352b9bd27b3e647259bb1cccb2304d725cb2e73c6, + 0x718b5abc88800949b2c1d03f159fbf396adca8526f1b476f80fe91c13308d645, + 0x2fd626053c941502e28d796cd655a3cd49df9f15ca02ad626e486f6a4921106b, + 0xf696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68 + ]) + ct = split (join [ + 0x707d18cabcf89670c80003b47d2b8678ad0da4aaad781a3351e82ac3e447e701, + 0x9af5cb86020fb2ac727e79654155835b45de9b8af5e5c7efa01295da8988131d, + 0xc8d6edb0645c3e4116aab080c5a571e760416fe8e299c89811963cf9776e0c82, + 0x8751701f90e26435897f8fdf7a7afaad987009c0eb12fb914dfaab1fce9264f5, + 0x5ee0cb4d89449385dd081b02dace9b179a54513d281529b8fd61c53e3bcfc9e2, + 0xc3ae72339a6197119f97d44b05d3f36a5abe0a3f7ccbdbb91d24b25856462a64, + 0x9b6c1d46ae6e05e999274da9239e674525a522f6141cb95de96b93b39f0f7d09, + 0x0d4b1c0546ef6fc3fd08e90b228f657af31eb933c9cfce634af6bf820d5e185f, + 0x3157efbc926a8ae420f29300513baf30236cc11447e74aed4e262799d77a5cf2, + 0x2b0a7da1264225fcd68cf07670bbf5b04f3173d6142dc9426d9006ddedc5d594, + 0x43a11c8d20453c2867c10434ab6b05b4f0b467b67a4203037c16ea720945de47, + 0x4102e168d5f79d7f530f61d6b7973ed6457e877fb2b45e321ded8ffd30368259, + 0xb3ea60b4cf9d11c5a0087f27ed40d5365c3d0b8ba2e8cdea59afa35149970488, + 0xcea9e07c9434923e96e6a99cf3a0be11016a86dc9eaa539fecbddc6cfd597a28, + 0xaecae2757234340194f4fac7e5a204821382d5928c8e035833c7cad49bba4304, + 0xe826d5c024c7cca2acf95c6cbbd68c3848554a855695c248add50c87dae4a49d, + 0x11cdbc7c757ab1e00b8fd21e7854a897dc21b40f087b3dfb131773d9d87401e5, + 0xd5017ab1f86430f889ff66cc9e04be863e7e38ad527e7644c8ce93d0bc2e255c, + 0xdc3be2d3784ed0c12649f5febbabac0c8e4c917c8bef29775fa3db1ea23feddc, + 0x609539c23354dce722aee71c45407b34da006f24452ea05e766e6b5dcac937ef, + 0x743aa908a7b7cf2f3ed8931c61cdd343dfdf6c588d1b1f4099ba5be53e769109, + 0x9660877463c4310a36767ee27e0dbd3132acf6888421e1012edf383d4eec9643, + 0xe8a10b50e10527c5a1474458b35e54b841fc02599ed07c190154525c47b85e69, + 0xb09e8208dcf36f7e38d9f1090b8daf0a324d7cb48ace08dac11be460585dba90, + 0x61abe7ef724343a4baf1c74090e8d7918648d0ddc43743bc031eec9e3a2912d8, + 0x70f50edcdb6e292456c400006ef65eb2c24e038ca3ddf975e2a2611a8b187e33, + 0xe52aaddc119ef9e6403c61924a7cf229f6619ef9baceee7c04f2675996174c93, + 0x8078f50ccaf6d6580fced01564723d2979b33b77f689951b7c77b650e48a8408, + 0x53932612c080f9b55bfc78de641e0902c5503b2f6cc450664771b94d5590957b, + 0x669ea08b96f368e11eb905427e2650ed185d6003ab704e23889300cdd920060d, + 0x3934b44074783db397172838c9be318b5f892058e67d9ec94019870d758229e6, + 0x3018cd85d4492e0eb8c0a90d3a666e7616ddab331601ec9611572929ee74bce8, + 0xd3bfb8a708858fdbf661bea1f0927f6e5192a86151fd03b001936c82da6d8c14, + 0x7a1af2e91b22a402ce758fd743226a870f3e3635231a390a20c6aee172818979, + 0xdcc4db5e8bd9802bc5c0bffda35c288d027cbade7d615996879a09292bb3ca2c, + 0x9720e741e51959d818c9df6903bb711a93ba67b845397dd1d578c6b937f8c3ee, + 0xe4675046f3c3004ab104a436c551352e70d5179c43ce48c5ee710744de4596b3, + 0xc4cdb12181d0d96ac0ec69aa1451159fabcf3fb8899809aecc4d4f097e86b4b7, + 0x35215c89d13b0dafe75df0020b22bef4973b457f548b4a8998dff79232ec4469, + 0x51aa7ebc92212bae1a06f782be9925a532e10dd02aada8948766c427ed5a5799, + 0x36ebbf5c7a2c9762fdbfe14c70b2c0118378acd644056fec83c774b54867e388, + 0x9c2af117661086aa5abdc1bd1be41c0f66343e0ec517a7a59849b2b5a37a990c, + 0xe4487b098dbdd9178b288411f4373654c873ee8ed018156bb3401153b096f853, + 0xaa14c365b2c3215413ebce8dc07c4bafdd02613e1659056a4d010e970b38dc7e, + 0x10072403d8c9622eebf4030b6ab640f7022d5c2c938c0ca2156bc16164b23206, + 0x63de1f904a5c0d9f63d46eb413081c809af2cbc247d26bb6cb74c58022cbc9b7, + 0xd60b17d03255e736024b6146ab9f1c1c6d648b9fdf256a602b7c469da04bffb6, + 0xb7355728a05308b9336a49a1522d7e7ee0ad2fd2472bb9cf882a4851f5ba5b43, + 0x3def666fb0bfed4358afdf5b6005051e74c16244f4579288a0da8c2f49598f74 + ]) + ss = split 0x23f211b84a6ee20c8c29f6e5314c91b414e940513d380add17bd724ab3a13a52 From cbf9ea92501624246cdd54e0189d50b6bb200967 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Thu, 3 Oct 2024 16:24:09 -0400 Subject: [PATCH 6/6] mlkem: add copyright notices #148 --- Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry | 5 ++++- Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM1024.cry | 3 +++ Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry | 3 +++ Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM768.cry | 3 +++ Primitive/Asymmetric/Cipher/ML_KEM/Tests/kat.awk | 4 ++++ 5 files changed, 17 insertions(+), 1 deletion(-) diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry index 8f116605..bbd61f42 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry @@ -1,3 +1,6 @@ - +/** + * @copyright Galois Inc + * @author Marios Georgiou + */ module Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM where import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM512 diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM1024.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM1024.cry index a4ef0318..7a23c85a 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM1024.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM1024.cry @@ -3,6 +3,9 @@ * * These are sourced from the Post Quantum Cryptography KAT repo: * @see https://github.com/post-quantum-cryptography/KAT/tree/main/MLKEM + * + * @copyright Galois Inc + * @author Marcella Hastings */ import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM1024 as ML_KEM diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry index b6e9a64e..d994c3df 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry @@ -3,6 +3,9 @@ * * These are sourced from the Post Quantum Cryptography KAT repo: * @see https://github.com/post-quantum-cryptography/KAT/tree/main/MLKEM + * + * @copyright Galois Inc + * @author Marcella Hastings */ import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM512 as ML_KEM diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM768.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM768.cry index 10e81e28..59421df6 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM768.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM768.cry @@ -3,6 +3,9 @@ * * These are sourced from the Post Quantum Cryptography KAT repo: * @see https://github.com/post-quantum-cryptography/KAT/tree/main/MLKEM + * + * @copyright Galois Inc + * @author Marcella Hastings */ import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM768 as ML_KEM diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/kat.awk b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/kat.awk index 32a26a97..c22665f8 100755 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/kat.awk +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/kat.awk @@ -1,6 +1,10 @@ # Create a batch file from ML-KEM known answer tests # The input is the *.rsp file. # Example input file: https://raw.githubusercontent.com/post-quantum-cryptography/KAT/main/MLKEM/kat_MLKEM_512.rsp +# +# @copyright Galois, Inc +# @author Marios Georgiou +# BEGIN { print ":load ml_kem.cry" }