From 6a316e99febd6799db8b32d14de5ab68115e97d1 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 10 Oct 2016 14:08:29 -0400 Subject: Spec.Ed25519: prove that Curve25519 is an elliptic curve --- src/Spec/Ed25519.v | 28 +++++++++++++++++++++------- 1 file changed, 21 insertions(+), 7 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index bdafa10fe..51b1b0831 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -4,6 +4,25 @@ Require Import Crypto.Spec.EdDSA. Require ModularArithmetic.PrimeFieldTheorems. (* to know that Z mod p is a field *) +(* TODO: move this to a separate file *) +Require Crypto.Util.Decidable. +Require Crypto.Util.Tactics. +Module Pre. + Local Open Scope F_scope. + Lemma curve25519_params_ok {prime_q:Znumtheory.prime (2^255-19)} : + @E.twisted_edwards_params (F (2 ^ 255 - 19)) (@eq (F (2 ^ 255 - 19))) (@F.zero (2 ^ 255 - 19)) + (@F.one (2 ^ 255 - 19)) (@F.add (2 ^ 255 - 19)) (@F.mul (2 ^ 255 - 19)) + (@F.opp (2 ^ 255 - 19) 1) + (@F.opp (2 ^ 255 - 19) (F.of_Z (2 ^ 255 - 19) 121665) / F.of_Z (2 ^ 255 - 19) 121666). + Proof. + pose (@PrimeFieldTheorems.F.Decidable_square (2^255-19) _); + Tactics.specialize_by Decidable.vm_decide; split; Decidable.vm_decide_no_check. + Qed. +End Pre. +(* these 2 proofs can be generated using https://github.com/andres-erbsen/safecurves-primes *) +Axiom prime_q : Znumtheory.prime (2^255-19). Global Existing Instance prime_q. +Axiom prime_l : Znumtheory.prime (2^252 + 27742317777372353535851937790883648493). Global Existing Instance prime_l. + Section Ed25519. Local Open Scope Z_scope. @@ -30,8 +49,7 @@ Section Ed25519. Global Instance curve_params : E.twisted_edwards_params (F:=Fq) (Feq:=Logic.eq) (Fzero:=F.zero) (Fone:=F.one) (Fadd:=F.add) (Fmul:=F.mul) - (a:=a) (d:=d). - Admitted. (* TODO(andreser): prove in a separate file *) + (a:=a) (d:=d). Proof Pre.curve25519_params_ok. Definition E : Type := E.point (F:=Fq) (Feq:=Logic.eq) (Fone:=F.one) (Fadd:=F.add) (Fmul:=F.mul) @@ -42,10 +60,6 @@ Section Ed25519. Axiom Eenc : E -> Word.word b. (* TODO(jadep) *) Axiom Senc : Fl -> Word.word b. (* TODO(jadep) *) - (* these 2 proofs can be generated using https://github.com/andres-erbsen/safecurves-primes *) - Axiom prime_q : Znumtheory.prime q. Global Existing Instance prime_q. - Axiom prime_l : Znumtheory.prime l. Global Existing Instance prime_l. - Require Import Crypto.Util.Decidable. Definition ed25519 : EdDSA (E:=E) (Eadd:=E.add) (Ezero:=E.zero) (EscalarMult:=E.mul) (B:=B) @@ -53,5 +67,5 @@ Section Ed25519. (Eeq:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.eq) (* TODO: move defn *) (l:=l) (b:=b) (n:=n) (c:=c) (Eenc:=Eenc) (Senc:=Senc) (H:=H). - Admitted. (* TODO(andreser): prove in a separate file *) + Admitted. End Ed25519. \ No newline at end of file -- cgit v1.2.3