This directory contains the bulk of the Coq source files associated with
our formal verification of the HMAC-DRBG cryptographic primitive.

The FCF development described in Sections 3 and 4 is contained in
  file ../fcf/HMAC_DRBG_nonadaptive.v, with constructions (functions,
  games, and lemmas/theorems) named in accordance with the paper.
  In particular, the games G_real and G_ideal are in lines 308-311 and
  450-452, respectively, and the proof of their closeness is in lines 4563-4571.
 
hmac_drbg.c is the C source file, based on mbedtls' implementation
   https://github.com/ARMmbed/mbedtls/blob/development/library/hmac_drbg.c.
   We started from mbedtls version 2.1.1., and added additional functions
   that connect the implementation of DRBG to ../sha/hmac.c, verified
   previously.

hmac_drbg.v is the Clight AST produced from hmac_drbg.c by CompCert's
   frontend tool, clightgen.

HMAC256_DRBG_functional_prog.v contains the functional programs,
   by instantiating formalizations of more primitive functions from 
   DRBG_functions, HMAC_DRBG_algorithms, according to the structure of 
   NIST 800-90A.

drbg_protocol_specs.v contains API specifications using the abstract
representation predicate AREP. In particular, the spec for
mbedtls_hmac_drbg_random given in Figure 1 is in lines 247-263. The
proofs of the function bodies are in the remainder of this file, and
in verif_hmac_drbg_generate_abs.v (for random_with_add) and
verif_hmac_drbg_other (for free, set parameters, etc). The file imports
auxiliary constructions from spec_hmac_drbg.v which also contains more
general function specifications that don't make use of AREP and also
cover error situations.

The file linking the two specifications, i.e. relating mbedtls_generate
to the core of the generate function used in the FCF proofs, is
HMAC256_DRBG_bridge_to_FCF.v.
