Crypto.Encoding.PHKDF

Documentation

extendTagToList :: ByteString -> [ByteString]

extendTag :: ByteString -> ByteString

Extends a PHKDF end-of-message tag in order to ensure the last SHA-256 block contains something interesting.

Tags less than 160 bits (20 bytes) long are appended directly, without extension, as the final portion of the message. Thus this function is the identity on short inputs.

After extension, tags that are at least 20 bytes long should be thought of as a bitstring with a single null bit appended at the end to make it a full bytestring.

Tags 160 bits or longer are first extended, iff necessary, to a full bytestring by adding a single "1" bit followed by zero to six "0" bits.

The bytestring is then extended by 0-63 bytes as needed to make the overall length equivalent to 19 (mod 64). The first byte of the extension is a null byte, then followed by the bytestring, then starting again at the null byte as needed.

The length of this extension takes up the first 6 bits of the last byte, followed by a "0" bit denoting the tag is a bytestring, or a "1" denoting that the tag is a proper bitstring whose length is not an exact multiple of 8.

The final bit is reserved for SHA-256's end-of-message padding, which will set it to 1.

trimExtendedTag :: ByteString -> Maybe ByteString

This function robustly undoes extendTag, thus "proving" that all collisions on PHKDF's tag are cryptographically non-trivial, even after extension.

This is a "proof" in the sense that if trimExtendedTag (extendTag x) == Just x is true for all bytestrings x, then all collisions are non-trivial, but we haven't presented a full deductive proof of this property. It is part of the test suite, tested by quickcheck fuzzing.

The rest of PHKDF and the G3P's syntax follows this as an iron rule of syntax design. I've not literally written a program to parse out the original arguments, but I've ensured that it is straightforward to do so in principle.

In the case of variable-length PHKDF, starting from some known buffer position (usually either 0 or 32), first there are zero or more bitstring arguments encoded via TupleHash syntax. Since TupleHash's length encoding cannot start with a null byte, a single null byte is used to signal the end of these input arguments. Then 0-63 end padding bytes are generated in order to bring the buffer position equivalent to 32 (mod 64), then 4 bytes of counter, then the extended version of PHKDF's end-of-message tag, then finally SHA256's end padding.

This is easy to robustly undo, as I've started to demonstrate in this subroutine. This leads to a simple categorical/combinatorial style proof that all collisions over PHKDF's input arguments and domain tag are cryptographically non-trivial.

add64WhileLt :: (Ord a, Num a, Bits a) => a -> a -> a

add64WhileLt b c is equivalent to while (b < c) { b += 64 }; return b

add64WhileLt' :: (Ord a, Num a, Bits a, Show a) => a -> a -> a

Equivalent to add64WhileLt, except with trace debugging. This should never be used in production.

dropBs :: Int64 -> [ByteString] -> [ByteString]

takeBs :: Int64 -> [ByteString] -> [ByteString]

takeBs' :: Int64 -> [ByteString] -> [ByteString]

takeB' :: Int64 -> ByteString -> Maybe ByteString

assertTakeB' :: Int64 -> ByteString -> ByteString

nullBuffer :: ByteString

chunkify :: Int -> ByteString -> [ByteString]

Partition a bytestring into chunks of up to a given size

chunkifyCycle

Arguments

:: Int64

Desired chunk size

-> ByteString

String to be cyclically extended.

-> Int64

Starting offset

-> [ByteString]

Infinite stream of chunks

Partition a cyclically extended bytestring into chunks of a given size, starting at a given offset.

Note that repetitions of the original string get a single null byte placed between them.