From 00cd3973c914b29c913ee5601fad8299ca4b3808 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Wed, 9 Oct 2024 10:26:04 -0400 Subject: [PATCH 1/3] fix several incorrectly-formed `repl` tests --- Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry | 1 + Primitive/Symmetric/Cipher/Block/AES_specification.cry | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry b/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry index 9db5af86..819b972b 100644 --- a/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry +++ b/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry @@ -208,6 +208,7 @@ publicKey d = EC::scmul (fromZ d) EC::G * [FIPS-186-5] Section 3.3. * ```repl * :check signAndVerifyIsCorrect`{64} + * ``` */ signAndVerifyIsCorrect : {m} (fin m, width m < 64) => [m] -> Z EC::n -> Z EC::n -> Bool property signAndVerifyIsCorrect M d k = verification diff --git a/Primitive/Symmetric/Cipher/Block/AES_specification.cry b/Primitive/Symmetric/Cipher/Block/AES_specification.cry index 40317c31..5ea9b5f8 100644 --- a/Primitive/Symmetric/Cipher/Block/AES_specification.cry +++ b/Primitive/Symmetric/Cipher/Block/AES_specification.cry @@ -44,7 +44,7 @@ encrypt k = encryptWithSchedule (keyExpansion k) decrypt : [KeySize] -> [BlockSize] -> [BlockSize] decrypt k = decryptWithSchedule (keyExpansion k) -/* +/** * This property must be true for each instantiation. * With high probability, it will be extremely slow to prove. * From 14dff285d922b1ef1c834b2b9a06a5f4d457abe5 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Wed, 11 Sep 2024 09:38:06 -0400 Subject: [PATCH 2/3] sha3: make state flattening more obvious #138 --- Primitive/Keyless/Hash/keccak.cry | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/Primitive/Keyless/Hash/keccak.cry b/Primitive/Keyless/Hash/keccak.cry index 1c5e01a7..0f5f027f 100644 --- a/Primitive/Keyless/Hash/keccak.cry +++ b/Primitive/Keyless/Hash/keccak.cry @@ -115,16 +115,36 @@ private /** * Convert a string into a state array. * [FIPS-202] Section 3.1.2. + * + * Note: The spec describes this in terms of all three coordinates + * `(x, y, z)`. Since the lanes determined by a pair `(x, y)` are composed + * of consecutive bits, we don't index into them separately; instead, we + * separate `S` into 25 lanes of length `w` and then place those lanes in + * the correct order according to the `(x, y)` coordinates. + * For ease of implementation of the subsequent step mappings, the bits of + * each lane are reversed. */ unflatten : [b] -> State - unflatten p = transpose (groupBy`{5} (reverse (groupBy`{w} (reverse p)))) + unflatten S = [[ Lanes@((5 * y + x)) + | y <- [0..4]] + | x <- [0..4]] where + Lanes = map reverse (split`{25} S) /** * Convert a state array into a string. * [FIPS-202] Section 3.1.3. */ - flatten : State -> [5 * 5 * w] - flatten A = reverse (join (reverse (join (transpose A)))) + flatten : State -> [b] + flatten A = S where + // No explicit appending or joining is needed to compute the Lanes. + // But we do need to accomodate the lane reversal that happened in the + // inverse `unflatten` function. + Lanes = [[ reverse (A@i@j) + | j <- [0..4]] + | i <- [0..4]] + Planes = [ Lanes@0@j # Lanes@1@j # Lanes@2@j # Lanes@3@j # Lanes@4@j + | j <- [0..4]] + S = join Planes /** * One of the step mappings that's part of a round of Keccak-p. @@ -145,7 +165,6 @@ private | y <- [0..4]] | x <- [0..4] ] - /** * One of the step mappings that's part of a round of Keccak-p. * From d8c0b210ead69ffa1ed69fc45164efe1382dc94d Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Tue, 15 Oct 2024 10:55:55 -0400 Subject: [PATCH 3/3] sha3: add no-index flattening #138 - adds equivalence properties - replaces uses --- Primitive/Keyless/Hash/keccak.cry | 32 +++++++++++++++++++++++++++++-- 1 file changed, 30 insertions(+), 2 deletions(-) diff --git a/Primitive/Keyless/Hash/keccak.cry b/Primitive/Keyless/Hash/keccak.cry index 0f5f027f..8baade60 100644 --- a/Primitive/Keyless/Hash/keccak.cry +++ b/Primitive/Keyless/Hash/keccak.cry @@ -130,6 +130,20 @@ private | x <- [0..4]] where Lanes = map reverse (split`{25} S) + /** + * Convert a string into a state array, but without indexing. + * Equivalent to [FIPS-202] Section 3.1.2. + */ + unflatten_noindex : [b] -> State + unflatten_noindex S = transpose (groupBy (reverse (groupBy`{w} (reverse S)))) + + /** + * ```repl + * :prove unflattens_match + * ``` + */ + property unflattens_match S = unflatten S == unflatten_noindex S + /** * Convert a state array into a string. * [FIPS-202] Section 3.1.3. @@ -146,6 +160,20 @@ private | j <- [0..4]] S = join Planes + /** + * Convert a state array into a string, but without indexing. + * Equivalent to [FIPS-202] Section 3.1.3. + */ + flatten_noindex : State -> [b] + flatten_noindex A = reverse (join (reverse (join (transpose A)))) + + /** + * ```repl + * :prove flattens_match + * ``` + */ + property flattens_match A = flatten A == flatten_noindex A + /** * One of the step mappings that's part of a round of Keccak-p. * @@ -378,11 +406,11 @@ private // The round transformation is defined in [FIPS-202] Section 3.3. Rnd A ir = ι (χ (π (ρ_hardcoded (θ A)))) ir // Step 1. - A0 = unflatten S + A0 = unflatten_noindex S // Step 2. rounds = [A0] # [ Rnd A ir | A <- rounds | ir <- [0..nr - 1]] // Step 3. - S' = flatten (rounds ! 0) + S' = flatten_noindex (rounds ! 0) /** * See https://keccak.team/files/Keccak-reference-3.0.pdf, Section 1.2