Copyright  (c) Levent Erkok 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
Implementation of SHA2 class of algorithms, closely following the spec http://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.1804.pdf.
We support all variants of SHA in the spec, except for SHA1. Note that this implementation is really useful for codegeneration purposes from SBV, as it is hard to state (or prove!) any particular properties of these algorithms that is suitable for SMT solving.
Synopsis
 data SHA w = SHA {
 wordSize :: Int
 blockSize :: Int
 sum0Coefficients :: (Int, Int, Int)
 sum1Coefficients :: (Int, Int, Int)
 sigma0Coefficients :: (Int, Int, Int)
 sigma1Coefficients :: (Int, Int, Int)
 shaConstants :: [w]
 h0 :: [w]
 shaLoopCount :: Int
 ch :: Bits a => a > a > a > a
 maj :: Bits a => a > a > a > a
 sum0 :: Bits a => SHA w > a > a
 sum1 :: Bits a => SHA w > a > a
 sigma0 :: Bits a => SHA w > a > a
 sigma1 :: Bits a => SHA w > a > a
 sha224P :: SHA (SWord 32)
 sha256P :: SHA (SWord 32)
 sha384P :: SHA (SWord 64)
 sha512P :: SHA (SWord 64)
 sha512_224P :: SHA (SWord 64)
 sha512_256P :: SHA (SWord 64)
 newtype Block a = Block [a]
 prepareMessage :: forall w. (Num w, ByteConverter w) => SHA w > String > [Block w]
 hashBlock :: (Num w, Bits w) => SHA w > [w] > Block w > [w]
 shaP :: (Num w, Bits w, ByteConverter w) => SHA w > String > [w]
 sha224 :: String > SWord 224
 sha256 :: String > SWord 256
 sha384 :: String > SWord 384
 sha512 :: String > SWord 512
 sha512_224 :: String > SWord 224
 sha512_256 :: String > SWord 256
 knownAnswerTests :: Int > Bool
 cgSHA256 :: IO ()
 chunkBy :: Int > ([a] > b) > [a] > [b]
 showHash :: (Show a, Integral a, SymVal a) => SBV a > String
Parameterizing SHA
Parameterized SHA representation, that captures all the differences
between variants of the algorithm. w
is the wordsize type.
SHA  

Section 4.1.2, SHA functions
sum0 :: Bits a => SHA w > a > a Source #
The sum0 function. We parameterize over the rotation amounts as different variants of SHA use different rotation amnounts.
SHA variants
sha512_224P :: SHA (SWord 64) Source #
Parameterization for SHA512_224. Inherits mostly from SHA512
sha512_256P :: SHA (SWord 64) Source #
Parameterization for SHA512_256. Inherits mostly from SHA512
Section 5, Preprocessing
prepareMessage :: forall w. (Num w, ByteConverter w) => SHA w > String > [Block w] Source #
Prepare the message by turning it into blocks. We also check for the message size requirement here. Note that this won't actually happen in practice as the input length would be > 2^64 (or 2^128), and you'd run out of memory first! Such a check
Section 6.2.2 and 6.4.2, Hash computation
hashBlock :: (Num w, Bits w) => SHA w > [w] > Block w > [w] Source #
Hash one block of message, starting from a previous hash. This function
corresponds to body of the forloop in the spec. This function always
produces a list of length 8, corresponding to the final 8 values of the H
.
shaP :: (Num w, Bits w, ByteConverter w) => SHA w > String > [w] Source #
Compute the hash of a given string using the specified parameterized hash algorithm.
Computing the digest
sha512_224 :: String > SWord 224 Source #
SHA512_224 digest.
sha512_256 :: String > SWord 256 Source #
SHA512_256 digest.
Testing
knownAnswerTests :: Int > Bool Source #
Collection of known answer tests for SHA. Since these tests take too long during regular regression runs, we pass as an argument how many to run. Increase the below number to 24 to run all tests. We have:
>>>
knownAnswerTests 1
True
Code generation
It is not practical to generate SBV code for hashing an entire string, as it would require handling of a fixed size string. Instead we show how to generate code for hashing one block, which can then be incorporated into a larger program by providing the appropriate loop.
Generate code for one block of SHA256 in action, starting from an arbitrary hash value.