miTLS
A verified reference TLS implementation
Home
Download
Browse
TLS Attacks
People
miTLS
:: HMAC
F# Interface: HMAC.fsi
(* * Copyright (c) 2012--2013 MSR-INRIA Joint Center. All rights reserved. * * This code is distributed under the terms for the CeCILL-B (version 1) * license. * * You should have received a copy of the CeCILL-B (version 1) license * along with this program. If not, see: * * http://www.cecill.info/licences/Licence_CeCILL-B_V1-en.txt *) module HMAC open Bytes open TLSConstants type key = bytes type data = bytes type mac = bytes val MAC: macAlg -> key -> data -> mac val MACVERIFY: macAlg -> key -> data -> mac -> bool
F# Implementation: HMAC.fs
(* * Copyright (c) 2012--2013 MSR-INRIA Joint Center. All rights reserved. * * This code is distributed under the terms for the CeCILL-B (version 1) * license. * * You should have received a copy of the CeCILL-B (version 1) license * along with this program. If not, see: * * http://www.cecill.info/licences/Licence_CeCILL-B_V1-en.txt *) module HMAC open Bytes open TLSConstants type key = bytes type data = bytes type mac = bytes (* SSL3 keyed hash *) let sslKeyedHashPads alg = match alg with | MD5 -> (ssl_pad1_md5, ssl_pad2_md5) | SHA -> (ssl_pad1_sha1, ssl_pad2_sha1) | _ -> Error.unexpectedError "[sslKeyedHashPads] invoked on unsupported algorithm" let sslKeyedHash alg key data = let (pad1, pad2) = sslKeyedHashPads alg in let dataStep1 = key @| pad1 @| data in let step1 = HASH.hash alg dataStep1 in let dataStep2 = key @| pad2 @| step1 in HASH.hash alg dataStep2 let sslKeyedHashVerify alg key data expected = let result = sslKeyedHash alg key data in equalBytes result expected (* Parametric keyed hash *) let HMAC alg key data = match alg with | MD5 -> CoreHMac.md5 key data | SHA -> CoreHMac.sha1 key data | SHA256 -> CoreHMac.sha256 key data | SHA384 -> CoreHMac.sha384 key data | NULL -> Error.unexpectedError "[HMAC] Invalid hash (NULL) for HMAC" | MD5SHA1 -> Error.unexpectedError "[HMAC] Invalid hash (MD5SHA1) for HMAC" let HMACVERIFY alg key data expected = let result = HMAC alg key data in equalBytes result expected (* Top level MAC function *) let MAC a k d = match a with | MA_HMAC(alg) -> HMAC alg k d | MA_SSLKHASH(alg) -> sslKeyedHash alg k d let MACVERIFY a k d t = match a with | MA_HMAC(alg) -> HMACVERIFY alg k d t | MA_SSLKHASH(alg) -> sslKeyedHashVerify alg k d t
F7 Interface: HMAC.fs7
(* * Copyright (c) 2012--2013 MSR-INRIA Joint Center. All rights reserved. * * This code is distributed under the terms for the CeCILL-B (version 1) * license. * * You should have received a copy of the CeCILL-B (version 1) license * along with this program. If not, see: * * http://www.cecill.info/licences/Licence_CeCILL-B_V1-en.txt *) module HMAC (* Core HMAC algorithms; trusted only on their tag lengths *) open Bytes open TLSConstants type key = bytes type data = bytes type mac = bytes val MAC: a:macAlg -> k:key {Length(k)=MacSize(a)} -> data -> t:mac {Length(t)=MacSize(a)} val MACVERIFY: a:macAlg -> k:key {Length(k)=MacSize(a)} -> data -> t:mac {Length(k)=MacSize(a)} -> bool
Verification status
Verification depends on the F7 interfaces of the following modules:
Error
Bytes
TLSConstants
HASH
Module list
Trusted
SessionDB
Bytes
Cert
Tcp
Range
TLSExtensions
TLSConstants
Idealized
Nonce
PRF
DH
MAC_SHA1
RSA
LHAE
RSAKey
DHGroup
MAC_SHA256
Sig
ENC
CRE
Verified
TLS
UTLS
DataStream
AppData
PwToken
LHAEPlain
TLSInfo
Handshake
StatefulLHAE
Alert
TLSFragment
Record
MAC
Dispatch
Error
Encode
PwApp