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()20 void 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