diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-03-21 23:21:50 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-03-21 23:21:50 -0400 |
| commit | 3d75a97748a6ce76364324762b919d3e54a4cac3 (patch) | |
| tree | 39396b5e9714d4b06bdccaea6798584ba664d4e9 /src/Spec | |
| parent | 0f77ed606c8687e5cdcd72c85eefde609c5e0de1 (diff) | |
nicer verify() derivation starter
Diffstat (limited to 'src/Spec')
| -rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 5 | ||||
| -rw-r--r-- | src/Spec/EdDSA.v | 3 |
2 files changed, 5 insertions, 3 deletions
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 := { (* <https://eprint.iacr.org/2015/677.pdf> *) 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 |