From 2e96e2cab74d00b40188b00a4e90eeeaa1c46706 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 15:08:21 -0400 Subject: EdDSA: prove things about spec --- .../DerivationsOptionRectLetInEncoding.v | 59 +------------- src/Experiments/EdDSARefinement.v | 91 ++++++++++++++++++++++ src/Experiments/SpecEd25519.v | 8 +- 3 files changed, 96 insertions(+), 62 deletions(-) create mode 100644 src/Experiments/EdDSARefinement.v (limited to 'src/Experiments') diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v index e5b74085e..c0b6be25b 100644 --- a/src/Experiments/DerivationsOptionRectLetInEncoding.v +++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v @@ -150,63 +150,6 @@ Proof. end. Qed. -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. - -Lemma option_rect_function {A B C S' N' v} f - : f (option_rect (fun _ : option A => option B) S' N' v) - = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v. -Proof. destruct v; reflexivity. Qed. -Local Ltac commute_option_rect_Let_In := (* pull let binders out side of option_rect pattern matching *) - idtac; - lazymatch goal with - | [ |- ?LHS = option_rect ?P ?S ?N (Let_In ?x ?f) ] - => (* we want to just do a [change] here, but unification is stupid, so we have to tell it what to unfold in what order *) - cut (LHS = Let_In x (fun y => option_rect P S N (f y))); cbv beta; - [ set_evars; - let H := fresh in - intro H; - rewrite H; - clear; - abstract (cbv [Let_In]; reflexivity) - | ] - end. - -(** TODO: possibly move me, remove local *) -Local Ltac replace_option_match_with_option_rect := - idtac; - lazymatch goal with - | [ |- _ = ?RHS :> ?T ] - => lazymatch RHS with - | match ?a with None => ?N | Some x => @?S x end - => replace RHS with (option_rect (fun _ => T) S N a) by (destruct a; reflexivity) - end - end. -Local Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect _ _ _ (Some _)] *) - repeat match goal with - | [ |- context[option_rect ?P ?S ?N None] ] - => change (option_rect P S N None) with N - | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ] - => change (option_rect P S N (Some x)) with (S x); cbv beta - end. - Definition COMPILETIME {T} (x:T) : T := x. Lemma N_to_nat_le_mono : forall a b, (a <= b)%N -> (N.to_nat a <= N.to_nat b)%nat. @@ -348,4 +291,4 @@ End with_unqualified_modulo2. Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y. Proof. split; eauto using F_eqb_eq, F_eqb_complete. -Qed. +Qed. \ No newline at end of file diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v new file mode 100644 index 000000000..e3a1a6ad2 --- /dev/null +++ b/src/Experiments/EdDSARefinement.v @@ -0,0 +1,91 @@ +Require Import Crypto.Spec.EdDSA Bedrock.Word. +Require Import Coq.Classes.Morphisms. +Require Import Util.Decidable Util.Option Util.Tactics. + +Section EdDSA. + Context `{prm:EdDSA}. + Context {eq_dec:DecidableRel Eeq}. + Local Infix "==" := Eeq (at level 69, no associativity). + Local Notation valid := (@valid E Eeq Eadd EscalarMult b H l B Eenc Senc). + Local Infix "*" := EscalarMult. Local Infix "+" := Eadd. Local Infix "++" := combine. + Local Notation "P - Q" := (P + Eopp Q). + + Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}. + Context {Proper_Eopp : Proper (Eeq==>Eeq) Eopp}. + Context {Proper_Eadd : Proper (Eeq==>Eeq==>Eeq) Eadd}. + Context {Proper_EscalarMult : Proper (Logic.eq==>Eeq==>Eeq) EscalarMult}. + + Context {decE:word b-> option E}. + Context {decS:word b-> option nat}. + + Context {decE_canonical: forall x s, decE x = Some s -> x = Eenc s }. + Context {decS_canonical: forall x s, decS x = Some s -> x = Senc s }. + + Context {decS_Senc: forall x, decS (Senc x) = Some x}. + Context {decE_Eenc: forall x, decE (Eenc x) = Some x}. (* FIXME: equivalence relation *) + + Lemma solve_for_R : forall s B R n A, s * B == R + n * A <-> R == s*B - n*A. + Proof. + intros; split; + intro Heq; rewrite Heq; clear Heq. + Admitted. + + Definition verify {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool := + option_rect (fun _ => bool) (fun S : nat => + option_rect (fun _ => bool) (fun A : E => + weqb + (split1 b b sig) + (Eenc (S * B - PeanoNat.Nat.modulo (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ pk ++ message))) l * A)) + ) false (decE pk) + ) false (decS (split2 b b sig)) + . + + Lemma verify_correct mlen (message:word mlen) (pk:word b) (sig:word (b+b)) : + verify message pk sig = true <-> valid message pk sig. + Proof. + cbv [verify option_rect option_map]. + split. + { + repeat match goal with + | |- false = true -> _ => let H:=fresh "H" in intro H; discriminate H + | [H: _ |- _ ] => apply decS_canonical in H + | [H: _ |- _ ] => apply decE_canonical in H + | _ => rewrite weqb_true_iff + | _ => break_match + end. + intro. + subst. + rewrite <-combine_split. + rewrite Heqo. + rewrite H0. + constructor. + rewrite <-H0. + rewrite solve_for_R. + reflexivity. + } + { + intros [? ? ? ? Hvalid]. + rewrite solve_for_R in Hvalid. + rewrite split1_combine. + rewrite split2_combine. + rewrite decS_Senc. + rewrite decE_Eenc. + rewrite weqb_true_iff. + f_equiv. exact Hvalid. + } + Qed. + + Lemma scalarMult_mod_order : forall l x B, l * B == Ezero -> (Nat.modulo x l) * B == x * B. Admitted. + + Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M). + Proof. + cbv [sign public]. + intros. subst. constructor. + Local Arguments H {_} _. + Local Notation "'$' x" := (wordToNat x) (at level 1). + Local Infix "mod" := Nat.modulo (at level 50). + set (HRAM := H (Eenc ($ (H (prngKey sk ++ M)) * B) ++ Eenc (curveKey sk * B) ++ M)). + set (r := H (prngKey sk ++ M)). + repeat rewrite scalarMult_mod_order by eapply EdDSA_l_order_B. + Admitted. +End EdDSA. \ No newline at end of file diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v index 4e30313d9..659a0ec66 100644 --- a/src/Experiments/SpecEd25519.v +++ b/src/Experiments/SpecEd25519.v @@ -149,11 +149,11 @@ Local Infix "*" := (E.mul(H0:=curve25519params)). Axiom H : forall n : nat, word n -> word (b + b). Axiom B : point. (* TODO: B = decodePoint (y=4/5, x="positive") *) Axiom B_nonzero : B <> zero. -Axiom l_order_B : l * B = zero. -Axiom point_encoding : canonical encoding of point as word b. -Axiom scalar_encoding : canonical encoding of {n : nat | n < l} as word b. +Axiom l_order_B : E.eq (l * B) zero. +Axiom Eenc : point -> word b. +Axiom Senc : nat -> word b. -Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B point_encoding scalar_encoding := +Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B Eenc Senc := { EdDSA_c_valid := c_valid; EdDSA_n_ge_c := n_ge_c; -- cgit v1.2.3