diff options
Diffstat (limited to 'src/Spec/EdDSA.v')
| -rw-r--r-- | src/Spec/EdDSA.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index c9660bd98..3decae6a7 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -74,9 +74,9 @@ Section EdDSA. 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 + 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 S_ : option (F (BinInt.Z.of_nat l)) with None => false | Some S' => if BinInt.Z.to_nat (FieldToZ S') * B == R + (H (R_ ++ A_ ++ M)) * A then true else false end |