HMAC.cry

/*
@copyright Galois, Inc. 2016-2018
@author Aaron Tomb <atomb@galois.com>
@author Nathan Collins <conathan@galois.com>
@author Joey Dodds <jdodds@galois.com>
*/

module Primitive::Symmetric::MAC::HMAC where

import Primitive::Keyless::Hash::SHA2Imperative::SHA256

//////// Functional version ////////

sha256Wrap msg = sha (join msg)

hmacSHA256 : {pwBytes, msgBytes}
             (fin pwBytes, fin msgBytes
             , 32 >= width msgBytes
             , 64 >= width (8*pwBytes)
             , 64 >= width (8 * (64 + msgBytes))
             ) => [pwBytes][8] -> [msgBytes][8] -> [256]
hmacSHA256 = hmac `{blockLength=64} sha256Wrap sha256Wrap sha256Wrap

kinit : { pwBytes, blockLength, digest }
        ( fin pwBytes, fin blockLength, fin digest )
     => ([pwBytes][8] -> [8*digest])
     -> [pwBytes][8]
     -> [blockLength][8]
kinit hash key =
  if `pwBytes > (`blockLength : [max (width pwBytes) (width blockLength)])
  then take `{blockLength} (split (hash key) # (zero : [blockLength][8]))
  else take `{blockLength} (key # (zero : [blockLength][8]))

// Due to limitations of the type system we must accept two
// separate arguments (both allegedly the same) for two
// separate length inputs.
hmac : { msgBytes, pwBytes, digest, blockLength }
       ( fin pwBytes, fin digest, fin blockLength )
    => ([blockLength + msgBytes][8] -> [8*digest])
    -> ([blockLength + digest][8] -> [8*digest])
    -> ([pwBytes][8] -> [8*digest])
    -> [pwBytes][8]
    -> [msgBytes][8]
    -> [digest*8]
hmac hash hash2 hash3 key message = hash2 (okey # internal)
 where
   ks : [blockLength][8]
   ks = kinit hash3 key
   okey = [k ^ 0x5C | k <- ks]
   ikey = [k ^ 0x36 | k <- ks]
   internal = split (hash (ikey # message))