Revision c59dd0c413b6111e9472f7f1dac42235893ce07c authored by Jonathan Protzenko on 31 March 2020, 17:43:02 UTC, committed by Jonathan Protzenko on 31 March 2020, 17:43:02 UTC
1 parent 4f4b329
Spec.HMAC_DRBG.Test.fst
module Spec.HMAC_DRBG.Test
open FStar.Seq
open Lib.IntTypes
open Lib.Meta
open Spec.Agile.HMAC
open Spec.HMAC_DRBG
open Spec.HMAC_DRBG.Test.Vectors
#set-options "--max_fuel 1 --max_ifuel 1 --z3rlimit 50"
let print_and_compare (len:size_nat) (test_expected test_result:lbytes len) : All.ML bool =
// Cheap alternative to friend Lib.IntTypes / Lib.RawIntTypes
assume (squash (uint8 == UInt8.t));
IO.print_string "\n\nResult: ";
List.iter (fun a -> IO.print_uint8_hex_pad a) (seq_to_list test_result);
IO.print_string "\nExpected: ";
List.iter (fun a -> IO.print_uint8_hex_pad a) (seq_to_list test_expected);
Lib.ByteSequence.lbytes_eq #len test_expected test_result
let test_vec
{a; entropy_input; entropy_input_reseed; nonce; personalization_string;
additional_input_reseed; additional_input_1; additional_input_2;
returned_bits}
=
let returned_bytes_len = String.strlen returned_bits / 2 in
let entropy_input_len = String.strlen entropy_input / 2 in
let entropy_input_reseed_len = String.strlen entropy_input_reseed / 2 in
let nonce_len = String.strlen nonce / 2 in
let personalization_string_len = String.strlen personalization_string / 2 in
let additional_input_reseed_len = String.strlen additional_input_reseed / 2 in
let additional_input_1_len = String.strlen additional_input_1 / 2 in
let additional_input_2_len = String.strlen additional_input_2 / 2 in
let returned_bits_len = String.strlen returned_bits / 2 in
if not (is_supported_alg a &&
min_length a <= entropy_input_len &&
entropy_input_len <= max_length &&
min_length a / 2 <= nonce_len &&
nonce_len <= max_length &&
personalization_string_len <= max_personalization_string_length &&
entropy_input_reseed_len <= max_length &&
additional_input_reseed_len <= max_additional_input_length &&
additional_input_1_len <= max_additional_input_length &&
additional_input_2_len <= max_additional_input_length &&
0 < returned_bits_len &&
returned_bits_len <= max_output_length)
then false
else
let _ = hmac_input_bound a in
let st = instantiate #a
(from_hex entropy_input) (from_hex nonce) (from_hex personalization_string)
in
let st = reseed st
(from_hex entropy_input_reseed) (from_hex additional_input_reseed)
in
match generate st returned_bytes_len (from_hex additional_input_1) with
| None -> false
| Some (_, st) ->
match generate st returned_bytes_len (from_hex additional_input_2) with
| None -> false
| Some (out, st) -> print_and_compare returned_bytes_len (from_hex returned_bits) out
let test () =
let result = List.for_all test_vec test_vectors in
if result then
begin
IO.print_string "\n\n[HMAC-DRBG] PASS\n";
true
end
else
begin
IO.print_string "\n\n[HMAC-DRBG] FAIL\n";
false
end
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...