1 /* 2 * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. 3 * 4 * Licensed under the Apache License, Version 2.0 (the "License"). 5 * You may not use this file except in compliance with the License. 6 * A copy of the License is located at 7 * 8 * http://aws.amazon.com/apache2.0 9 * 10 * or in the "license" file accompanying this file. This file is distributed 11 * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either 12 * express or implied. See the License for the specific language governing 13 * permissions and limitations under the License. 14 */ 15 16 #include <cbmc_proof/cbmc_utils.h> 17 18 #include "crypto/s2n_hmac.h" 19 s2n_hmac_hash_block_size_harness()20void s2n_hmac_hash_block_size_harness() 21 { 22 /* Non-deterministic inputs. */ 23 s2n_hmac_algorithm hmac_alg; 24 uint16_t * block_size = malloc(sizeof(*block_size)); 25 26 /* Operation under verification. */ 27 if (s2n_hmac_hash_block_size(hmac_alg, block_size) == S2N_SUCCESS) { 28 /* Post-conditions. */ 29 switch(hmac_alg) { 30 case S2N_HMAC_NONE: 31 case S2N_HMAC_MD5: 32 case S2N_HMAC_SHA1: 33 case S2N_HMAC_SHA224: 34 case S2N_HMAC_SSLv3_MD5: 35 case S2N_HMAC_SSLv3_SHA1: 36 case S2N_HMAC_SHA256: 37 assert(*block_size == 64); break; 38 case S2N_HMAC_SHA384: 39 case S2N_HMAC_SHA512: 40 assert(*block_size == 128); break; 41 default: 42 __CPROVER_assert(0, "Unssuported algorithm."); 43 } 44 } 45 } 46