diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-03-24 18:15:48 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-03-24 18:15:48 -0400 |
commit | 824d84126187f359605527beb947a385e43761c4 (patch) | |
tree | dd9369490e09e7ad47236db163a45194f0ef3088 | |
parent | 3d75a97748a6ce76364324762b919d3e54a4cac3 (diff) |
ed25519 derivation: pair programming with jgross... slow progress
-rw-r--r-- | src/Spec/EdDSA.v | 2 | ||||
-rw-r--r-- | src/Specific/Ed25519.v | 148 |
2 files changed, 128 insertions, 22 deletions
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index c9660bd98..3decae6a7 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -74,9 +74,9 @@ Section EdDSA. Definition verify (A_:publickey) {n:nat} (M : Word.word n) (sig:signature) : bool := let R_ := Word.split1 b b sig in let S_ := Word.split2 b b sig in + match dec S_ : option (F (BinInt.Z.of_nat l)) with None => false | Some S' => match dec A_ : option point with None => false | Some A => match dec R_ : option point with None => false | Some R => - match dec S_ : option (F (BinInt.Z.of_nat l)) with None => false | Some S' => if BinInt.Z.to_nat (FieldToZ S') * B == R + (H (R_ ++ A_ ++ M)) * A then true else false end diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index efee4e7af..a705ceb90 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -14,7 +14,69 @@ Local Arguments H {_} _. Local Arguments scalarMultM1 {_} {_} _ _. Local Arguments unifiedAddM1 {_} {_} _ _. -Lemma sharper_verify : { verify | forall pk l msg sig, verify pk l msg sig = ed25519_verify pk l msg sig}. +Ltac set_evars := + repeat match goal with + | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E) + end. +Ltac subst_evars := + repeat match goal with + | [ e := ?E |- _ ] => is_evar E; subst e + end. + +Axiom point_eqb : forall {prm : TwistedEdwardsParams}, point -> point -> bool. +Axiom point_eqb_correct : forall P Q, point_eqb P Q = if point_eq_dec P Q then true else false. + +Require Import Coq.Setoids.Setoid. +Require Import Coq.Classes.Morphisms. +Global Instance option_rect_Proper_nd {A T} + : Proper ((pointwise_relation _ eq) ==> eq ==> eq ==> eq) (@option_rect A (fun _ => T)). +Proof. + intros ?? H ??? [|]??; subst; simpl; congruence. +Qed. + +Global Instance option_rect_Proper_nd' {A T} + : Proper ((pointwise_relation _ eq) ==> eq ==> forall_relation (fun _ => eq)) (@option_rect A (fun _ => T)). +Proof. + intros ?? H ??? [|]; subst; simpl; congruence. +Qed. + +Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?T))) => exact (@option_rect_Proper_nd' A T) : typeclass_instances. + +Lemma option_rect_option_map : forall {A B C} (f:A->B) some none v, + option_rect (fun _ => C) (fun x => some (f x)) none v = option_rect (fun _ => C) some none (option_map f v). +Proof. + destruct v; reflexivity. +Qed. + +Axiom decode_scalar : word b -> option N. +Local Existing Instance Ed25519.FlEncoding. +Axiom decode_scalar_correct : forall x, decode_scalar x = option_map (fun x : F (Z.of_nat Ed25519.l) => Z.to_N x) (dec x). + +Local Infix "==?" := point_eqb (at level 70) : E_scope. + +Axiom negate : point -> point. +Definition point_sub P Q := (P + negate Q)%E. +Infix "-" := point_sub : E_scope. +Axiom solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E. + +Axiom negateExtended : extendedPoint -> extendedPoint. +Axiom negateExtended_correct : forall P, negate (unExtendedPoint P) = unExtendedPoint (negateExtended P). + +Local Existing Instance PointEncoding. +Axiom decode_point_eq : forall (P_ Q_ : word (S (b-1))) (P Q:point), dec P_ = Some P -> dec Q_ = Some Q -> weqb P_ Q_ = (P ==? Q)%E. + +Lemma decode_test_encode_test : forall S_ X, option_rect (fun _ : option point => bool) + (fun S : point => (S ==? X)%E) false (dec S_) = weqb S_ (enc X). +Proof. + intros. + destruct (dec S_) eqn:H. + { symmetry; eauto using decode_point_eq, encoding_valid. } + { simpl @option_rect. + destruct (weqb S_ (enc X)) eqn:Heqb; trivial. + apply weqb_true_iff in Heqb. subst. rewrite encoding_valid in H; discriminate. } +Qed. + +Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. Proof. eexists; intros. cbv [ed25519_verify EdDSA.verify @@ -22,28 +84,72 @@ Proof. EdDSA.E EdDSA.B EdDSA.b EdDSA.l EdDSA.H EdDSA.PointEncoding EdDSA.FlEncoding EdDSA.FqEncoding]. - (* zoom in to the interesting case *) - repeat match goal with |- context[match ?a with Some x => _ | _ => _ end] => - let n := fresh x in - let H := fresh "Heq" x in - destruct a as [x|] - end. + etransitivity. + Focus 2. + { repeat match goal with + | [ |- ?x = ?x ] => reflexivity + | [ |- _ = match ?a with None => ?N | Some x => @?S x end :> ?T ] + => etransitivity; + [ + | refine (_ : option_rect (fun _ => T) _ N a = _); + let S' := match goal with |- option_rect _ ?S' _ _ = _ => S' end in + refine (option_rect (fun a' => option_rect (fun _ => T) S' N a' = match a' with None => N | Some x => S x end) + (fun x => _) _ a); intros; simpl @option_rect ]; + [ reflexivity | .. ] + end. + set_evars. + rewrite<- point_eqb_correct. + rename x0 into R. rename x1 into S. rename x into A. + rewrite solve_for_R. + let p1 := constr:(scalarMultM1_rep eq_refl) in + let p2 := constr:(unifiedAddM1_rep eq_refl) in + repeat match goal with + | |- context [(_ * ?P)%E] => + rewrite <-(unExtendedPoint_mkExtendedPoint P); + rewrite <-p1 + | |- context [(?P + unExtendedPoint _)%E] => + rewrite <-(unExtendedPoint_mkExtendedPoint P); + rewrite p2 + end; + rewrite ?Znat.Z_nat_N, <-?Word.wordToN_nat; + subst_evars; + reflexivity. + } Unfocus. + + etransitivity. + Focus 2. + { lazymatch goal with |- _ = option_rect _ _ ?false ?dec => + symmetry; etransitivity; [|eapply (option_rect_option_map (fun (x:F _) => Z.to_N x) _ false dec)] + end. + eapply option_rect_Proper_nd; [intro|reflexivity..]. + match goal with + | [ |- ?RHS = ?e ?v ] + => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in + unify e RHS' + end. + reflexivity. + } Unfocus. + rewrite <-decode_scalar_correct. + + etransitivity. + Focus 2. + { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + symmetry; apply decode_test_encode_test. + } Unfocus. + + etransitivity. + Focus 2. + { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + unfold point_sub. rewrite negateExtended_correct. + let p := constr:(unifiedAddM1_rep eq_refl) in rewrite p. + reflexivity. + } Unfocus. - let p1 := constr:(scalarMultM1_rep eq_refl) in - let p2 := constr:(unifiedAddM1_rep eq_refl) in - repeat match goal with - | |- context [(?n * ?P)%E] => - rewrite <-(unExtendedPoint_mkExtendedPoint P); - erewrite <-p1 - | |- context [(?P + unExtendedPoint _)%E] => - rewrite <-(unExtendedPoint_mkExtendedPoint P); - erewrite p2 - end. - rewrite !Znat.Z_nat_N, <-!Word.wordToN_nat. - cbv [scalarMultM1 iter_op]. - Local Arguments funexp {_} _ {_} {_}. (* do not display the initializer and iteration bound for now *) cbv iota zeta delta [test_and_op]. + Local Arguments funexp {_} _ {_} {_}. (* do not display the initializer and iteration bound for now *) - + Axiom rep : forall {m}, list Z -> F m -> Prop. + Axiom decode_point_limbs : word (S (b-1)) -> option (list Z * list Z). + Axiom point_dec_rep : forall P_ P lx ly, dec P_ = Some P -> decode_point_limbs P_ = Some (lx, ly) -> rep lx (fst (proj1_sig P)) /\ rep ly (fst (proj1_sig P)). Admitted.
\ No newline at end of file |