sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Crypto.SHA

Contents

- Parameterizing SHA
- Section 4.1.2, SHA functions
- SHA variants
- Section 5, Preprocessing
- Section 6.2.2 and 6.4.2, Hash computation
- Computing the digest
- Testing
- Code generation
- Helpers

Description

Implementation of SHA2 class of algorithms, closely following the spec http://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf.

We support all variants of SHA in the spec, except for SHA1. Note that this implementation is really useful for code-generation 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 ()
- cgSHA512 :: IO ()
- chunkBy :: Int -> ([a] -> b) -> [a] -> [b]
- showHash :: (Show a, Integral a, SymVal a) => SBV a -> String

# Parameterizing SHA

data SHA w Source #

Parameterized SHA representation, that captures all the differences between variants of the algorithm. `w` is the word-size type.

Constructors

SHA |

Fields

- wordSize :: Int

  Section 1 : Word size we operate with

- blockSize :: Int

  Section 1 : Block size for messages

- sum0Coefficients :: (Int, Int, Int)

  Section 4.1.2-3 : Coefficients of the Sum0 function

- sum1Coefficients :: (Int, Int, Int)

  Section 4.1.2-3 : Coefficients of the Sum1 function

- sigma0Coefficients :: (Int, Int, Int)

  Section 4.1.2-3 : Coefficients of the sigma0 function

- sigma1Coefficients :: (Int, Int, Int)

  Section 4.1.2-3 : Coefficients of the sigma1 function

- shaConstants :: [w]

  Section 4.2.2-3 : Magic SHA constants

- h0 :: [w]

  Section 5.3.2-6 : Initial hash value

- shaLoopCount :: Int

  Section 6.2.2, 6.4.2: How many iterations are there in the inner loop

# Section 4.1.2, SHA functions

ch :: Bits a => a -> a -> a -> a Source #

The choose function.

maj :: Bits a => a -> a -> a -> a Source #

The majority function.

sum0 :: Bits a => SHA w -> a -> a Source #

The sum-0 function. We parameterize over the rotation amounts as different variants of SHA use different rotation amounts.

sum1 :: Bits a => SHA w -> a -> a Source #

The sum-1 function. Again, parameterized.

sigma0 :: Bits a => SHA w -> a -> a Source #

The sigma0 function. Parameterized.

sigma1 :: Bits a => SHA w -> a -> a Source #

The sigma1 function. Parameterized.

# SHA variants

sha224P :: SHA (SWord 32) Source #

Parameterization for SHA224.

sha256P :: SHA (SWord 32) Source #

Parameterization for SHA256. Inherits mostly from SHA224.

sha384P :: SHA (SWord 64) Source #

Parameterization for SHA384.

sha512P :: SHA (SWord 64) Source #

Parameterization for SHA512. Inherits mostly from SHA384.

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

newtype Block a Source #

`Block` is a synonym for lists, but makes the intent clear.

Constructors

Block [a] |

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!

# 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 for-loop 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

sha224 :: String -> SWord 224 Source #

SHA224 digest.

sha256 :: String -> SWord 256 Source #

SHA256 digest.

sha384 :: String -> SWord 384 Source #

SHA384 digest.

sha512 :: String -> SWord 512 Source #

SHA512 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.

cgSHA256 :: IO () Source #

Generate code for one block of SHA256 in action, starting from an arbitrary hash value.

cgSHA512 :: IO () Source #

Generate code for one block of SHA512 in action, starting from an arbitrary hash value.

# Helpers

chunkBy :: Int -> ([a] -> b) -> [a] -> [b] Source #

Helper for chunking a list by given lengths and combining each chunk with a function

showHash :: (Show a, Integral a, SymVal a) => SBV a -> String Source #

Nicely lay out a hash value as a string