diff options
-rw-r--r-- | _CoqProject | 2 | ||||
-rw-r--r-- | src/Spec/MxDH.v | 81 | ||||
-rw-r--r-- | src/Test/Curve25519SpecTestVectors.v | 22 |
3 files changed, 105 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 06764f53c..d732d0b40 100644 --- a/_CoqProject +++ b/_CoqProject @@ -84,6 +84,7 @@ src/Spec/EdDSA.v src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v +src/Spec/MxDH.v src/Spec/WeierstrassCurve.v src/Specific/GF1305.v src/Specific/GF25519.v @@ -92,6 +93,7 @@ src/Specific/FancyMachine256/Core.v src/Specific/FancyMachine256/Montgomery.v src/Tactics/VerdiTactics.v src/Tactics/Algebra_syntax/Nsatz.v +src/Test/Curve25519SpecTestVectors.v src/Util/AdditionChainExponentiation.v src/Util/AutoRewrite.v src/Util/Bool.v diff --git a/src/Spec/MxDH.v b/src/Spec/MxDH.v new file mode 100644 index 000000000..512930fbc --- /dev/null +++ b/src/Spec/MxDH.v @@ -0,0 +1,81 @@ +Require Crypto.Algebra. + +Module MxDH. (* from RFC7748 *) + Section MontgomeryLadderKeyExchange. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq}. + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Infix "+" := Fadd. Local Infix "*" := Fmul. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. + Local Notation "x ^ 2" := (x*x) (at level 30). + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Notation "2" := (1+1). Local Notation "4" := (2+2). + + Context {a b: F}. (* parameters of the Montgomery curve *) + Context {nonsquare_aa_m4:~exists sqrt, sqrt^2 = a^2-4} {five_neq_zero:1+4<>0}. + + (* Implemention from RFC7748. Note that this differs from EFD and + Montgomery '87 in the choice of which precomputed constant to use + for [a] *) + (* Ideally we would want to verify that this correspons to + x-coordinate addition on the relevant elliptic curve, as + specified by addition formulas in Montgomery coordinates. + However, even if we did get to doing that, we still would not + want to change the type of the ladder function to talk about + points that are on the curve -- there are contexts where this + can be, carefully, used with values that are not verified to + be on the curve *) + Context {a24:F} {a24_correct:4*a24 = a-2}. + Definition ladderstep (X1:F) (P1 P2:F*F) : (F*F)*(F*F) := + match P1, P2 return _ with + (X2, Z2), (X3, Z3) => + let A := X2+Z2 in + let AA := A^2 in + let B := X2-Z2 in + let BB := B^2 in + let E := AA-BB in + let C := X3+Z3 in + let D := X3-Z3 in + let DA := D*A in + let CB := C*B in + let X5 := (DA+CB)^2 in + let Z5 := X1*(DA-CB)^2 in + let X4 := AA*BB in + let Z4 := E*(AA + a24*E) in + ((X4, Z4), (X5, Z5)) + end. + + Context {S:Type} {testbit:S->nat->bool} {cswap:bool->F*F->F*F->(F*F)*(F*F)}. + + Fixpoint downto_iter (i:nat) : list nat := + match i with + | Datatypes.S i' => i'::downto_iter i' + | O => nil + end. + + Definition downto {state} init count (step:state->nat->state) : state := + List.fold_left step (downto_iter count) init. + + Local Notation xor := Coq.Init.Datatypes.xorb. + + (* Ideally, we would verify that this corresponds to x coordinate + multiplication *) + Definition montladder bound (s:S) (u:F) := + let '(_, _, P1, P2, swap) := + downto + (s, u, (1, 0), (u, 1), false) + bound + (fun state i => + let '(s, x, P1, P2, swap) := state in + let s_i := testbit s i in + let swap := xor swap s_i in + let '(P1, P2) := cswap swap P1 P2 in + let swap := s_i in + let '(P1, P2) := ladderstep x P1 P2 in + (s, x, P1, P2, swap) + ) in + let '((x, z), _) := cswap swap P1 P2 in + x/z. + End MontgomeryLadderKeyExchange. +End MxDH. + +(* see [Test.Curve25519SpecTestVectors] for sanity-checks *)
\ No newline at end of file diff --git a/src/Test/Curve25519SpecTestVectors.v b/src/Test/Curve25519SpecTestVectors.v new file mode 100644 index 000000000..511998d48 --- /dev/null +++ b/src/Test/Curve25519SpecTestVectors.v @@ -0,0 +1,22 @@ +(* Test vectors from <https://tools.ietf.org/html/rfc7748#section-5.2>, + with hex values converted to decimal using python like this: + > int.from_bytes(binascii.unhexlify('deadbeef'), 'little') *) +Require Import Spec.ModularArithmetic Spec.MxDH Crypto.Util.Decidable. +Definition F := F (2^255 - 19). +Definition a : F := F.of_Z _ 486662. +Definition a24 : F := ((a - F.of_Z _ 2) / F.of_Z _ 4)%F. +Definition cswap {T} (swap:bool) (a b:T) := if swap then (b, a) else (a, b). +Definition monty : BinNums.N -> F -> F := @MxDH.montladder F F.zero F.one F.add F.sub F.mul F.div a24 BinNums.N BinNat.N.testbit_nat cswap 255. + +Example one_basepoint : F.to_Z (monty 1 (F.of_Z _ 9)) = 9%Z. +Proof. vm_decide_no_check. Qed. + +Example testvector_one : F.to_Z (monty + 31029842492115040904895560451863089656472772604678260265531221036453811406496%N + (F.of_Z _ 34426434033919594451155107781188821651316167215306631574996226621102155684838%Z)) = 37325765543539916631701301279660700968428932651319597985674090122993663859395%Z. +Proof. vm_decide_no_check. Qed. + +Example testvector_two : F.to_Z (monty + 35156891815674817266734212754503633747128614016119564763269015315466259359304%N + (F.of_Z _ 8883857351183929894090759386610649319417338800022198945255395922347792736741%Z)) = 39566196721700740701373067725336211924689549479508623342842086701180565506965%Z. +Proof. vm_decide_no_check. Qed.
\ No newline at end of file |