miTLS :: MAC_SHA1

F# Interface: MAC_SHA1.fsi

F# Implementation: MAC_SHA1.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 MAC_SHA1

open Bytes
open TLSConstants
open TLSInfo
open Error

type text = bytes
type tag = bytes
type keyrepr = bytes
type key = {k:keyrepr}

// for concreteness; the rest of the module is parametric in a
let a = MA_HMAC(SHA)

#if ideal // We maintain a table of MACed plaintexts
type entry = epoch * text * tag
let log:entry list ref=ref []
let rec tmem (e:epoch) (t:text) (xs: entry list) =
  match xs with
      [] -> false
    | (e',t',m)::res when e = e' && t = t' -> true
    | (e',t',m)::res -> tmem e t res
#endif

let Mac (ki:epoch) key t =
    let m = HMAC.MAC a key.k t in
    #if ideal // We log every authenticated texts, with their index and resulting tag
    log := (ki, t, m)::!log;
    #endif
    m

let Verify (ki:epoch) key t m =
    HMAC.MACVERIFY a key.k t m
    #if ideal // We use the log to correct any verification errors
    && tmem ki t !log
    #endif

let GEN (ki:epoch) = {k= random (macKeySize(a))}

F7 Interface: MAC_SHA1.fs7

module MAC_SHA1

(* Core HMAC algorithms, idealized for INT-CMA:
   compared with MAC.fs7, we are still abstractly indexed (for multi-instance)
   but the algorithm is fixed, the keys are abstract, and security is unconditional *)

open Bytes
open TLSConstants
open TLSInfo

val a: a:macAlg{ a = MA_HMAC(SHA) } // symbolic constant

type (;ki:succEpoch) keyrepr = k:bytes {Length(k) = MacSize(a)}
private type (;ki:succEpoch) key = {k:(;ki) keyrepr}

type text = bytes
predicate val Msg: epoch * text -> bool

type tag = m:bytes {Length(m) = MacSize(a)}

val Mac:
  ki:succEpoch -> (;ki) key ->
  t:text {Msg(ki,t)} -> tag
val Verify:
  ki:succEpoch -> (;ki) key -> t:text ->
  tag -> b:bool { b=true => Msg(ki,t) }

val GEN:
  ki:succEpoch -> (;ki) key

(* typing the log for the ideal functionality *)

private type entry = (ki:epoch * t:text * tag){Msg(ki,t)}
private val log: entry list ref
private val tmem: ki:epoch -> t:text -> entry list -> b:bool{ b=true => Msg(ki,t) }

Verification status

This module is idealized: it contains both concrete F# code and an ideal implementation (when "ideal" flag set to true). The concrete code is not verified. Where applicable, we verify that the ideal implementation matches the F7 interface.

Verification depends on the F7 interfaces of the following modules: Error Bytes TLSConstants RSAKey DHGroup HASH HMAC Sig Cert TLSInfo

miTLS

A verified reference TLS implementation

miTLS :: MAC_SHA1

F# Interface: MAC_SHA1.fsi

F# Implementation: MAC_SHA1.fs

F7 Interface: MAC_SHA1.fs7

Verification status

Module list

Trusted

Idealized

Verified