Add links to proofs of elliptic curve formulas.
Change-Id: I166f740185f26770b51759714efd5d634fbcc173
Reviewed-on: https://boringssl-review.googlesource.com/24424
Reviewed-by: David Benjamin <davidben@google.com>
diff --git a/third_party/fiat/curve25519.c b/third_party/fiat/curve25519.c
index d54aa83..92a965a 100644
--- a/third_party/fiat/curve25519.c
+++ b/third_party/fiat/curve25519.c
@@ -4928,6 +4928,24 @@
e[0] &= 248;
e[31] &= 127;
e[31] |= 64;
+
+ // The following implementation was transcribed to Coq and proven to
+ // correspond to unary scalar multiplication in affine coordinates given that
+ // x1 != 0 is the x coordinate of some point on the curve. It was also checked
+ // in Coq that doing a ladderstep with x1 = x3 = 0 gives z2' = z3' = 0, and z2
+ // = z3 = 0 gives z2' = z3' = 0. The statement was quantified over the
+ // underlying field, so it applies to Curve25519 itself and the quadratic
+ // twist of Curve25519. It was not proven in Coq that prime-field arithmetic
+ // correctly simulates extension-field arithmetic on prime-field values.
+ // The decoding of the byte array representation of e was not considered.
+ // Specification of Montgomery curves in affine coordinates:
+ // <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Spec/MontgomeryCurve.v#L27>
+ // Proof that these form a group that is isomorphic to a Weierstrass curve:
+ // <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/AffineProofs.v#L35>
+ // Coq transcription and correctness proof of the loop (where scalarbits=255):
+ // <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZ.v#L118>
+ // <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L278>
+ // preconditions: 0 <= e < 2^255 (not necessarily e < order), fe_invert(0) = 0
fe_frombytes(&x1, point);
fe_1(&x2);
fe_0(&z2);
@@ -4937,11 +4955,22 @@
unsigned swap = 0;
int pos;
for (pos = 254; pos >= 0; --pos) {
+ // loop invariant as of right before the test, for the case where x1 != 0:
+ // pos >= -1; if z2 = 0 then x2 is nonzero; if z3 = 0 then x3 is nonzero
+ // let r := e >> (pos+1) in the following equalities of projective points:
+ // to_xz (r*P) === if swap then (x3, z3) else (x2, z2)
+ // to_xz ((r+1)*P) === if swap then (x2, z2) else (x3, z3)
+ // x1 is the nonzero x coordinate of the nonzero point (r*P-(r+1)*P)
unsigned b = 1 & (e[pos / 8] >> (pos & 7));
swap ^= b;
fe_cswap(&x2, &x3, swap);
fe_cswap(&z2, &z3, swap);
swap = b;
+ // Coq transcription of ladderstep formula (called from transcribed loop):
+ // <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZ.v#L89>
+ // <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L131>
+ // x1 != 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L217>
+ // x1 = 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/src/Curves/Montgomery/XZProofs.v#L147>
fe_sub(&tmp0l, &x3, &z3);
fe_sub(&tmp1l, &x2, &z2);
fe_add(&x2l, &x2, &z2);
@@ -4961,6 +4990,7 @@
fe_mul_ttt(&z3, &x1, &z2);
fe_mul_tll(&z2, &tmp1l, &tmp0l);
}
+ // here pos=-1, so r=e, so to_xz (e*P) === if swap then (x3, z3) else (x2, z2)
fe_cswap(&x2, &x3, swap);
fe_cswap(&z2, &z3, swap);
diff --git a/third_party/fiat/p256.c b/third_party/fiat/p256.c
index 25ef383..9c7de35 100644
--- a/third_party/fiat/p256.c
+++ b/third_party/fiat/p256.c
@@ -983,12 +983,24 @@
// Building on top of the field operations we have the operations on the
// elliptic curve group itself. Points on the curve are represented in Jacobian
// coordinates.
+//
+// Both operations were transcribed to Coq and proven to correspond to naive
+// implementations using Affine coordinates, for all suitable fields. In the
+// Coq proofs, issues of constant-time execution and memory layout (aliasing)
+// conventions were not considered. Specification of affine coordinates:
+// <https://github.com/mit-plv/fiat-crypto/blob/79f8b5f39ed609339f0233098dee1a3c4e6b3080/src/Spec/WeierstrassCurve.v#L28>
+// As a sanity check, a proof that these points form a commutative group:
+// <https://github.com/mit-plv/fiat-crypto/blob/79f8b5f39ed609339f0233098dee1a3c4e6b3080/src/Curves/Weierstrass/AffineProofs.v#L33>
// point_double calculates 2*(x_in, y_in, z_in)
//
// The method is taken from:
// http://hyperelliptic.org/EFD/g1p/auto-shortw-jacobian-3.html#doubling-dbl-2001-b
//
+// Coq transcription and correctness proof:
+// <https://github.com/mit-plv/fiat-crypto/blob/79f8b5f39ed609339f0233098dee1a3c4e6b3080/src/Curves/Weierstrass/Jacobian.v#L93>
+// <https://github.com/mit-plv/fiat-crypto/blob/79f8b5f39ed609339f0233098dee1a3c4e6b3080/src/Curves/Weierstrass/Jacobian.v#L201>
+//
// 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).
static void point_double(fe x_out, fe y_out, fe z_out,
@@ -1037,6 +1049,10 @@
// http://hyperelliptic.org/EFD/g1p/auto-shortw-jacobian-3.html#addition-add-2007-bl,
// adapted for mixed addition (z2 = 1, or z2 = 0 for the point at infinity).
//
+// Coq transcription and correctness proof:
+// <https://github.com/mit-plv/fiat-crypto/blob/79f8b5f39ed609339f0233098dee1a3c4e6b3080/src/Curves/Weierstrass/Jacobian.v#L135>
+// <https://github.com/mit-plv/fiat-crypto/blob/79f8b5f39ed609339f0233098dee1a3c4e6b3080/src/Curves/Weierstrass/Jacobian.v#L205>
+//
// This function includes a branch for checking whether the two input points
// are equal, (while not equal to the point at infinity). This case never
// happens during single point multiplication, so there is no timing leak for
