From f1ef056a7a153931c7f05c126742d941d0908d25 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 25 Apr 2016 23:04:13 -0400 Subject: consolidate and rename Edwards curve lemmas --- src/Spec/EdDSA.v | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) (limited to 'src/Spec/EdDSA.v') diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 8a48f4dea..80aed4a20 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -22,7 +22,7 @@ Section EdDSAParams. b : nat; (* public keys are k bits, signatures are 2*k bits *) b_valid : 2^(b - 1) > BinInt.Z.to_nat q; FqEncoding : encoding of F q as Word.word (b-1); - PointEncoding : encoding of point as Word.word b; + PointEncoding : encoding of E.point as Word.word b; H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *) @@ -33,13 +33,13 @@ Section EdDSAParams. n_ge_c : n >= c; n_le_b : n <= b; - B : point; - B_not_identity : B <> zero; + B : E.point; + B_not_identity : B <> E.zero; l : nat; (* order of the subgroup of E generated by B *) l_prime : Znumtheory.prime (BinInt.Z.of_nat l); l_odd : l > 2; - l_order_B : (l*B)%E = zero; + l_order_B : (l*B)%E = E.zero; FlEncoding : encoding of F (BinInt.Z.of_nat l) as Word.word b }. End EdDSAParams. @@ -55,8 +55,7 @@ Section EdDSA. Notation secretkey := (Word.word b) (only parsing). Notation publickey := (Word.word b) (only parsing). Notation signature := (Word.word (b + b)) (only parsing). - Let point_eq_dec : forall P Q, {P = Q} + {P <> Q} := CompleteEdwardsCurveTheorems.point_eq_dec. - Local Infix "==" := point_eq_dec (at level 70) : E_scope . + Local Infix "==" := CompleteEdwardsCurveTheorems.E.point_eq_dec (at level 70) : E_scope . (* TODO: proofread curveKey and definition of n *) Definition curveKey (sk:secretkey) : nat := @@ -68,7 +67,7 @@ Section EdDSA. Definition sign (A_:publickey) sk {n} (M : Word.word n) := let r : nat := H (prngKey sk ++ M) in (* secret nonce *) - let R : point := (r * B)%E in (* commitment to nonce *) + let R : E.point := (r * B)%E in (* commitment to nonce *) let s : nat := curveKey sk in (* secret scalar *) let S : F (BinInt.Z.of_nat l) := ZToField (BinInt.Z.of_nat (r + H (enc R ++ public sk ++ M) * s)) in @@ -78,8 +77,8 @@ Section EdDSA. 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 A_ : option E.point with None => false | Some A => + match dec R_ : option E.point with None => false | Some R => if BinInt.Z.to_nat (FieldToZ S') * B == R + (H (R_ ++ A_ ++ M)) * A then true else false end -- cgit v1.2.3