From 3d75a97748a6ce76364324762b919d3e54a4cac3 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 21 Mar 2016 23:21:50 -0400 Subject: nicer verify() derivation starter --- src/Spec/CompleteEdwardsCurve.v | 5 ++++- src/Spec/EdDSA.v | 3 +-- 2 files changed, 5 insertions(+), 3 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 8dbfdf7b9..b7d2c0d8e 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -46,8 +46,11 @@ Section TwistedEdwardsCurves. | O => zero | S n' => unifiedAdd P (scalarMult n' P) end. + + Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}. End TwistedEdwardsCurves. Delimit Scope E_scope with E. Infix "+" := unifiedAdd : E_scope. -Infix "*" := scalarMult : E_scope. \ No newline at end of file +Infix "*" := scalarMult : E_scope. +Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope. diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 6f57d7bec..c9660bd98 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -14,6 +14,7 @@ Infix "mod" := NPeano.modulo. Infix "++" := Word.combine. Section EdDSAParams. + Class EdDSAParams := { (* *) E : TwistedEdwardsParams; (* underlying elliptic curve *) @@ -70,8 +71,6 @@ Section EdDSA. (r + H (enc R ++ public sk ++ M) * s)) in enc R ++ enc S. - Axiom point_eq_dec : forall P Q : point, {P = Q} + {P <> Q}. - Infix "==" := point_eq_dec (no associativity, at level 70) : E_scope. 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 -- cgit v1.2.3