Following on from the MD6-in-Cryptol posting, let’s consider another very interesting candidate from the (deep) pool of SHA-3 submissions; Skein
http://www.skein-hash.info/ http://www.schneier.com/skein.html
by the merry band of Ferguson, Lucks, Schneier, et al.The expression of their reference implementation comes out, we think, fairly cleanly in Cryptol. The digest output size is a variable parameter to the algorithm, but we’ll focus on the 512-bit version here — the submission’s primary candidate for SHA-3.In order to avoid duplicating the introductory material on Cryptol, we suggest the reader go through the MD6 writeup to get a grounding in Cryptol, its idioms, and syntax.
The structure of Skein
Skein refers to a family of hashing functions, differing in the size of their internal state. We’ll look at the 512-bit version here. Skein is built up out of three main components:
- A tweakable block cipher, Threefish.
- The Unique Block Iteration(UBI) chaining mode, defining the mode-of-operation by the repeated application of the block cipher function.
- Optional arguments to the hashing function. Extra functionality and input to the hashing function can be accommodated via Skein’s optional argument system. There is also input, like key material and randomized-hashing via nonces, etc. (see spec for details). We won’t consider any such additional inputs in our implementation of the basic hashing functionality.
We’ll take the same tack as with the MD6 presentation – starting at the top by showing the mode-of operation function, working our way down to the tweakable block cipher that the Skein team developed as part of Skein.
The Skein hashing function
The pure/simple Skein hashing function (512 bit) transforms an arbitrary length byte sequence into a 512-bit output:
hash512 : {a}
// type constraints
( fin a // finite input
, 32 >= width (8*((8*a+7)/8))
, 32 >= width (8*a)
, 64*(((8*a+7)/8+63)/64) >= (8*a+7)/8
, 8*((8*a+7)/8) >= 8*a
) => [a][8] // input message
-> [64][8]; // 512-bit result
The Cryptol type signature captures that (and more!), with the [64][8] result packaging up the result into a 64-element wide sequence of 8-bit bytes. The type constraints look involved, but capture the pre-condition that the input message size has already been padded out to the desired width. (Writing Cryptol functions that automatically perform padding based on input sizes is possible, but would be a distraction here.)The definition of hash512 closely mirrors the specification (Section 3.5.4):
hash512 m = output512 g1
where {
k = (zero : [64][8]);
c = mkConfig(512); // config string, see Section 3.5.2 of spec.
g0 = ubi512 (encrypt512, k,join c, t_cfg);
g1 = ubi512 (encrypt512,g0,join m, t_msg);
};
i.e., it is the double application of the chaining mode UBI, followed in the end by the computation of the result by the output512 function. As the internal size has been fixed here to 512, the innermost UBI computation is actually all over constant inputs and could be folded/optimized away. This optimization can be done manually or by the Cryptol tools, but we won’t bother with the optimization here.The output function is simply another application of the UBI:
output512 : [64][8] -> [64][8]; output512 g = ubi512 (encrypt512, g, (zero:[64]), t_out);
i.e., a straight UBI computation of the internal state argument g to the null message and a special output type value.Regarding t_out, the various t_X values in the above represent the type values that Skein defines —
t_out : [128]; t_out = ((0x3f: [6]) # zero) << 120; t_cfg : [128]; t_cfg = ((0x04: [6]) # zero) << 120; t_msg : [128]; t_msg = ((0x30: [6]) # zero) << 120;
i.e., padded out to 128-bit widths so as to fit with subsequent use as basis for Skein’s tweak values.That’s the toplevel driver for the Skein hashing function. Let’s consider next the chaining mode that it builds upon.
UBI: the Unique Block Iteration chaining mode
The chaining mode employed by Skein is parameterized over the following values:
- G – (chained) internal state / starting value.
- M – the message string.
- T – a 128-bit starting value for the tweak (the type value from the above.)
As a Cryptol type signature, its external interface would be
ubi512 : {a}
( fin a
, 32 >= width (8*((a+7)/8))
, 32 >= width a
, 64*(((a+7)/8+63)/64) >= (a+7)/8
, 8*((a+7)/8) >= a
) => ( (([64][8],[16][8],[64][8]) -> [8][64]) // block cipher function
, [64][8] // initial (chained) value / state.
, [a] // input message
, [128] // tweak base value
) -> ([64][8]); // 512 bit result
The type constraints all involve the type variable a, which is the size of the input message. Together they express the padding assumptions made or introduced over that bit string.The function takes four arguments, the first being a function value — the block cipher function to apply for each of the blocks that the input message is divvied up into. We’ll have more to say about its type and properties in the next section when we show how the Threefish cipher is expressed in Cryptol.The other three are the G, M, and T parameters to the UBI, which we can now define as follows:
ubi512 (encryptor,g,m,t) = last hs
where {
hs = [g] # [| m ^ split(join(encryptor(h, groupBy(8,mkTweak(t,width(m1),nb,width ms,i,b)),m)))
|| h
Like before, let’s start with the result value and work ourselves inwards from there — the result being the last element of the hs sequence. hs represents the result of processing each block (512 bits) of the input message. The definition of hs expresses how to compute block N’s digested output:
hs = [g] # [| m ^ split(join(encryptor(h, groupBy(8,mkTweak(t,width(m1),nb,width ms,i,b)),m)))
|| h
The iterative nature of the chaining mode is captured as a recursive sequence comprehension in Cryptol, with each of the arms of the comprehension providing input to the UBI’s result computation (e.g., m <- ms selects each block in turn.) That result computation is a bit of a mouthful, but easy enough to pick apart a bit:
m ^ split(join(encryptor(h, groupBy(8,mkTweak(t,width(m1),nb,width ms,i,b)),m)))
i.e., XORing the message block with the application of the block cipher encryptor —
encryptor(H,Tweak,MsgBlock)
where Tweak is a 128-bit value made up out of a range of parameters, globally-constant, per-UBI-specific and per-round, all contributing to diffusing the output. The h is the output from the previous invocation of the block cipher, i.e., to compute element we need to have access to the previous UBI result only.We hope it is relatively straightforward to map the definition of hs back to the recurrence relation that defines the UBI in Section 3.4 of the Skein specification. With tweaks and message blocks in place, it is time to consider the block cipher that Skein uses.
Threefish, a tweakable block cipher
This block cipher is parameterized over the following values:
- K – block cipher key (512 bits / 64 bytes)
- T – tweak (128 bits / 16 bytes)
- P – plaintext (equal to key)
Deriving the Cryptol type signature from that is straightforward:
encrypt512 : ([64][8],[16][8],[64][8]) -> [8][64];
with the result being 8 64-bit words. This simple type hides many a clever detail though:
encrypt512 (key,tweak,pt) = vn + kn
where {
vn : [nw][64];
vn = last vss;
kn : [nw][64];
kn = last kss;
// ...more below...
The result is the element-wise addition of two 64-bit word sequences of width 8 (cf. the definition of the ciphertext C in Section 3.3 of the specification). kn is the last value from the key schedule of the cipher, and vn is the last value from the round computation. The key schedule is a Cryptol sequence of values, splitting up the input key and tweak into round/4 sub-keys:
kss : [19][nw][64]; kss = [| keySchedule_8(tw_words, key_words, d) || d
We won’t show the implementation of the keySchedule_8() function here, but the reader is encouraged to download the sources and look it over in Skein/Threefish.cry.The subkeys are combined together with the per-round values:
vss : [73][nw][64]; vss = [pt_words] # [| fs @@ pi_8 || fs
Again, we won’t go into further details on the internals of the cipher, but it is worth highlighting the use of mutually recursive sequences values — vss is computed in terms of fss, which is defined in terms of ess, which ties the knot back to vss in its definition. The recursive nature works out by being initialized with pt_words as the result of round 0.
The MIX function
Threefish uses the MIX function to perform its permutation and mixing; encoded in Cryptol as follows:
mix8 : ([8],[8][64]) -> [8][64];
mix8 (d,xss) = join [| mix_8(d,j,xs) || j [2][64];
mix_8 (d,j,[x0 x1]) = [y0 y1]
where {
y0 : [64];
y0 = (x0 + x1);
y1 = (x1 <<< (rs_8 @ j @ ((d%0x8)#zero))) ^ y0;
};
Included here for completeness, the round-dependent permutation of its 512-bit input maps relatively cleanly onto the specification of MIX in Section 3.3.1. The built-in groupBy operator perform useful function here in dividing up its per-round input:
groupBy : {a b c} (b,[a*b]c) -> [a][b]c
i.e., if the second argument is a multiple of the first (b), we can divide it up into a values of width b. Use it here to split up the 512-bit input into 4 pairs of 128-bit values.
Concluding remarks
Skein has an appealingly clean structure and composition, something we hope to have maintained some in its Cryptol rendition. The use of recursive sequence definitions to express the chaining and iterative nature of the algorithm is one place which helped in maintaining the clear mapping back to the specification. Having a clean reference implementation like this has considerable value, but using it with Cryptol and its toolchain, you may take advantage of its definition in a number of ways. Please see the concluding remarks for the MD6 posting for an outline of what they are.
Downloading Cryptol Skein
If you want to try out the implementation of Skein in Cryptol, it’s available from download as a separate archive. Load it into your Cryptol interpreter, and verify its sanity by running some of the known-answer tests:
Cryptol> :load Skein.cry ... Skein> ts_1 True Skein> ts_4 True Skein>
To have a closer look at the underlying code and experiment with it, edit the .cry files followed by :reload from the Cryptol interpreter prompt.
Want more?
If you’d like to see more examples of Cryptol, maybe other SHA-3 candidates, please let us know. Or, better still, have a go at implementing some of them yourself. The CubeHash submission by D.J. Bernstein is perhaps a good place to start?
Author
("Sigbjorn Finne" # "Galois, Inc" # "2009-01-23") : [35][8]