miTLS
A verified reference TLS implementation
Home
Download
Browse
TLS Attacks
People
miTLS
:: HASH
F# Interface: HASH.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 HASH open Bytes open TLSConstants val hash: hashAlg -> bytes -> bytes
F# Implementation: HASH.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 HASH open Bytes open TLSConstants (* Parametric hash algorithm (implements interface) *) let hash alg data = match alg with | NULL -> data | MD5SHA1 -> CoreHash.md5 data @| CoreHash.sha1 data | MD5 -> CoreHash.md5 data | SHA -> CoreHash.sha1 data | SHA256 -> CoreHash.sha256 data | SHA384 -> CoreHash.sha384 data
F7 Interface: HASH.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 HASH (* Core cryptographic hash algorithms; trusted only to have the right tag length *) open Bytes open TLSConstants val hash: a:hashAlg -> bytes -> b:bytes{Length(b)=HashSize(a)}
Verification status
Verification depends on the F7 interfaces of the following modules:
Error
Bytes
TLSConstants
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