diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/Ed25519.v | 61 | ||||
-rw-r--r-- | src/Experiments/Ed25519Extraction.v | 6 | ||||
-rw-r--r-- | src/Spec/MxDH.v | 18 | ||||
-rw-r--r-- | src/Test/Curve25519SpecTestVectors.v | 2 |
4 files changed, 74 insertions, 13 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 86c075e19..20208924d 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -2,6 +2,7 @@ Require Import Coq.omega.Omega. Require Import Coq.Lists.List. Import ListNotations. Require Import Crypto.EdDSARepChange. +Require Import Crypto.MxDHRepChange. Import MxDH. Require Import Crypto.Spec.Ed25519. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.ListUtil. @@ -879,6 +880,7 @@ Proof. apply dec_bool. vm_cast_no_check (eq_refl true). (* Time Qed. (* Finished transaction in 1646.167 secs (1645.753u,0.339s) (successful) *) *) +Admitted. Definition sign := @EdDSARepChange.sign E (@CompleteEdwardsCurveTheorems.E.eq Fq (@eq Fq) (@ModularArithmetic.F.one q) @@ -1478,5 +1480,60 @@ Let verify_correct : (* SRepDec := *) SRepDec (* SRepDec_correct := *) SRepDec_correct . -Let both_correct := (@sign_correct, @verify_correct). -Print Assumptions both_correct.
\ No newline at end of file + +Lemma Fhomom_inv_zero : + GF25519BoundedCommon.eq + (GF25519BoundedCommon.encode + (@ModularArithmetic.F.inv GF25519.modulus + (ModularArithmetic.F.of_Z GF25519.modulus 0))) + (GF25519Bounded.inv GF25519BoundedCommon.zero). +Proof. + vm_decide_no_check. +Qed. + +Import ModularArithmetic. +Module Spec. + Module X25519. + Definition a : F q := F.of_Z _ 486662. + Definition a24 : F q := ((a - F.of_Z _ 2) / F.of_Z _ 4)%F. + End X25519. +End Spec. + +Section X25519Constants. + Import GF25519BoundedCommon. + Definition a24' : GF25519BoundedCommon.fe25519 := + Eval vm_compute in GF25519BoundedCommon.encode Spec.X25519.a24. + Definition a24 : GF25519BoundedCommon.fe25519 := + Eval cbv [a24' fe25519_word64ize word64ize andb opt.word64ToZ opt.word64ize opt.Zleb Z.compare CompOpp Pos.compare Pos.compare_cont] in (fe25519_word64ize a24'). + Lemma a24_correct : GF25519BoundedCommon.eq + (GF25519BoundedCommon.encode Spec.X25519.a24) + (a24). + Proof. vm_decide_no_check. Qed. +End X25519Constants. + +Definition x25519 (n:N) (x:GF25519BoundedCommon.fe25519) : GF25519BoundedCommon.fe25519 := + @MxDH.montladder GF25519BoundedCommon.fe25519 GF25519BoundedCommon.zero + GF25519BoundedCommon.one GF25519Bounded.add GF25519Bounded.sub + GF25519Bounded.mul GF25519Bounded.inv a24 + (fun (H : bool) + (H0 + H1 : GF25519BoundedCommon.fe25519 * GF25519BoundedCommon.fe25519) + => if H then (H1, H0) else (H0, H1)) 255 (N.testbit_nat n) x. + +Definition x25519_correct' n x : + GF25519BoundedCommon.eq + (GF25519BoundedCommon.encode (MxDH.montladder 255 (N.testbit_nat n) x)) + (MxDH.montladder 255 (N.testbit_nat n) (GF25519BoundedCommon.encode x)) := + MxDHRepChange + (field:=PrimeFieldTheorems.F.field_modulo GF25519.modulus) + (impl_field:=GF25519Bounded.field25519) + (homomorphism_inv_zero:=Fhomom_inv_zero) + (homomorphism_a24:=a24_correct) + (Fcswap_correct:= fun _ _ _ => (reflexivity _)) + (Kcswap_correct:= fun _ _ _ => (reflexivity _)) + (tb2_correct:=fun _ => (reflexivity _)) + 255 _. + +Print Assumptions x25519_correct'. +Let three_correct := (@sign_correct, @verify_correct, x25519_correct'). +Print Assumptions three_correct.
\ No newline at end of file diff --git a/src/Experiments/Ed25519Extraction.v b/src/Experiments/Ed25519Extraction.v index 47cf4f791..20a76f17f 100644 --- a/src/Experiments/Ed25519Extraction.v +++ b/src/Experiments/Ed25519Extraction.v @@ -292,4 +292,8 @@ Extraction "src/Experiments/Ed25519_noimports.hs" Ed25519.sign (* Ed25519.verify True *Ed25519 Prelude> eRepEnc ((sRepERepMul l eRepB) `erepAdd` eRepB) == eRepEnc eRepB True -*)
\ No newline at end of file +*) + +Import Crypto.Spec.MxDH. +Extraction Inline MxDH.ladderstep MxDH.montladder. +Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519.
\ No newline at end of file diff --git a/src/Spec/MxDH.v b/src/Spec/MxDH.v index d637836e4..0829c46f7 100644 --- a/src/Spec/MxDH.v +++ b/src/Spec/MxDH.v @@ -44,7 +44,7 @@ Module MxDH. (* from RFC7748 *) ((X4, Z4), (X5, Z5)) end. - Context {S:Type} {testbit:S->nat->bool} {cswap:bool->F*F->F*F->(F*F)*(F*F)}. + Context {cswap:bool->F*F->F*F->(F*F)*(F*F)}. Fixpoint downto_iter (i:nat) : list nat := match i with @@ -59,22 +59,22 @@ Module MxDH. (* from RFC7748 *) (* Ideally, we would verify that this corresponds to x coordinate multiplication *) - Definition montladder bound (s:S) (u:F) := - let '(_, _, P1, P2, swap) := + Definition montladder bound (testbit:nat->bool) (u:F) := + let '(P1, P2, swap) := downto - (s, u, (1, 0), (u, 1), false) + ((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 '(P1, P2, swap) := state in + let s_i := testbit 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) + let '(P1, P2) := ladderstep u P1 P2 in + (P1, P2, swap) ) in let '((x, z), _) := cswap swap P1 P2 in - x/z. + x * Finv z. End MontgomeryLadderKeyExchange. End MxDH. diff --git a/src/Test/Curve25519SpecTestVectors.v b/src/Test/Curve25519SpecTestVectors.v index 511998d48..15ca468c1 100644 --- a/src/Test/Curve25519SpecTestVectors.v +++ b/src/Test/Curve25519SpecTestVectors.v @@ -6,7 +6,7 @@ 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. +Definition monty s : F -> F := @MxDH.montladder F F.zero F.one F.add F.sub F.mul F.inv a24 cswap 255 (BinNat.N.testbit_nat s). Example one_basepoint : F.to_Z (monty 1 (F.of_Z _ 9)) = 9%Z. Proof. vm_decide_no_check. Qed. |