From 64dfdde0aa7f7ef24e6cbf3c57e6d24efc55367e Mon Sep 17 00:00:00 2001 From: MarcoFalke Date: Tue, 13 Dec 2016 12:37:40 +0100 Subject: Squashed 'src/secp256k1/' changes from 6c527ec..8225239 8225239 Merge #433: Make the libcrypto detection fail the newer API. 12de863 Make the libcrypto detection fail the newer API. 2928420 Merge #427: Remove Schnorr from travis as well 8eecc4a Remove Schnorr from travis as well a8abae7 Merge #310: Add exhaustive test for group functions on a low-order subgroup b4ceedf Add exhaustive test for verification 83836a9 Add exhaustive tests for group arithmetic, signing, and ecmult on a small group 20b8877 Add exhaustive test for group functions on a low-order subgroup 80773a6 Merge #425: Remove Schnorr experiment e06e878 Remove Schnorr experiment 04c8ef3 Merge #407: Modify parameter order of internal functions to match API parameter order 6e06696 Merge #411: Remove guarantees about memcmp-ability 40c8d7e Merge #421: Update scalar_4x64_impl.h a922365 Merge #422: Restructure nonce clearing 3769783 Restructure nonce clearing 0f9e69d Restructure nonce clearing 9d67afa Update scalar_4x64_impl.h 7d15cd7 Merge #413: fix auto-enabled static precompuatation 00c5d2e fix auto-enabled static precompuatation 91219a1 Remove guarantees about memcmp-ability 7a49cac Merge #410: Add string.h include to ecmult_impl 0bbd5d4 Add string.h include to ecmult_impl 353c1bf Fix secp256k1_ge_set_table_gej_var parameter order 541b783 Fix secp256k1_ge_set_all_gej_var parameter order 7d893f4 Fix secp256k1_fe_inv_all_var parameter order c5b32e1 Merge #405: Make secp256k1_fe_sqrt constant time 926836a Make secp256k1_fe_sqrt constant time e2a8e92 Merge #404: Replace 3M + 4S doubling formula with 2M + 5S one 8ec49d8 Add note about 2M + 5S doubling formula 5a91bd7 Merge #400: A couple minor cleanups ac01378 build: add -DSECP256K1_BUILD to benchmark_internal build flags a6c6f99 Remove a bunch of unused stdlib #includes 65285a6 Merge #403: configure: add flag to disable OpenSSL tests a9b2a5d configure: add flag to disable OpenSSL tests b340123 Merge #402: Add support for testing quadratic residues e6e9805 Add function for testing quadratic residue field/group elements. efd953a Add Jacobi symbol test via GMP fa36a0d Merge #401: ecmult_const: unify endomorphism and non-endomorphism skew cases c6191fd ecmult_const: unify endomorphism and non-endomorphism skew cases 0b3e618 Merge #378: .gitignore build-aux cleanup 6042217 Merge #384: JNI: align shared files copyright/comments to bitcoinj's 24ad20f Merge #399: build: verify that the native compiler works for static precomp b3be852 Merge #398: Test whether ECDH and Schnorr are enabled for JNI aa0b1fd build: verify that the native compiler works for static precomp eee808d Test whether ECDH and Schnorr are enabled for JNI 7b0fb18 Merge #366: ARM assembly implementation of field_10x26 inner (rebase of #173) 001f176 ARM assembly implementation of field_10x26 inner 0172be9 Merge #397: Small fixes for sha256 3f8b78e Fix undefs in hash_impl.h 2ab4695 Fix state size in sha256 struct 6875b01 Merge #386: Add some missing `VERIFY_CHECK(ctx != NULL)` 2c52b5d Merge #389: Cast pointers through uintptr_t under JNI 43097a4 Merge #390: Update bitcoin-core GitHub links 31c9c12 Merge #391: JNI: Only call ecdsa_verify if its inputs parsed correctly 1cb2302 Merge #392: Add testcase which hits additional branch in secp256k1_scalar_sqr d2ee340 Merge #388: bench_ecdh: fix call to secp256k1_context_create 093a497 Add testcase which hits additional branch in secp256k1_scalar_sqr a40c701 JNI: Only call ecdsa_verify if its inputs parsed correctly faa2a11 Update bitcoin-core GitHub links 47b9e78 Cast pointers through uintptr_t under JNI f36f9c6 bench_ecdh: fix call to secp256k1_context_create bcc4881 Add some missing `VERIFY_CHECK(ctx != NULL)` for functions that use `ARG_CHECK` 6ceea2c align shared files copyright/comments to bitcoinj's 70141a8 Update .gitignore 7b549b1 Merge #373: build: fix x86_64 asm detection for some compilers bc7c93c Merge #374: Add note about y=0 being possible on one of the sextic twists e457018 Merge #364: JNI rebased 86e2d07 JNI library: cleanup, removed unimplemented code 3093576a JNI library bd2895f Merge pull request #371 e72e93a Add note about y=0 being possible on one of the sextic twists 3f8fdfb build: fix x86_64 asm detection for some compilers e5a9047 [Trivial] Remove double semicolons c18b869 Merge pull request #360 3026daa Merge pull request #302 03d4611 Add sage verification script for the group laws a965937 Merge pull request #361 83221ec Add experimental features to configure 5d4c5a3 Prevent damage_array in the signature test from going out of bounds. 419bf7f Merge pull request #356 03d84a4 Benchmark against OpenSSL verification git-subtree-dir: src/secp256k1 git-subtree-split: 8225239f490f79842a5a3b82ad6cc8aa11d5208e --- sage/weierstrass_prover.sage | 264 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 264 insertions(+) create mode 100644 sage/weierstrass_prover.sage (limited to 'sage/weierstrass_prover.sage') diff --git a/sage/weierstrass_prover.sage b/sage/weierstrass_prover.sage new file mode 100644 index 0000000000..03ef2ec901 --- /dev/null +++ b/sage/weierstrass_prover.sage @@ -0,0 +1,264 @@ +# Prover implementation for Weierstrass curves of the form +# y^2 = x^3 + A * x + B, specifically with a = 0 and b = 7, with group laws +# operating on affine and Jacobian coordinates, including the point at infinity +# represented by a 4th variable in coordinates. + +load("group_prover.sage") + + +class affinepoint: + def __init__(self, x, y, infinity=0): + self.x = x + self.y = y + self.infinity = infinity + def __str__(self): + return "affinepoint(x=%s,y=%s,inf=%s)" % (self.x, self.y, self.infinity) + + +class jacobianpoint: + def __init__(self, x, y, z, infinity=0): + self.X = x + self.Y = y + self.Z = z + self.Infinity = infinity + def __str__(self): + return "jacobianpoint(X=%s,Y=%s,Z=%s,inf=%s)" % (self.X, self.Y, self.Z, self.Infinity) + + +def point_at_infinity(): + return jacobianpoint(1, 1, 1, 1) + + +def negate(p): + if p.__class__ == affinepoint: + return affinepoint(p.x, -p.y) + if p.__class__ == jacobianpoint: + return jacobianpoint(p.X, -p.Y, p.Z) + assert(False) + + +def on_weierstrass_curve(A, B, p): + """Return a set of zero-expressions for an affine point to be on the curve""" + return constraints(zero={p.x^3 + A*p.x + B - p.y^2: 'on_curve'}) + + +def tangential_to_weierstrass_curve(A, B, p12, p3): + """Return a set of zero-expressions for ((x12,y12),(x3,y3)) to be a line that is tangential to the curve at (x12,y12)""" + return constraints(zero={ + (p12.y - p3.y) * (p12.y * 2) - (p12.x^2 * 3 + A) * (p12.x - p3.x): 'tangential_to_curve' + }) + + +def colinear(p1, p2, p3): + """Return a set of zero-expressions for ((x1,y1),(x2,y2),(x3,y3)) to be collinear""" + return constraints(zero={ + (p1.y - p2.y) * (p1.x - p3.x) - (p1.y - p3.y) * (p1.x - p2.x): 'colinear_1', + (p2.y - p3.y) * (p2.x - p1.x) - (p2.y - p1.y) * (p2.x - p3.x): 'colinear_2', + (p3.y - p1.y) * (p3.x - p2.x) - (p3.y - p2.y) * (p3.x - p1.x): 'colinear_3' + }) + + +def good_affine_point(p): + return constraints(nonzero={p.x : 'nonzero_x', p.y : 'nonzero_y'}) + + +def good_jacobian_point(p): + return constraints(nonzero={p.X : 'nonzero_X', p.Y : 'nonzero_Y', p.Z^6 : 'nonzero_Z'}) + + +def good_point(p): + return constraints(nonzero={p.Z^6 : 'nonzero_X'}) + + +def finite(p, *affine_fns): + con = good_point(p) + constraints(zero={p.Infinity : 'finite_point'}) + if p.Z != 0: + return con + reduce(lambda a, b: a + b, (f(affinepoint(p.X / p.Z^2, p.Y / p.Z^3)) for f in affine_fns), con) + else: + return con + +def infinite(p): + return constraints(nonzero={p.Infinity : 'infinite_point'}) + + +def law_jacobian_weierstrass_add(A, B, pa, pb, pA, pB, pC): + """Check whether the passed set of coordinates is a valid Jacobian add, given assumptions""" + assumeLaw = (good_affine_point(pa) + + good_affine_point(pb) + + good_jacobian_point(pA) + + good_jacobian_point(pB) + + on_weierstrass_curve(A, B, pa) + + on_weierstrass_curve(A, B, pb) + + finite(pA) + + finite(pB) + + constraints(nonzero={pa.x - pb.x : 'different_x'})) + require = (finite(pC, lambda pc: on_weierstrass_curve(A, B, pc) + + colinear(pa, pb, negate(pc)))) + return (assumeLaw, require) + + +def law_jacobian_weierstrass_double(A, B, pa, pb, pA, pB, pC): + """Check whether the passed set of coordinates is a valid Jacobian doubling, given assumptions""" + assumeLaw = (good_affine_point(pa) + + good_affine_point(pb) + + good_jacobian_point(pA) + + good_jacobian_point(pB) + + on_weierstrass_curve(A, B, pa) + + on_weierstrass_curve(A, B, pb) + + finite(pA) + + finite(pB) + + constraints(zero={pa.x - pb.x : 'equal_x', pa.y - pb.y : 'equal_y'})) + require = (finite(pC, lambda pc: on_weierstrass_curve(A, B, pc) + + tangential_to_weierstrass_curve(A, B, pa, negate(pc)))) + return (assumeLaw, require) + + +def law_jacobian_weierstrass_add_opposites(A, B, pa, pb, pA, pB, pC): + assumeLaw = (good_affine_point(pa) + + good_affine_point(pb) + + good_jacobian_point(pA) + + good_jacobian_point(pB) + + on_weierstrass_curve(A, B, pa) + + on_weierstrass_curve(A, B, pb) + + finite(pA) + + finite(pB) + + constraints(zero={pa.x - pb.x : 'equal_x', pa.y + pb.y : 'opposite_y'})) + require = infinite(pC) + return (assumeLaw, require) + + +def law_jacobian_weierstrass_add_infinite_a(A, B, pa, pb, pA, pB, pC): + assumeLaw = (good_affine_point(pa) + + good_affine_point(pb) + + good_jacobian_point(pA) + + good_jacobian_point(pB) + + on_weierstrass_curve(A, B, pb) + + infinite(pA) + + finite(pB)) + require = finite(pC, lambda pc: constraints(zero={pc.x - pb.x : 'c.x=b.x', pc.y - pb.y : 'c.y=b.y'})) + return (assumeLaw, require) + + +def law_jacobian_weierstrass_add_infinite_b(A, B, pa, pb, pA, pB, pC): + assumeLaw = (good_affine_point(pa) + + good_affine_point(pb) + + good_jacobian_point(pA) + + good_jacobian_point(pB) + + on_weierstrass_curve(A, B, pa) + + infinite(pB) + + finite(pA)) + require = finite(pC, lambda pc: constraints(zero={pc.x - pa.x : 'c.x=a.x', pc.y - pa.y : 'c.y=a.y'})) + return (assumeLaw, require) + + +def law_jacobian_weierstrass_add_infinite_ab(A, B, pa, pb, pA, pB, pC): + assumeLaw = (good_affine_point(pa) + + good_affine_point(pb) + + good_jacobian_point(pA) + + good_jacobian_point(pB) + + infinite(pA) + + infinite(pB)) + require = infinite(pC) + return (assumeLaw, require) + + +laws_jacobian_weierstrass = { + 'add': law_jacobian_weierstrass_add, + 'double': law_jacobian_weierstrass_double, + 'add_opposite': law_jacobian_weierstrass_add_opposites, + 'add_infinite_a': law_jacobian_weierstrass_add_infinite_a, + 'add_infinite_b': law_jacobian_weierstrass_add_infinite_b, + 'add_infinite_ab': law_jacobian_weierstrass_add_infinite_ab +} + + +def check_exhaustive_jacobian_weierstrass(name, A, B, branches, formula, p): + """Verify an implementation of addition of Jacobian points on a Weierstrass curve, by executing and validating the result for every possible addition in a prime field""" + F = Integers(p) + print "Formula %s on Z%i:" % (name, p) + points = [] + for x in xrange(0, p): + for y in xrange(0, p): + point = affinepoint(F(x), F(y)) + r, e = concrete_verify(on_weierstrass_curve(A, B, point)) + if r: + points.append(point) + + for za in xrange(1, p): + for zb in xrange(1, p): + for pa in points: + for pb in points: + for ia in xrange(2): + for ib in xrange(2): + pA = jacobianpoint(pa.x * F(za)^2, pa.y * F(za)^3, F(za), ia) + pB = jacobianpoint(pb.x * F(zb)^2, pb.y * F(zb)^3, F(zb), ib) + for branch in xrange(0, branches): + assumeAssert, assumeBranch, pC = formula(branch, pA, pB) + pC.X = F(pC.X) + pC.Y = F(pC.Y) + pC.Z = F(pC.Z) + pC.Infinity = F(pC.Infinity) + r, e = concrete_verify(assumeAssert + assumeBranch) + if r: + match = False + for key in laws_jacobian_weierstrass: + assumeLaw, require = laws_jacobian_weierstrass[key](A, B, pa, pb, pA, pB, pC) + r, e = concrete_verify(assumeLaw) + if r: + if match: + print " multiple branches for (%s,%s,%s,%s) + (%s,%s,%s,%s)" % (pA.X, pA.Y, pA.Z, pA.Infinity, pB.X, pB.Y, pB.Z, pB.Infinity) + else: + match = True + r, e = concrete_verify(require) + if not r: + print " failure in branch %i for (%s,%s,%s,%s) + (%s,%s,%s,%s) = (%s,%s,%s,%s): %s" % (branch, pA.X, pA.Y, pA.Z, pA.Infinity, pB.X, pB.Y, pB.Z, pB.Infinity, pC.X, pC.Y, pC.Z, pC.Infinity, e) + print + + +def check_symbolic_function(R, assumeAssert, assumeBranch, f, A, B, pa, pb, pA, pB, pC): + assumeLaw, require = f(A, B, pa, pb, pA, pB, pC) + return check_symbolic(R, assumeLaw, assumeAssert, assumeBranch, require) + +def check_symbolic_jacobian_weierstrass(name, A, B, branches, formula): + """Verify an implementation of addition of Jacobian points on a Weierstrass curve symbolically""" + R. = PolynomialRing(QQ,8,order='invlex') + lift = lambda x: fastfrac(R,x) + ax = lift(ax) + ay = lift(ay) + Az = lift(Az) + bx = lift(bx) + by = lift(by) + Bz = lift(Bz) + Ai = lift(Ai) + Bi = lift(Bi) + + pa = affinepoint(ax, ay, Ai) + pb = affinepoint(bx, by, Bi) + pA = jacobianpoint(ax * Az^2, ay * Az^3, Az, Ai) + pB = jacobianpoint(bx * Bz^2, by * Bz^3, Bz, Bi) + + res = {} + + for key in laws_jacobian_weierstrass: + res[key] = [] + + print ("Formula " + name + ":") + count = 0 + for branch in xrange(branches): + assumeFormula, assumeBranch, pC = formula(branch, pA, pB) + pC.X = lift(pC.X) + pC.Y = lift(pC.Y) + pC.Z = lift(pC.Z) + pC.Infinity = lift(pC.Infinity) + + for key in laws_jacobian_weierstrass: + res[key].append((check_symbolic_function(R, assumeFormula, assumeBranch, laws_jacobian_weierstrass[key], A, B, pa, pb, pA, pB, pC), branch)) + + for key in res: + print " %s:" % key + val = res[key] + for x in val: + if x[0] is not None: + print " branch %i: %s" % (x[1], x[0]) + + print -- cgit v1.2.3