Skip to content

Commit

Permalink
Merge pull request #141 from GaloisInc/138-clarify-round-functions
Browse files Browse the repository at this point in the history 
SHA3: clean up round functions
  • Loading branch information
@marsella
marsella authored Sep 30, 2024
2 parents 2227e5b + a44273c commit 7468d17
Showing 1 changed file with 166 additions and 86 deletions.
252 changes: 166 additions & 86 deletions Primitive/Keyless/Hash/keccak.cry
View file
Original file line number Diff line number Diff line change
Expand Up @@ -129,96 +129,195 @@ private
/**
* One of the step mappings that's part of a round of Keccak-p.
*
* The effect of this mapping is to XOR each bit in the state with the
* parity of two columns in the array. `C` computes the parities, `D`
* combines two of the parities for each column, and `A'` completes the
* transformation.
* [FIPS-202] Section 3.2.1.
*/
θ : State -> State
θ A = A' where
C = [ xor a | a <- A ]
D = [ C @ x ^ (C @ y <<< 1)
// In the spec, this is denoted `(x-1) mod 5` for 0 <= x < 5.
| (x:[8]) <- [4,0,1,2,3]
// In the spec, this is denoted `(x+1) mod 5` for 0 <= x < 5.
| (y:[8]) <- [1,2,3,4,0]
]
A' = [ [ a ^ (D @ x) | a <- A @ x ] | (x:[8]) <- [0 .. 4] ]

xor : {a, l} (fin a) => [a][l] -> [l]
xor xs = xors ! 0
where xors = [zero] # [ x ^ z | x <- xs | z <- xors ]
C = [ A@x@0 ^ A@x@1 ^ A@x@2 ^ A@x@3 ^ A@x@4
| x <- [0..4]]
D = [ C @ ((x - 1) % 5) ^ (C @ ((x + 1) % 5) <<< 1)
| x <- [0..4]]
A' = [[ A@x@y ^ D@x
| y <- [0..4]]
| x <- [0..4] ]


/**
* One of the step mappings that's part of a round of Keccak-p.
*
* The effect of this mapping is to rotate the bits of each lane by a
* an _offset_ (computed in `set_lane`) that depends on the `x` and `y`
* coordinates of that lane.
* [FIPS-202] Section 3.2.2.
*/
ρ : State -> State
ρ A = groupBy`{5} [ a <<< r | a <- join A | (r:[8]) <- R ]
where
R = [
00, 36, 03, 41, 18,
01, 44, 10, 45, 02,
62, 06, 43, 15, 61,
28, 55, 25, 21, 56,
27, 20, 39, 08, 14
]
ρ A = A' where
// Step 1.
A1 = [[ if (x == 0) && (y == 0) then A@0@0 else zero
| y <- [0..4]]
| x <- [0..4]]
// Step 2-3.
As = [((1,0), A1)] #
[ ((y, (2*x + 3*y) % 5), set_lane x y t Ai)
| ((x, y), Ai) <- As
| t <- [0..23]]
(_, A') = As ! 0

// Step 3a. Update the lane defined by x' and y'.
set_lane x' y' t Ai = [[
if (x' == x) && (y' == y) then A@x@y <<< ((t+1)*(t+2)/2)
else Ai@x@y
| y <- [0..4]]
| x <- [0..4]]

/**
* Optimized and hard-coded version of `ρ`.
*
* This optimizes the hard-codable parts of `ρ` in the following ways:
* - Pre-computes the offsets `(t+1)*(t+2) / 2`
* - Pre-computes the corresponding sequence of lane indexes (e.g. the
* series defined by `(y, (2x + 3y) % 5))`
* - Re-orders the offsets and the lane indexes to be in the same order
* that we get if we iterate over the lanes generated by `join A` (e.g.
* (0,0), (0,1), (0,2), ...)
* - Maps directly over A, rotating each lane by the expected offset,
* instead of iteratively updating the lanes
*
* This provides a 2x speedup.
*
* Equivalent to [FIPS-202] Section 3.2.2, Algorithm 2.
*/
ρ_hardcoded : State -> State
ρ_hardcoded A = A' where
A' = groupBy [ a <<< offset | a <- join A | offset <- t_offsets]

// This is technically equivalent to Table 2, but we index in the
// "normal" way e.g. the top-left corner is (0, 0) and the bottom-right
// is (4, 4), unlike the the table.
// We also write these in hex instead of base-10.
t_offsets = [
0x000, 0x024, 0x003, 0x069, 0x0d2,
0x001, 0x12c, 0x00a, 0x02d, 0x042,
0x0be, 0x006, 0x0ab, 0x00f, 0x0fd,
0x01c, 0x037, 0x099, 0x015, 0x078,
0x05b, 0x114, 0x0e7, 0x088, 0x04e
]

/**
* Prove that the hardcoded version of `ρ` is correct.
* ```repl
* :prove hardcoded_rho_is_correct
* ```
*/
property hardcoded_rho_is_correct A = ρ A == ρ_hardcoded A

/**
* One of the step mappings that's part of a round of Keccak-p.
*
* The effect of this mapping is to rearrange the position of the lanes,
* based on an offset of the `x` and `y` coordinates.
* [FIPS-202] Section 3.2.3.
*/
π : State -> State
π A = groupBy`{5} [ A @ ((x + 3*y) % 5) @ x
| (x:[8]) <- [0..4], (y:[8]) <- [0..4]
]
π A = [[ A @((x + 3 * y) % 5) @x
| y <- [0..4]]
| x <- [0..4]]

/**
* One of the step mappings that's part of a round of Keccak-p.
*
* The effect of this mapping is to XOR each bit with a non-linear function
* of two other bits in its row.
* [FIPS-202] Section 3.2.4.
*
* Note: in the first line, XOR 1 on a single bit is equivalent to bitwise
* NOT. Since we operate over the whole slice defined by each z-coordinate,
* it's nicer to use `~`. You can see the NOT gates in Figure 6.
*/
χ : State -> State
χ A = groupBy`{5} [ (A @ x @ y) ^ (~ A @ ((x + 1) % 5) @ y
&& A @ ((x + 2) % 5) @ y)
| (x:[8]) <- [0..4], (y:[8]) <- [0..4]
]
χ A = [[ A @x @y ^ (~A @((x + 1) % 5) @y && A @((x + 2) % 5) @y)
| y <- [0..4]]
| x <- [0..4]]

/**
* One of the step mappings that's part of a round of Keccak-p.
* Compute the round constant for the `t`th lane.
*
* [FIPS-202] Section 3.2.5, Algorithm 6 (kind of).
* [FIPS-202] Section 3.2.5, Algorithm 5.
*/
ι : State -> State -> State
ι RC A = A ^ RC
rc : [8] -> Bit
rc t = if (t % 255) == 0 then 1 // Step 1.
else Rs @ (t % 255) @0 // Step 4.
where
// Step 2 - 3.
Rs = [0b10000000] # [lfsr R | R <- Rs ]
// Step 3. Linear feedback shift register.
// The truncation in step f is done manually in the return value.
lfsr : [8] -> [8]
lfsr Rin = [R0, R@1, R@2, R@3, R4, R5, R6, R@7]
where
R = 0b0 # Rin
R0 = R@0 ^ R@8
R4 = R@4 ^ R@8
R5 = R@5 ^ R@8
R6 = R@6 ^ R@8

/**
* Format the hard-coded round constant values.
* Hardcode the round constant values.
*
* Since the `rc` function doesn't depend on any of the functor parameters,
* this hardcoded value is correct for all instantiations.
* We computed the value `constants` with:
* ```cryptol
* [rc i | i <- [0..255]]
* ```
*
* [FIPS-202] Section 3.2.5.
* This provides a 4x speedup.
*
* Equivalent to [FIPS-202] Section 3.2.5, Algorithm 5.
*/
rc_hardcoded : [8] -> Bit
rc_hardcoded t = constants @ t where
constants = join [
0x80b1e87f90a7d57062b32fde6ee54a25,
0xa339e361175edf0d35b504ec9303a471
]

/**
* Prove that the hardcoded round constants are correct.
* ```repl
* :prove round_constants_correctly_hardcoded
* ```
*/
RCs : {n} (fin n, 24 >= n, n == 12 + 2 * ell) => [n]State
RCs = take`{n} [ [[take`{w} RC] # zero] # zero | RC <- RCs64 ]
property round_constants_correctly_hardcoded t = rc_hardcoded t == rc t

/**
* Hardcode the round constant values for b = 1600.
* [FIPS-202] Section 3.2.5.
* One of the step mappings that's part of a round of Keccak-p.
*
* The effect is to modify some of the bits of the Lane defined by
* `(0, 0)` according to the round index.
* [FIPS-202] Section 3.2.5, Algorithm 6.
*/
RCs64 : [24][64]
RCs64 = join (transpose [
[0x0000000000000001, 0x000000008000808B],
[0x0000000000008082, 0x800000000000008B],
[0x800000000000808A, 0x8000000000008089],
[0x8000000080008000, 0x8000000000008003],
[0x000000000000808B, 0x8000000000008002],
[0x0000000080000001, 0x8000000000000080],
[0x8000000080008081, 0x000000000000800A],
[0x8000000000008009, 0x800000008000000A],
[0x000000000000008A, 0x8000000080008081],
[0x0000000000000088, 0x8000000000008080],
[0x0000000080008009, 0x0000000080000001],
[0x000000008000000A, 0x8000000080008008]
])
ι : State -> [8] -> State
ι A ir = A'' where
// Step 1.
A' = A
// Step 2.
RC0 = zero : [w]
// Step 3. 0 is the identity for XOR, so we iteratively set the
// `2^j-1`th element by XORing the previously-set bits of RC with the
// correct value at the desired index.
RCs = [RC0] # [RC' ^ (zext`{w} [rc_hardcoded (j + 7 * ir)] << (2^^j - 1))
| RC' <- RCs
| j <- [0..ell] ]
RC = (RCs ! 0) : [w]
// Step 4.
A'' = [[ if (x == 0) && (y == 0) then A'@0@0 ^ RC else A'@x@y
| y <- [0..4]]
| x <- [0..4]]

/**
* Padding rule `pad10*1`.
Expand All @@ -244,47 +343,28 @@ private
/**
* Keccak-f family of permutations.
*
* This is implemented as defined in Section 3.4, but while `Keccak-p` isn't
* explicitly implemented, we "expanded" the `Keccak-p` implementation
* according to the parameters given in the definition of `Keccak-f`.
* Specifically, note the range of `ir`.
*
* The number of rounds is a parameter to this functor and not passed
* explicitly here.
*
* [FIPS-202] Section 3.4.
*/
Keccak_f : [b] -> [b]
Keccak_f S = S'
where
// The round transformation is defined in [FIPS-202] Section 3.3.
Rnd A ir = ι (χ (π (ρ_hardcoded (θ A)))) ir
// Step 1.
A0 = unflatten S
rounds = [A0] # [ Round RC A | RC <- RCs | A <- rounds ]
// Step 2.
rounds = [A0] # [ Rnd A ir | A <- rounds | ir <- [0..nr - 1]]
// Step 3.
S' = flatten (rounds ! 0)


/**
* The round function for `Keccak-p`. Denoted `Rnd` in the spec.
* [FIPS-202] Section 3.3.
*/
Round : State -> State -> State
Round RC A = ι RC (χ (π (ρ (θ A))))


/**
* Equivalence property showing that the hard-coded round constants
* match the description in the spec.
* [FIPS-202] Section 3.2.5.
*
* This takes about 6 seconds to prove.
* ```repl
* :prove RC_correct
* ```
*/
RC_correct : [8] -> [8] -> Bool
property RC_correct i j =
// See Algorithm 6, Step 3.
i < 24 ==> j < `ell ==> RCs64@i!(2^^j - 1) == lfsr@(j + 7*i)
where
// Algorithm 5.
lfsr : [inf]
lfsr = [ p!0 | p <- ps ]
where
/* powers of x modulo m */
ps = [0x01] # [ pmod (pmult p 0b10) m | p <- ps ]
m = <| x^^8 + x^^6 + x^^5 + x^^4 + 1 |>

/**
* See https://keccak.team/files/Keccak-reference-3.0.pdf, Section 1.2
* ```repl
Expand Down

0 comments on commit 7468d17

Please sign in to comment.