Merge pull request #150 from GaloisInc/148-add-mlkem-kats

Add ML-KEM KATs
GaloisInc · Oct 4, 2024 · 972b6a7 · 972b6a7
2 parents 7468d17 + cbf9ea9
commit 972b6a7
Show file tree

Hide file tree

Showing 15 changed files with 609 additions and 48 deletions.
diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/ml_kem.cry b/Primitive/Asymmetric/Cipher/ML-KEM/ml_kem.cry
diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/ml_kem1024.cry b/Primitive/Asymmetric/Cipher/ML-KEM/ml_kem1024.cry
diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/ml_kem512.cry b/Primitive/Asymmetric/Cipher/ML-KEM/ml_kem512.cry
diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/ml_kem768.cry b/Primitive/Asymmetric/Cipher/ML-KEM/ml_kem768.cry
diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry
@@ -0,0 +1,6 @@
+/**
+ * @copyright Galois Inc
+ * @author Marios Georgiou <[email protected]>
+ */
+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
@@ -0,0 +1,15 @@
+/*
+ * @copyright Galois, Inc
+ * @author Marios Georgiou <[email protected]>
+ *
+ * @copyright Amazon.com or its affiliates.
+ * @editor Rod Chapman <[email protected]>
+ */
+module Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM1024 =
+    Primitive::Asymmetric::Cipher::ML_KEM::Specification where
+
+type k = 4
+type eta_1 = 2
+type eta_2 = 2
+type d_u = 11
+type d_v = 5
diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM512.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM512.cry
@@ -0,0 +1,16 @@
+/*
+ * @copyright Galois, Inc
+ * @author Marios Georgiou <[email protected]>
+ *
+ * @copyright Amazon.com or its affiliates.
+ * @editor Rod Chapman <[email protected]>
+ */
+
+module Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM512 =
+    Primitive::Asymmetric::Cipher::ML_KEM::Specification where
+
+type k = 2
+type eta_1 = 3
+type eta_2 = 2
+type d_u = 10
+type d_v = 4
diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM768.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM768.cry
@@ -0,0 +1,15 @@
+/*
+ * @copyright Galois, Inc
+ * @author Marios Georgiou <[email protected]>
+ *
+ * @copyright Amazon.com or its affiliates.
+ * @editor Rod Chapman <[email protected]>
+ */
+module Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM768 =
+    Primitive::Asymmetric::Cipher::ML_KEM::Specification where
+
+type k = 3
+type eta_1 = 2
+type eta_2 = 2
+type d_u = 10
+type d_v = 4
diff --git a/...etric/Cipher/ML-KEM/NIST.FIPS.203.ipd.pdf → ...etric/Cipher/ML_KEM/NIST.FIPS.203.ipd.pdf b/...etric/Cipher/ML-KEM/NIST.FIPS.203.ipd.pdf → ...etric/Cipher/ML_KEM/NIST.FIPS.203.ipd.pdf
diff --git a/Primitive/Asymmetric/Cipher/ML-KEM/README.md → Primitive/Asymmetric/Cipher/ML_KEM/README.md b/Primitive/Asymmetric/Cipher/ML-KEM/README.md → Primitive/Asymmetric/Cipher/ML_KEM/README.md
diff --git a/...symmetric/Cipher/ML-KEM/specification.cry → ...symmetric/Cipher/ML_KEM/Specification.cry b/...symmetric/Cipher/ML-KEM/specification.cry → ...symmetric/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 <[email protected]>
 */
-module specification where
+module Primitive::Asymmetric::Cipher::ML_KEM::Specification where
 
 type q = 3329
 

diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM1024.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM1024.cry
diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry
@@ -0,0 +1,140 @@
+/*
+ * 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
+ *
+ * @copyright Galois Inc
+ * @author Marcella Hastings <[email protected]>
+ */
+
+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