From e9f257606a2729c17d46ed67cf1b63204270579d Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Tue, 22 Oct 2024 10:54:25 -0400 Subject: [PATCH 1/8] mlkem: tweak rounding property #144 --- Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry index e772ca1..aa5ba2c 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry @@ -128,8 +128,14 @@ BitsToBytes input = map reverse (groupBy input) BytesToBits : {ell} (fin ell, ell > 0) => [ell]Byte -> [ell*8]Bit BytesToBits input = join (map reverse input) -// In Cryptol, rounding is computed via the built-in function roundAway -property rounding = ((roundAway(1.5) == 2) && (roundAway(1.4) == 1)) +/** + * In Cryptol, rounding is computed via the built-in function `roundAway`. + * [FIPS-203] Section 2.3. + */ +property roundingWorks y = y >= 0 ==> roundUpWorks && roundDownWorks where + y' = fromInteger y + roundUpWorks = roundAway (y' + 0.5) == (y + 1) + roundDownWorks = roundAway (y' + 0.4) == y /** * Compression from an integer mod `q` to an integer mod `2^d`. From 0eb75d1e50c6cb6a69eb2573559650c529905ad0 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Tue, 22 Oct 2024 11:16:35 -0400 Subject: [PATCH 2/8] mlkem: expand docs on compression #144 --- .../Cipher/ML_KEM/Specification.cry | 22 ++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry index aa5ba2c..2442ad1 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry @@ -138,18 +138,30 @@ property roundingWorks y = y >= 0 ==> roundUpWorks && roundDownWorks where roundDownWorks = roundAway (y' + 0.4) == y /** - * Compression from an integer mod `q` to an integer mod `2^d`. + * Compress an integer mod `q` into an integer mod `2^d`. * [FIPS-203] Section 4.2.1, Equation 4.7. */ -Compress'' : {d} (d < lg2 q) => Z q -> [d] -Compress'' x = fromInteger(roundAway(((2^^`d)/.`q) * fromInteger(fromZ(x))) % 2^^`d) +Compress'' : {d} (d < 12) => Z q -> [d] +Compress'' x = y where + // Convert from an integer mod `q` to a rational number. + x' = fromInteger (fromZ x) : Rational + // Compress. Note that `/.` denotes division of rationals. + y' = roundAway (((2^^`d) /. `q) * x') + // mod 2^^d (by converting from an integer to a d-bit vector). + y = (fromInteger y') : [d] /** - * Decompression from an integer mod `2^d` to an integer mod `q`. + * Decompress an integer mod `2^d` into an integer mod `q`. * [FIPS-203] Section 4.2.1, Equation 4.8. */ Decompress'' : {d} (d < lg2 q) => [d] -> Z q -Decompress'' x = fromInteger(roundAway(((`q)/.(2^^`d))*fromInteger(toInteger(x)))) +Decompress'' y = x where + // Convert from a d-length bit vector to a rational number. + y' = fromInteger (toInteger y) : Rational + // Decompress! As before, `/.` is division of rationals. + x' = roundAway((`q /. (2^^`d)) * y') + // Convert from an integer to an integer mod `q`. + x = (fromInteger x') : Z q /** * When `d` is large, compression followed by decompression must not From 9bdb16c044748df52a6226b4fb3be7845c760c91 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Tue, 22 Oct 2024 12:28:26 -0400 Subject: [PATCH 3/8] mlkem: clean up properties for compression #144 --- .../Cipher/ML_KEM/Specification.cry | 42 ++++++++++++++----- 1 file changed, 32 insertions(+), 10 deletions(-) diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry index 2442ad1..aac8a3b 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry @@ -141,7 +141,7 @@ property roundingWorks y = y >= 0 ==> roundUpWorks && roundDownWorks where * Compress an integer mod `q` into an integer mod `2^d`. * [FIPS-203] Section 4.2.1, Equation 4.7. */ -Compress'' : {d} (d < 12) => Z q -> [d] +Compress'' : {d} (d < width q) => Z q -> [d] Compress'' x = y where // Convert from an integer mod `q` to a rational number. x' = fromInteger (fromZ x) : Rational @@ -154,7 +154,7 @@ Compress'' x = y where * Decompress an integer mod `2^d` into an integer mod `q`. * [FIPS-203] Section 4.2.1, Equation 4.8. */ -Decompress'' : {d} (d < lg2 q) => [d] -> Z q +Decompress'' : {d} (d < width q) => [d] -> Z q Decompress'' y = x where // Convert from a d-length bit vector to a rational number. y' = fromInteger (toInteger y) : Rational @@ -163,22 +163,44 @@ Decompress'' y = x where // Convert from an integer to an integer mod `q`. x = (fromInteger x') : Z q +/** + * Compression inverts decompression for all inputs and bit lengths. + * We'll prove it for the bit lengths found in the + * ```repl + * :prove CompressInvertsDecompress`{1} + * :prove CompressInvertsDecompress`{d_u} + * :prove CompressInvertsDecompress`{d_v} + * ``` + */ +CompressInvertsDecompress : {d} (d < width q) => [d] -> Bit +property CompressInvertsDecompress y = Compress'' (Decompress'' y) == y + /** * When `d` is large, compression followed by decompression must not * significantly alter the value. + * This sets `d = d_u`, which is the largest value for `d` used in the + * spec. * [FIPS-203] Section 4.2.1, "Compression and Decompression". + * ```repl + * :prove DecompressMostlyInvertsCompress + * ``` */ -CorrectnessCompress : Z q -> Bit -property CorrectnessCompress x = err <= B_q`{d_u} where - x' = Decompress''`{d_u}(Compress''`{d_u}(x)) - err = abs(modpm(x'-x)) - +DecompressMostlyInvertsCompress : Z q -> Bit +property DecompressMostlyInvertsCompress x = errIsSmallEnough where + x' = Decompress''`{d_u} (Compress''`{d_u} x) + err = abs (modpm (x' - x)) + errIsSmallEnough = err <= B_q`{d_u} + + // The spec doesn't describe formally what "not significantly altered" + // means; we use this equation. B_q : {d} (d < lg2 q) => Integer B_q = roundAway((`q/.(2^^(`d+1)))) - modpm : {alpha} (fin alpha, alpha > 0) => Z alpha -> Integer - modpm r = if r' > (`alpha / 2) then r' - `alpha else r' - where r' = fromZ(r) + // Convert an integer mod `q` to a representation centered around 0 + // (and represented as an `Integer`). + modpm : Z q -> Integer + modpm r = if r' > (`q / 2) then r' - `q else r' + where r' = fromZ r /** * Compression applied to a vector is equivalent to applying compression to From 9eec5ad9e12fe63e736d8adb23140345140759c1 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Tue, 22 Oct 2024 12:33:44 -0400 Subject: [PATCH 4/8] mlkem: rename compression functions with types #144 Replaces tick marks with explicit denotations of what dimension the input and output are. --- .../Cipher/ML_KEM/Specification.cry | 44 +++++++++---------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry index aac8a3b..984f705 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry @@ -141,8 +141,8 @@ property roundingWorks y = y >= 0 ==> roundUpWorks && roundDownWorks where * Compress an integer mod `q` into an integer mod `2^d`. * [FIPS-203] Section 4.2.1, Equation 4.7. */ -Compress'' : {d} (d < width q) => Z q -> [d] -Compress'' x = y where +Compress : {d} (d < width q) => Z q -> [d] +Compress x = y where // Convert from an integer mod `q` to a rational number. x' = fromInteger (fromZ x) : Rational // Compress. Note that `/.` denotes division of rationals. @@ -154,8 +154,8 @@ Compress'' x = y where * Decompress an integer mod `2^d` into an integer mod `q`. * [FIPS-203] Section 4.2.1, Equation 4.8. */ -Decompress'' : {d} (d < width q) => [d] -> Z q -Decompress'' y = x where +Decompress : {d} (d < width q) => [d] -> Z q +Decompress y = x where // Convert from a d-length bit vector to a rational number. y' = fromInteger (toInteger y) : Rational // Decompress! As before, `/.` is division of rationals. @@ -173,7 +173,7 @@ Decompress'' y = x where * ``` */ CompressInvertsDecompress : {d} (d < width q) => [d] -> Bit -property CompressInvertsDecompress y = Compress'' (Decompress'' y) == y +property CompressInvertsDecompress y = Compress (Decompress y) == y /** * When `d` is large, compression followed by decompression must not @@ -187,7 +187,7 @@ property CompressInvertsDecompress y = Compress'' (Decompress'' y) == y */ DecompressMostlyInvertsCompress : Z q -> Bit property DecompressMostlyInvertsCompress x = errIsSmallEnough where - x' = Decompress''`{d_u} (Compress''`{d_u} x) + x' = Decompress`{d_u} (Compress`{d_u} x) err = abs (modpm (x' - x)) errIsSmallEnough = err <= B_q`{d_u} @@ -207,32 +207,32 @@ property DecompressMostlyInvertsCompress x = errIsSmallEnough where * each individual element. * [FIPS-203] Section 2.4.8, Equation 2.15. */ -Compress' : {d} (d < lg2 q) => Z_q_256 -> [n][d] -Compress' x = map Compress''`{d} x +Compress_Vec : {d} (d < lg2 q) => Z_q_256 -> [n][d] +Compress_Vec x = map Compress`{d} x /** * Decompression applied to a vector is equivalent to applying decompression to * each individual element. * [FIPS-203] Section 2.4.8. */ -Decompress' : {d} (d < lg2 q) => [n][d] -> Z_q_256 -Decompress' x = map Decompress''`{d} x +Decompress_Vec : {d} (d < lg2 q) => [n][d] -> Z_q_256 +Decompress_Vec x = map Decompress`{d} x /** - * Compression applied to an array is equivalent to applying compression to + * Compression applied to a matrix is equivalent to applying compression to * each individual element. * [FIPS-203] Section 2.4.8. */ -Compress : {d, k1} (d < lg2 q, fin k1) => [k1]Z_q_256 -> [k1][n][d] -Compress x = map Compress'`{d} x +Compress_Mat : {d, k1} (d < lg2 q, fin k1) => [k1]Z_q_256 -> [k1][n][d] +Compress_Mat x = map Compress_Vec`{d} x /** - * Decompression applied to an array is equivalent to applying decompression to + * Decompression applied to a matrix is equivalent to applying decompression to * each individual element. * [FIPS-203] Section 2.4.8. */ -Decompress : {d, k1} (d < lg2 q, fin k1) => [k1][n][d] -> [k1]Z_q_256 -Decompress x = map Decompress'`{d} x +Decompress_Mat : {d, k1} (d < lg2 q, fin k1) => [k1][n][d] -> [k1]Z_q_256 +Decompress_Mat x = map Decompress_Vec`{d} x private /** @@ -1004,13 +1004,13 @@ private submodule K_PKE where // Step 19. u = NTTInv (dotMatVec (transpose A_hat) y_hat) + e1 // Step 20. - mu = Decompress'`{1} (ByteDecode`{1} m) + mu = Decompress_Vec`{1} (ByteDecode`{1} m) // Step 21. v = (NTTInv' (dotVecVec t_hat y_hat)) + e2 + mu // Step 22. - c1 = ByteEncode_Vec`{d_u} (Compress`{d_u} u) + c1 = ByteEncode_Vec`{d_u} (Compress_Mat`{d_u} u) // Step 23. - c2 = ByteEncode`{d_v} (Compress'`{d_v} v) + c2 = ByteEncode`{d_v} (Compress_Vec`{d_v} v) // Step 24. c = c1 # c2 @@ -1030,15 +1030,15 @@ private submodule K_PKE where // Step 2. c2 = c @@[32 * d_u * k .. 32 * (d_u * k + d_v) - 1] // Step 3.j - u' = Decompress`{d_u} (ByteDecode_Vec`{d_u} c1) + u' = Decompress_Mat`{d_u} (ByteDecode_Vec`{d_u} c1) // Step 4. - v' = Decompress'`{d_v} (ByteDecode`{d_v} c2) + v' = Decompress_Vec`{d_v} (ByteDecode`{d_v} c2) // Step 5. s_hat = ByteDecode12_Vec dkPKE // Step 6. w = v' - NTTInv' (dotVecVec s_hat (NTT u')) // Step 7. - m = ByteEncode`{1} (Compress'`{1} w) + m = ByteEncode`{1} (Compress_Vec`{1} w) /** * The K-PKE scheme must satisfy the basic properties of an encryption From 40886cd601b956161ab2547bc591f1b8abe18233 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Tue, 22 Oct 2024 14:23:56 -0400 Subject: [PATCH 5/8] mlkem: add bit-to-byte conversion properties #144 --- .../Cipher/ML_KEM/Specification.cry | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry index 984f705..056d767 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry @@ -128,6 +128,34 @@ BitsToBytes input = map reverse (groupBy input) BytesToBits : {ell} (fin ell, ell > 0) => [ell]Byte -> [ell*8]Bit BytesToBits input = join (map reverse input) +/** + * The conversions between bits and bytes are each others' inverses. + * [FIPS-203] Section 4.2.1 (see description on Algorithm 4). + * The sample `ell` values here are a subset of the possible values in the spec. + * ```repl + * :prove B2B2BInverts`{32} + * :prove B2B2BInverts`{192} + * :prove B2B2BInverts`{384} + * ``` + */ +B2B2BInverts : {ell} (fin ell, ell > 0) => [ell * 8] -> Bit +B2B2BInverts bits = bitsWorks && bytesWorks where + bitsWorks = BytesToBits (BitsToBytes bits) == bits + bytesWorks = BitsToBytes (BytesToBits (split bits)) == split bits + +/** + * This currently fails due to endianness issues! + * Check the example given in the spec for converting between bits and bytes. + * [FIPS-203] Section 4.2.1 "Converting between bits and bytes." + * + * Note: The `reverse` here is needed because Cryptol's default representation + * for byte arrays, including literal values like "139", is big-endian. + * ```repl + * :prove B2BExampleWorks + * ``` + */ + B2BExampleWorks = BitsToBytes 0b11010001 == [reverse 139] + /** * In Cryptol, rounding is computed via the built-in function `roundAway`. * [FIPS-203] Section 2.3. From 23d2d89fa72c166f5cb7846759b7f42d3e50831a Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Tue, 22 Oct 2024 14:24:14 -0400 Subject: [PATCH 6/8] mlkem: make b2b look more like spec #144 Changes implementation details of BytesToBits and BitsToBytes --- .../Cipher/ML_KEM/Specification.cry | 52 +++++++++++++++---- 1 file changed, 43 insertions(+), 9 deletions(-) diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry index 056d767..73265e8 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry @@ -115,18 +115,55 @@ XOF : ([34]Byte) -> [inf]Byte XOF(d) = groupBy (SHAKE128::xof (join d)) /** - * Conversion from bit arrays to byte arrays. + * Conversion from little-endian bit arrays to byte arrays. * [FIPS-203] Section 4.2.1, Algorithm 3. */ -BitsToBytes : {ell} (fin ell, ell > 0) => [ell*8]Bit -> [ell]Byte -BitsToBytes input = map reverse (groupBy input) +BitsToBytes : {ell} (fin ell) => [8 * ell]Bit -> [ell]Byte +BitsToBytes b + | ell == 0 => zero + | ell > 0 => B where + // Group the bits into the B[⌊i / 8⌋] sets; pad them to support + // subsequent operations, and correlate each bit with its index `i`. + b' = groupBy`{8} [(zext [bi], i) + | bi <- b + | i <- [0..8 * ell - 1]] + + // Steps 2-4. + B = [sum [bi * (2 ^^ (i % 8)) + | (bi, i) <- bi8] + | bi8 <- b'] /** * Conversion from byte arrays to bit arrays. * [FIPS-203] Section 4.2.1, Algorithm 4. */ -BytesToBits : {ell} (fin ell, ell > 0) => [ell]Byte -> [ell*8]Bit -BytesToBits input = join (map reverse input) +BytesToBits : {ell} (fin ell) => [ell]Byte -> [ell*8]Bit +BytesToBits C + | ell == 0 => [] + | ell > 0 => join [[ b8ij where + // Step 4. Taking the last bit is the same as modding by 2. + b8ij = Ci' ! 0 + // Step 5. Shifting right is the same as the iterative + // division (see `div2IsShiftR`). This accounts for all the + // divisions "up to this point" (e.g. none when `j = 0`), which + // is why we use `Ci'` to evaluate `b8ij` above. + Ci' = Ci >> j + // Step 3. + | j <- [0..7]] + // Step 2. We iterate over `C` directly instead of indexing into it. + | Ci <- C ] + +/** + * The iterative division by 2 in `BytesToBits` is the same as shifting right. + * ```repl + * :prove div2IsShiftR + * ``` + */ +div2IsShiftR : Byte -> Bit +div2IsShiftR C = take (d2 C) == shl where + // Note: division here is floor'd by default. + d2 c = [c] # d2 (c / 2) + shl = [C >> j | j <- [0..7]] /** * The conversions between bits and bytes are each others' inverses. @@ -147,14 +184,11 @@ B2B2BInverts bits = bitsWorks && bytesWorks where * This currently fails due to endianness issues! * Check the example given in the spec for converting between bits and bytes. * [FIPS-203] Section 4.2.1 "Converting between bits and bytes." - * - * Note: The `reverse` here is needed because Cryptol's default representation - * for byte arrays, including literal values like "139", is big-endian. * ```repl * :prove B2BExampleWorks * ``` */ - B2BExampleWorks = BitsToBytes 0b11010001 == [reverse 139] +B2BExampleWorks = BitsToBytes 0b11010001 == [139] /** * In Cryptol, rounding is computed via the built-in function `roundAway`. From 78a089977522e7f9ba0fe56ce34a986f258a63df Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Fri, 1 Nov 2024 12:37:13 -0400 Subject: [PATCH 7/8] mlkem: switch `prove` to `exhaust` #144 This is to support different z3 versions, some of which don't prove the property in a reasonable amount of time. However since it's exhaustable we can do that equivalently. --- Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry index 73265e8..4915ee7 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry @@ -230,8 +230,8 @@ Decompress y = x where * We'll prove it for the bit lengths found in the * ```repl * :prove CompressInvertsDecompress`{1} - * :prove CompressInvertsDecompress`{d_u} - * :prove CompressInvertsDecompress`{d_v} + * :exhaust CompressInvertsDecompress`{d_u} + * :exhaust CompressInvertsDecompress`{d_v} * ``` */ CompressInvertsDecompress : {d} (d < width q) => [d] -> Bit @@ -244,7 +244,7 @@ property CompressInvertsDecompress y = Compress (Decompress y) == y * spec. * [FIPS-203] Section 4.2.1, "Compression and Decompression". * ```repl - * :prove DecompressMostlyInvertsCompress + * :exhaust DecompressMostlyInvertsCompress * ``` */ DecompressMostlyInvertsCompress : Z q -> Bit From d50c74d9f6d0ab9b5db0dd6c829d2d75206747a1 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Fri, 1 Nov 2024 12:40:11 -0400 Subject: [PATCH 8/8] mlkem: add reference to helper property #144 --- Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry index 4915ee7..72c6298 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry @@ -141,7 +141,8 @@ BytesToBits : {ell} (fin ell) => [ell]Byte -> [ell*8]Bit BytesToBits C | ell == 0 => [] | ell > 0 => join [[ b8ij where - // Step 4. Taking the last bit is the same as modding by 2. + // Step 4. Taking the last bit is the same as modding by 2. (See + // `mod2IsFinalBit`). b8ij = Ci' ! 0 // Step 5. Shifting right is the same as the iterative // division (see `div2IsShiftR`). This accounts for all the