From 4b55dad303d4e14c02c8c563a8e2fde962b8986e Mon Sep 17 00:00:00 2001 From: dkostic Date: Wed, 15 May 2024 16:10:30 -0700 Subject: [PATCH] addressing CR --- crypto/fipsmodule/ec/ec_nistp.c | 25 +++++++++++++------------ crypto/fipsmodule/ec/ec_nistp.h | 8 ++------ 2 files changed, 15 insertions(+), 18 deletions(-) diff --git a/crypto/fipsmodule/ec/ec_nistp.c b/crypto/fipsmodule/ec/ec_nistp.c index e5972d66d8..a4484dc06c 100644 --- a/crypto/fipsmodule/ec/ec_nistp.c +++ b/crypto/fipsmodule/ec/ec_nistp.c @@ -1,9 +1,5 @@ -/* ------------------------------------------------------------------------------------- - Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. - SPDX-License-Identifier: Apache-2.0 OR ISC ------------------------------------------------------------------------------------- -*/ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR ISC // In this file we will implement elliptic curve point operations for // NIST curves P-256, P-384, and P-521. The idea is to implement the operations @@ -19,8 +15,8 @@ // // | op | P-521 | P-384 | P-256 | // |----------------------------| -// | 1. | x | x | x* | -// | 2. | | | | +// | 1. | | | | +// | 2. | x | x | x* | // | 3. | | | | // | 4. | | | | // | 5. | | | | @@ -49,12 +45,17 @@ typedef ec_nistp_felem_limb ec_nistp_felem[NISTP_FELEM_MAX_NUM_OF_LIMBS]; // // ec_nistp_point_double calculates 2*(x_in, y_in, z_in) // -// The method is taken from: +// The method is based on: // http://hyperelliptic.org/EFD/g1p/auto-shortw-jacobian-3.html#doubling-dbl-2001-b +// for which there is a Coq transcription and correctness proof: +// +// +// +// However, we slighty changed the computation for efficiency (see the full +// explanation within the function body), which makes the Coq proof above +// not applicable to our implementation. +// TODO(awslc): Write a Coq correctness proof for our version of the algorithm. // -// Coq transcription and correctness proof: -// -// // Outputs can equal corresponding inputs, i.e., x_out == x_in is allowed; // while x_out == y_in is not (maybe this works, but it's not tested). void ec_nistp_point_double(const ec_nistp_felem_meth *ctx, diff --git a/crypto/fipsmodule/ec/ec_nistp.h b/crypto/fipsmodule/ec/ec_nistp.h index eec0c54e14..027380581f 100644 --- a/crypto/fipsmodule/ec/ec_nistp.h +++ b/crypto/fipsmodule/ec/ec_nistp.h @@ -1,9 +1,5 @@ -/* ------------------------------------------------------------------------------------- - Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. - SPDX-License-Identifier: Apache-2.0 OR ISC ------------------------------------------------------------------------------------- -*/ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR ISC #ifndef EC_NISTP_H #define EC_NISTP_H