miTLS :: MAC

F# Interface: MAC.fsi

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

open Bytes
open TLSConstants

open TLSInfo
open Error

type text = bytes
type tag = bytes
type keyrepr = bytes
type key =
  | KeyNoAuth  of keyrepr
  | Key_SHA256 of MAC_SHA256.key
  | Key_SHA1   of MAC_SHA1.key

// We comment out an ideal variant that directly specifies that MAC
// is ideal at Auth indexes; we do not need that assumption anymore,
// as we now typecheck this module against plain INT-CMA MAC interfaces:
// idealization now occurs within each of their implementations.
//
// #if ideal
// 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',tag)::res when e = e' && t = t' -> true
//    | (e',t',tag)::res -> tmem e t res
// #endif

let Mac ki key data =
    let si = epochSI(ki) in
    let a = macAlg_of_ciphersuite si.cipher_suite si.protocol_version in
    // // Commented out old ideal specification:
    // #if ideal
    // let tag =
    // #endif
      match key with
        | KeyNoAuth(k)  -> HMAC.MAC a k data
        | Key_SHA256(k) -> MAC_SHA256.Mac ki k data
        | Key_SHA1(k)   -> MAC_SHA1.Mac ki k data
    // #if ideal
    // // We log every authenticated texts, with their index and resulting tag
    // log := (ki, data, tag)::!log;
    // tag
    // #endif

let Verify ki key data tag =
    let si = epochSI(ki) in
    let a = macAlg_of_ciphersuite si.cipher_suite si.protocol_version in
    match key with
    | Key_SHA256(k) -> MAC_SHA256.Verify ki k data tag
    | Key_SHA1(k)   -> MAC_SHA1.Verify ki k data tag
    | KeyNoAuth(k) -> HMAC.MACVERIFY a k data tag
    // #if ideal
    // // At safe indexes, we use the log to detect and correct verification errors
    // && if safeMAC ki
    //   then
    //       tmem ki data !log
    //   else
    //       true
    // #endif

let GEN ki =
    let si = epochSI(ki) in
    #if ideal
    // ideally, we separately keep track of "Auth" keys,
    // with an additional indirection to HMAFC
    if safeMAC ki then
      let a = macAlg_of_ciphersuite si.cipher_suite si.protocol_version in
      match a with
      | a when a = MAC_SHA256.a -> Key_SHA256(MAC_SHA256.GEN ki)
      | a when a = MAC_SHA1.a   -> Key_SHA1(MAC_SHA1.GEN ki)
      | a                       -> unreachable "only strong algorithms provide safety"
    else
    #endif
    let a = macAlg_of_ciphersuite si.cipher_suite si.protocol_version in
    KeyNoAuth(random (macKeySize (a)))

let COERCE (ki:epoch) k = KeyNoAuth(k)
let LEAK (ki:epoch) k =
    match k with
    | Key_SHA256(k) -> unreachable "since we have Auth"
    | Key_SHA1(k)   -> unreachable "since we have Auth"
    | KeyNoAuth(k)  -> k

F7 Interface: MAC.fs7

module MAC

open Bytes
open TLSConstants
open TLSInfo

(* refined, agile, ideal interface for indexed MACs
   resistant to existential forgery against chosen message attacks (INT-CMA).

This module depends on

- a datatype of MAC algorithms (TLSConstants.MAC_alg)
   - an abstract type of indexes (TLSInfo.epoch)
   - a function from indexes to MAC algorithms (macAlg_of_epoch) and its logical spec.
   - functions from MAC algorithms to their key-lengths and tag-lengths, and their logical specs.
   - an function from indexes to booleans that indicates the safe indexes (safeMAC) and its logical spec;
     (this function is used only #if ideal)
   - an abstract predicate on indexes and message (Msg),
     specifying the logical property authenticated by safe MACs.

and the following assumptions:

- we generate (or coerce) at most one key per index.
   - if an index is Auth, then its algorithm is computationally strong (INT-CMA).

Notes: - this interface deals with CMA, not the joint CTXT assumption (where we rely on PRF)
          - this multiplexing similarly applies to any keyed functionality.
		  - concretely, we would get a bound depending on the quantitative usage of each strong algorithm
		  - pragmatically, we may e.g. assume INT-CMA for both variants of SHA2, but not for MD5 or SHA.
		  - so far we do attempt to prove that the ad hoc constructions of SSL_3p0 are strong.

We typecheck an ideal variant of this module,
   with an additional indirection for every call to HMAC with an Auth index via
   a series of (standard, non-agile) MAC$a interfaces that specify that algorithm $a is INT-CMA.
   where $a ranges over the subset of MAC algorithms of TLS for which we assume are INT-CMA.

The proof that MAC securely implements MAC.fs7 (up to computational indistinguishability)
   goes as follows. Formally, it is parametric in the number of MAC algorithms that are INT-CMA,
   so we need to typecheck MAC.fs for each such number, but this is very uniform; we do it for 2.

(1) When using the concrete implementations of MAC$a,
       we easily check that toggling the #ideal flag in MAC.fs does not change its behaviour,
	   (e.g. by inlining MAC$a.fs within MAC.fs) since both variants make the same calls to HMAC.

(2) By MAC.tc7, and since no other module calls any MAC$a,
       we have (complete) abstraction for MAC$a.key, so
       we apply their INT-CMA assumptions (up to computational indistinguishability),
       setting the #ideal flag in each MAC$a.fs implementation.

(3) By MAC$a.tc7, we typecheck that the ideal variant of MAC$a now implements MAC$a.fs7

(4) By MAC.tc7, we conclude that the ideal variant of MAC now implements MAC.fs7

Our concrete core algorithms are implemented by HMAC,
   after partial application of the algorithm name.
   (we keep using a single HMAC module just for convenience, with constants as their first "a" parameters) *)

type (;ki:succEpoch) keyrepr = k:bytes {Length(k) = MacSize(CipherSuiteMACAlg(EpochSI(ki).cipher_suite,EpochSI(ki).protocol_version)) }
type (;ki:succEpoch) tag     = m:bytes {Length(m) = MacSize(CipherSuiteMACAlg(EpochSI(ki).cipher_suite,EpochSI(ki).protocol_version))}

// Our type of keys has a separate constructor for each strong MAC algorithm,
// so that each of their key types (MAC_SHA256.key) can be kept abstract at every Auth index when #ideal.
// plus a default constructor for all other keys, concretely represented as fixed-length bytes.
// (thus, when not #ideal, all keys are KeyNoAuth and the other constructors are not used.)
private type (;ki:succEpoch) key =
  | KeyNoAuth of (k:(;ki) keyrepr { not(Auth(ki)) })
  | Key_SHA256 of (k:(;ki) MAC_SHA256.key
    { Auth(ki) /\
	  MAC_SHA256.a = CipherSuiteMACAlg(EpochSI(ki).cipher_suite,EpochSI(ki).protocol_version) })
  | Key_SHA1 of (k:(;ki) MAC_SHA1.key
    { Auth(ki) /\
	  MAC_SHA1.a = CipherSuiteMACAlg(EpochSI(ki).cipher_suite,EpochSI(ki).protocol_version) })

// this assumption records the list of concrete MAC algorithms
// assumed to be INT-CMA (in this instance, just MAC_SHA256.a is)
private assume
  !ki. Auth(ki) => (  CipherSuiteMACAlg(EpochSI(ki).cipher_suite,EpochSI(ki).protocol_version) = MAC_SHA256.a
                   \/ CipherSuiteMACAlg(EpochSI(ki).cipher_suite,EpochSI(ki).protocol_version) = MAC_SHA1.a )

ask !e,alg. Auth(e) /\ alg = CipherSuiteMACAlg(EpochSI(e).cipher_suite,EpochSI(e).protocol_version) =>
	(alg = MAC_SHA256.a \/ alg = MAC_SHA1.a)

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

// We define the Msg predicate of each MAC_SHA256 as follows,
// logically multiplexing them to the Msg predicate of MAC (to be defined in turn by users of MAC)
private definition
  !ki,t. MAC_SHA256.Msg(ki,t) <=>
      (Msg(ki,t) /\
	   Auth(ki) /\
	   MAC_SHA256.a = CipherSuiteMACAlg(EpochSI(ki).cipher_suite,EpochSI(ki).protocol_version))
private definition
  !ki,t. MAC_SHA1.Msg(ki,t) <=>
      (Msg(ki,t) /\
	   Auth(ki) /\
	   MAC_SHA1.a = CipherSuiteMACAlg(EpochSI(ki).cipher_suite,EpochSI(ki).protocol_version))

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

val GEN:    ki:succEpoch -> (;ki) key
val LEAK:   ki:succEpoch {not(Auth(ki))} -> (;ki)key -> (;ki)keyrepr
val COERCE: ki:succEpoch {not(Auth(ki))} -> (;ki)keyrepr -> (;ki)key

(*
// typing the log for an ideal functionality that
// directly specifies the security of MAC (not used anymore)
private type entry = (ki:epoch * t:text * (;ki)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

The F# code of this module has been verified to meet its F7 interface.

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

miTLS

A verified reference TLS implementation

miTLS :: MAC

F# Interface: MAC.fsi

F# Implementation: MAC.fs

F7 Interface: MAC.fs7

Verification status

Module list

Trusted

Idealized

Verified