Moving ECDH derive spec to its own file.

apetcher-amazon · Apr 8, 2024 · 57dec43 · 57dec43
1 parent f5dad26
commit 57dec43
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 10 deletions.
diff --git a/SAW/proof/EC/EC.saw b/SAW/proof/EC/EC.saw
@@ -26,7 +26,6 @@ include "../EVP/EVP_CTX.saw";
 import "../../spec/EC/EC_FIPS.cry";
 include "EC_P384_private.saw";
 
-
 let points_to_p384_bignum_st ptr d_ptr flags = points_to_bignum_st ptr d_ptr ec_words ec_words flags;
 
 
@@ -1412,7 +1411,7 @@ ec_felem_to_bytes_ov <- llvm_verify m
   "ec_felem_to_bytes"
   [bignum_fromlebytes_6_ov,
   bignum_tolebytes_6_ov,
-  bignum_deamont_p384_ov
+  bignum_deamont_p384_same_ov
   ]
   true
   ec_felem_to_bytes_spec
@@ -1427,7 +1426,7 @@ ec_get_x_coordinate_as_bytes_ov <- llvm_verify m
   [BN_num_bytes_ec_bits_ov,
   bignum_tolebytes_6_ov,
   bignum_fromlebytes_6_ov,
-  bignum_deamont_p384_ov, 
+  bignum_deamont_p384_same_ov, 
   ec_GFp_nistp384_point_get_affine_coordinates_x_ov,
   ec_felem_to_bytes_ov]
   true

diff --git a/SAW/proof/ECDH/ECDH.saw b/SAW/proof/ECDH/ECDH.saw
@@ -7,10 +7,8 @@
 import "../../../cryptol-specs/Common/EC/EC_P384.cry";
 import "../../../cryptol-specs/Common/utils.cry";
 
-
 include "../ECDSA/goal-rewrites.saw";
 
-
 /*
  * Verification parameters.
  */
@@ -29,6 +27,8 @@ include "../common/memory.saw";
 include "../BN/BN.saw";
 include "../EC/EC.saw";
 
+import "../../spec/EC/ECDH.cry";
+
 
 let ptr_to_new_evp_pkey_ctx_st pkey_ptr = do {
   ptr <- crucible_alloc (llvm_struct "struct.evp_pkey_ctx_st");

diff --git a/SAW/spec/EC/ECDH.cry b/SAW/spec/EC/ECDH.cry
@@ -0,0 +1,17 @@
+/*
+ * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ * SPDX-License-Identifier: Apache-2.0
+*/
+
+module ECDH where
+
+import Common::EC::EC_P384
+import EC_primitives
+import EC_P384_5
+
+ECDH_derive_bv : JacobianBVPoint -> scalar -> [bit_length]
+ECDH_derive_bv peer_pub_key priv_key =
+ reverse_bytes (felem_to_bytes (felem_from_mont (felem_from_bytes (jacobianToAffine (point_mul_generic peer_pub_key priv_key)).X))) 
+
+
+
diff --git a/SAW/spec/EC/EC_mul.cry b/SAW/spec/EC/EC_mul.cry
@@ -375,9 +375,4 @@ validate_one_wrapper: () -> felem -> Bit
 validate_one_wrapper _ x = validate_one x
 
 
-ECDH_derive_bv : JacobianBVPoint -> scalar -> [bit_length]
-ECDH_derive_bv peer_pub_key priv_key =
- reverse_bytes (felem_to_bytes (felem_from_mont (felem_from_bytes (jacobianToAffine (point_mul_generic peer_pub_key priv_key)).X))) 
-
-