diff options
| -rw-r--r-- | _CoqProject | 2 | ||||
| -rw-r--r-- | src/Experiments/DerivationsOptionRectLetInEncoding.v | 59 | ||||
| -rw-r--r-- | src/Experiments/EdDSARefinement.v | 91 | ||||
| -rw-r--r-- | src/Experiments/SpecEd25519.v | 8 | ||||
| -rw-r--r-- | src/Spec/EdDSA.v | 23 | ||||
| -rw-r--r-- | src/Util/Option.v | 62 |
6 files changed, 171 insertions, 74 deletions
diff --git a/_CoqProject b/_CoqProject index afad38124..904d716b8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -29,6 +29,7 @@ src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v src/Experiments/DerivationsOptionRectLetInEncoding.v +src/Experiments/EdDSARefinement.v src/Experiments/GenericFieldPow.v src/Experiments/SpecEd25519.v src/ModularArithmetic/ExtendedBaseVector.v @@ -58,6 +59,7 @@ src/Util/ListUtil.v src/Util/NatUtil.v src/Util/Notations.v src/Util/NumTheoryUtil.v +src/Util/Option.v src/Util/Sum.v src/Util/Tactics.v src/Util/Tuple.v 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; diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index c28ff0482..7e4d3ed25 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -1,4 +1,3 @@ -Require Import Crypto.Spec.Encoding. Require Bedrock.Word Crypto.Util.WordUtil. Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt. Require Coq.Numbers.Natural.Peano.NPeano. @@ -33,8 +32,8 @@ Section EdDSA. {B : E} (* base point *) - {PointEncoding : canonical encoding of E as Word.word b} (* wire format *) - {FlEncoding : canonical encoding of { n | n < l } as Word.word b} + {Eenc : E -> Word.word b} (* normative encoding of elliptic cuve points *) + {Senc : nat -> Word.word b} (* normative encoding of scalars *) := { EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp; @@ -48,13 +47,13 @@ Section EdDSA. EdDSA_l_prime : Znumtheory.prime (BinInt.Z.of_nat l); EdDSA_l_odd : l > 2; - EdDSA_l_order_B : EscalarMult l B = Ezero + EdDSA_l_order_B : Eeq (EscalarMult l B) Ezero }. Global Existing Instance EdDSA_group. Context `{prm:EdDSA}. - Local Infix "=" := Eeq. + Local Infix "=" := Eeq : type_scope. Local Coercion Word.wordToNat : Word.word >-> nat. Local Notation secretkey := (Word.word b) (only parsing). Local Notation publickey := (Word.word b) (only parsing). @@ -75,18 +74,18 @@ Section EdDSA. Local Infix "*" := EscalarMult. Definition prngKey (sk:secretkey) : Word.word b := Word.split2 b b (H sk). - Definition public (sk:secretkey) : publickey := enc (curveKey sk*B). + Definition public (sk:secretkey) : publickey := Eenc (curveKey sk*B). Program Definition sign (A_:publickey) sk {n} (M : Word.word n) := let r : nat := H (prngKey sk ++ M) in (* secret nonce *) let R : E := r * B in (* commitment to nonce *) let s : nat := curveKey sk in (* secret scalar *) - let S : {n|n<l} := exist _ ((r + H (enc R ++ public sk ++ M) * s) mod l) _ in - enc R ++ enc S. + let S : nat := (r + H (Eenc R ++ A_ ++ M) * s) mod l in + Eenc R ++ Senc S. (* For a [n]-bit [message] from public key [A_], validity of a signature [R_ ++ S_] *) Inductive valid {n:nat} : Word.word n -> publickey -> signature -> Prop := - ValidityRule : forall (message:Word.word n) (A:E) (R:E) (S:nat) S_lt_l, - S * B = R + (H (enc R ++ enc A ++ message) mod l) * A - -> valid message (enc A) (enc R ++ enc (exist _ S S_lt_l)). -End EdDSA. + ValidityRule : forall (message:Word.word n) (A:E) (R:E) (S:nat), + S * B = R + (H (Eenc R ++ Eenc A ++ message) mod l) * A + -> valid message (Eenc A) (Eenc R ++ Senc S). +End EdDSA.
\ No newline at end of file diff --git a/src/Util/Option.v b/src/Util/Option.v new file mode 100644 index 000000000..db4b69dde --- /dev/null +++ b/src/Util/Option.v @@ -0,0 +1,62 @@ +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. + +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. + +(* +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 *) +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. + +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. |