From e93ec9a4112d2a6f78deb8fca10c5bd5c4b3c1cb Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Fri, 26 Apr 2019 16:28:19 -0400 Subject: Remove EdDSA Remove Spec/EdDSA.v and its reverse dependencies Spec/Ed25519.v and Primitives/EdDSARepChange.v. This code is no longer in use. --- _CoqProject | 3 - src/Primitives/EdDSARepChange.v | 267 ---------------------------------------- src/Spec/Ed25519.v | 91 -------------- src/Spec/EdDSA.v | 82 ------------ 4 files changed, 443 deletions(-) delete mode 100644 src/Primitives/EdDSARepChange.v delete mode 100644 src/Spec/Ed25519.v delete mode 100644 src/Spec/EdDSA.v diff --git a/_CoqProject b/_CoqProject index 8859f08ed..f8e005119 100644 --- a/_CoqProject +++ b/_CoqProject @@ -96,7 +96,6 @@ src/Fancy/Compiler.v src/Fancy/Montgomery256.v src/Fancy/Prod.v src/Fancy/Spec.v -src/Primitives/EdDSARepChange.v src/Primitives/MxDHRepChange.v src/PushButtonSynthesis/BarrettReduction.v src/PushButtonSynthesis/BarrettReductionReificationCache.v @@ -120,8 +119,6 @@ src/Rewriter/StripLiteralCasts.v src/Rewriter/ToFancy.v src/Rewriter/ToFancyWithCasts.v src/Spec/CompleteEdwardsCurve.v -src/Spec/Ed25519.v -src/Spec/EdDSA.v src/Spec/ModularArithmetic.v src/Spec/MontgomeryCurve.v src/Spec/MxDH.v diff --git a/src/Primitives/EdDSARepChange.v b/src/Primitives/EdDSARepChange.v deleted file mode 100644 index b7f4acd9b..000000000 --- a/src/Primitives/EdDSARepChange.v +++ /dev/null @@ -1,267 +0,0 @@ -Require Import Crypto.Util.FixCoqMistakes. -Require Import Crypto.Spec.EdDSA bbv.WordScope. -Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions. -Require Import Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.ScalarMult. -Require Import Crypto.Util.Decidable Crypto.Util.Option. -Require Import Crypto.Util.Tactics.SetEvars. -Require Import Crypto.Util.Tactics.SubstEvars. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Coq.omega.Omega. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil Util.LetIn Util.NatUtil. -Require Import Crypto.Spec.ModularArithmetic Crypto.Arithmetic.PrimeFieldTheorems. -Import NPeano. - -Import Notations. - -Section EdDSA. - Context `{prm:EdDSA}. - Local Infix "==" := Eeq. Local Infix "+" := Eadd. Local Infix "*" := ZEmul. - - Local Notation valid := (@valid E Eeq Eadd ZEmul b H l B Eenc Senc). - Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M). - Proof using Type. - cbv [sign public Spec.EdDSA.valid]; intros; subst; - repeat match goal with - | |- exists _, _ => eexists - | |- _ /\ _ => eapply conj - | |- _ => reflexivity - end. - rewrite F.to_Z_of_Z, scalarmult_mod_order, scalarmult_add_l, cancel_left, scalarmult_mod_order, Z.mul_comm, scalarmult_assoc; - try solve [ reflexivity - | setoid_rewrite (*unify 0*) (Z2Nat.inj_iff _ 0); pose proof EdDSA_l_odd; omega - | pose proof EdDSA_l_odd; omega - | apply EdDSA_l_order_B - | rewrite scalarmult_assoc, Z.mul_comm, <-scalarmult_assoc, - EdDSA_l_order_B, scalarmult_zero_r; reflexivity]. - Qed. - - Lemma solve_for_R_sig : forall s B R n A, { solution | s * B == R + n * A <-> R == solution }. - Proof. - eexists. - set_evars. - setoid_rewrite <-(symmetry_iff(R:=Eeq)) at 1. - setoid_rewrite <-eq_r_opp_r_inv. - setoid_rewrite <-scalarmult_opp_r. - subst_evars. - reflexivity. - Defined. - Definition solve_for_R := Eval cbv [proj2_sig solve_for_R_sig] in (fun s B R n A => proj2_sig (solve_for_R_sig s B R n A)). - - Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}. - Global Instance Proper_eq_Eenc ref : Proper (Eeq ==> iff) (fun P => Eenc P = ref). - Proof using Proper_Eenc. intros ? ? Hx; rewrite Hx; reflexivity. Qed. - - Context {Edec:word b-> option E} {eq_enc_E_iff: forall P_ P, Eenc P = P_ <-> option_eq Eeq (Edec P_) (Some P)}. - Context {Sdec:word b-> option (F l)} {eq_enc_S_iff: forall n_ n, Senc n = n_ <-> Sdec n_ = Some n}. - - Local Infix "++" := Word.combine. - Definition verify'_sig : { verify | forall mlen (message:word mlen) (pk:word b) (sig:word (b+b)), - verify mlen message pk sig = true <-> valid message pk sig }. - Proof. - eexists; intros mlen message pk sig; set_evars. - unfold Spec.EdDSA.valid. - setoid_rewrite solve_for_R. - setoid_rewrite combine_eq_iff. - setoid_rewrite and_comm at 4. setoid_rewrite and_assoc. repeat setoid_rewrite exists_and_indep_l. - setoid_rewrite (and_rewrite_l Eenc (split1 b b sig) - (fun x y => x == _ * B + Z.of_nat (wordToNat (H _ (y ++ Eenc _ ++ message))) mod _ * Eopp _)); setoid_rewrite eq_enc_S_iff. - setoid_rewrite (@exists_and_equiv_r _ _ _ _ _ _). - setoid_rewrite <- (fun A => and_rewriteleft_l (fun x => x) (Eenc A) (fun pk EencA => exists a, - Sdec (split2 b b sig) = Some a /\ - Eenc (_ * B + Z.of_nat (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ EencA ++ message))) mod _ * Eopp A) - = split1 b b sig)). setoid_rewrite (eq_enc_E_iff pk). - setoid_rewrite <-weqb_true_iff. - setoid_rewrite <-option_rect_false_returns_true_iff_eq. - rewrite <-option_rect_false_returns_true_iff by - (intros ? ? Hxy; unfold option_rect; break_match; rewrite <-?Hxy; reflexivity). - - subst_evars. - eapply reflexivity. - Defined. - Definition verify' {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool := - Eval cbv [proj1_sig verify'_sig] in proj1_sig verify'_sig mlen message pk sig. - Lemma verify'_correct : forall {mlen} (message:word mlen) pk sig, - verify' message pk sig = true <-> valid message pk sig. - Proof using Type*. exact (proj2_sig verify'_sig). Qed. - - Section ChangeRep. - Context {Erep ErepEq ErepAdd ErepId ErepOpp} {Agroup:@Algebra.Hierarchy.group Erep ErepEq ErepAdd ErepId ErepOpp}. - Context {EToRep} {Ahomom:@is_homomorphism E Eeq Eadd Erep ErepEq ErepAdd EToRep}. - - Context {ERepEnc : Erep -> word b} - {ERepEnc_correct : forall P:E, Eenc P = ERepEnc (EToRep P)} - {Proper_ERepEnc:Proper (ErepEq==>Logic.eq) ERepEnc}. - - Context {ERepDec : word b -> option Erep} - {ERepDec_correct : forall w, option_eq ErepEq (ERepDec w) (option_map EToRep (Edec w)) }. - - Context {SRep SRepEq} `{@Equivalence SRep SRepEq} {S2Rep:F l->SRep}. - - Context {SRepDecModL} {SRepDecModL_correct: forall (w:word (b+b)), SRepEq (S2Rep (F.of_Z _ (Z.of_nat (wordToNat w)))) (SRepDecModL w)}. - - Context {SRepERepMul:SRep->Erep->Erep} - {SRepERepMul_correct:forall n P, ErepEq (EToRep ((n mod l)*P)) (SRepERepMul (S2Rep (F.of_Z _ n)) (EToRep P))} - {Proper_SRepERepMul: Proper (SRepEq==>ErepEq==>ErepEq) SRepERepMul}. - - Context {SRepDec: word b -> option SRep} - {SRepDec_correct : forall w, option_eq SRepEq (option_map S2Rep (Sdec w)) (SRepDec w)}. - - Definition verify_using_representation - {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) - : { answer | answer = verify' message pk sig }. - Proof. - eexists. - pose proof EdDSA_l_odd. - cbv [verify']. - - etransitivity. Focus 2. { - eapply Proper_option_rect_nd_changebody; [intro|reflexivity]. - eapply Proper_option_rect_nd_changebody; [intro|reflexivity]. - rewrite <-F.mod_to_Z by omega. - repeat ( - rewrite ERepEnc_correct - || rewrite homomorphism - || rewrite homomorphism_id - || rewrite (homomorphism_inv(INV:=Eopp)(inv:=ErepOpp)(eq:=ErepEq)(phi:=EToRep)) - || rewrite SRepERepMul_correct - || rewrite SdecS_correct - || rewrite SRepDecModL_correct - || rewrite (@F.of_Z_to_Z _ _) - || rewrite (@F.mod_to_Z _ _) - ). - reflexivity. - } Unfocus. - - (* lazymatch goal with |- _ _ (option_rect _ ?some _ _) => idtac some end. *) - setoid_rewrite (option_rect_option_map EToRep - (fun s => - option_rect (fun _ : option _ => bool) - (fun s0 => - weqb - (ERepEnc - (ErepAdd (SRepERepMul (_ s0) (EToRep B)) - (SRepERepMul - (SRepDecModL - (H _ (split1 b b sig ++ pk ++ message))) - (ErepOpp (s))))) (split1 b b sig)) false - (Sdec (split2 b b sig))) - false). - (* rewrite with a complicated proper instance for inline code .. *) - etransitivity; - [| eapply Proper_option_rect_nd_changevalue; - [ - | reflexivity - | eapply ERepDec_correct - ]; - [ repeat match goal with - | |- _ => intro - | |- _ => eapply Proper_option_rect_nd_changebody - | |- ?R ?x ?x => reflexivity - | H : _ |- _ => rewrite H; reflexivity - end - ] - ]. - - etransitivity. Focus 2. { - eapply Proper_option_rect_nd_changebody; [intro|reflexivity]. - set_evars. - setoid_rewrite (option_rect_option_map S2Rep - (fun s0 => - weqb - (ERepEnc - (ErepAdd (SRepERepMul (s0) (EToRep B)) - (SRepERepMul - (SRepDecModL (H _ (split1 b b sig ++ pk ++ message))) - (ErepOpp _)))) (split1 b b sig)) - - false). - subst_evars. - - eapply Proper_option_rect_nd_changevalue; - [repeat intro; repeat f_equiv; eassumption|reflexivity|..]. - - symmetry. - eapply SRepDec_correct. - } Unfocus. - - reflexivity. - Defined. - - Definition verify {mlen} (msg:word mlen) pk sig := - Eval cbv beta iota delta [proj1_sig verify_using_representation] in - proj1_sig (verify_using_representation msg pk sig). - Lemma verify_correct {mlen} (msg:word mlen) pk sig : verify msg pk sig = true <-> valid msg pk sig. - Proof using Type*. - etransitivity; [|eapply (verify'_correct msg pk sig)]. - eapply iff_R_R_same_r, (proj2_sig (verify_using_representation _ _ _)). - Qed. - - Context {SRepEnc : SRep -> word b} - {SRepEnc_correct : forall x, Senc x = SRepEnc (S2Rep x)} - {Proper_SRepEnc:Proper (SRepEq==>Logic.eq) SRepEnc}. - Context {SRepAdd : SRep -> SRep -> SRep} - {SRepAdd_correct : forall x y, SRepEq (S2Rep (x+y)%F) (SRepAdd (S2Rep x) (S2Rep y)) } - {Proper_SRepAdd:Proper (SRepEq==>SRepEq==>SRepEq) SRepAdd}. - Context {SRepMul : SRep -> SRep -> SRep} - {SRepMul_correct : forall x y, SRepEq (S2Rep (x*y)%F) (SRepMul (S2Rep x) (S2Rep y)) } - {Proper_SRepMul:Proper (SRepEq==>SRepEq==>SRepEq) SRepMul}. - Context {ErepB:Erep} {ErepB_correct:ErepEq ErepB (EToRep B)}. - - Context {SRepDecModLShort} {SRepDecModLShort_correct: forall (w:word (n+1)), SRepEq (S2Rep (F.of_nat _ (wordToNat w))) (SRepDecModLShort w)}. - - (* We would ideally derive the optimized implementations from - specifications using `setoid_rewrite`, but doing this without - inlining let-bound subexpressions turned out to be quite messy in - the current state of Coq: *) - - Let n_le_bpb : (n <= b+b)%nat. destruct prm. omega. Qed. - - (* TODO: change impl to basesystem *) - Context (splitSecretPrngCurve : forall (sk:word b), SRep * word b). - Context (splitSecretPrngCurve_correct : forall sk, - let (s, r) := splitSecretPrngCurve sk in - SRepEq s (S2Rep (F.of_Z l (curveKey sk))) /\ r = prngKey (H:=H) sk). - - Definition sign (pk sk : word b) {mlen} (msg:word mlen) := - dlet sp := splitSecretPrngCurve sk in - dlet s := fst sp in - dlet p := snd sp in - dlet r := SRepDecModL (H _ (p ++ msg)) in - dlet R := SRepERepMul r ErepB in - dlet S := SRepAdd r (SRepMul (SRepDecModL (H _ (ERepEnc R ++ pk ++ msg))) s) in - ERepEnc R ++ SRepEnc S. - - Lemma Z_l_nonzero : Z.pos l <> 0%Z. discriminate. Qed. - - Lemma sign_correct (pk sk : word b) {mlen} (msg:word mlen) - : sign pk sk msg = EdDSA.sign pk sk msg. - Proof using Agroup Ahomom ERepEnc_correct ErepB_correct H0 Proper_ERepEnc Proper_SRepAdd Proper_SRepERepMul Proper_SRepEnc Proper_SRepMul SRepAdd_correct SRepDecModLShort_correct SRepDecModL_correct SRepERepMul_correct SRepEnc_correct SRepMul_correct splitSecretPrngCurve_correct. - cbv [sign EdDSA.sign Let_In]. - - let H := fresh "H" in - pose proof (splitSecretPrngCurve_correct sk) as H; - destruct (splitSecretPrngCurve sk); - destruct H as [curveKey_correct prngKey_correct]. - - repeat ( - reflexivity - || rewrite ERepEnc_correct - || rewrite SRepEnc_correct - || rewrite SRepDecModL_correct - || rewrite SRepERepMul_correct - || rewrite (F.of_Z_add (m:=l)) - || rewrite (F.of_Z_mul (m:=l)) - || rewrite SRepAdd_correct - || rewrite SRepMul_correct - || rewrite ErepB_correct - || rewrite <-prngKey_correct - || rewrite <-curveKey_correct - || eapply (f_equal2 (fun a b => a ++ b)) - || f_equiv - || rewrite <-(scalarmult_mod_order l B Z_l_nonzero EdDSA_l_order_B), SRepERepMul_correct - ). - Qed. - End ChangeRep. -End EdDSA. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v deleted file mode 100644 index e0fba6e23..000000000 --- a/src/Spec/Ed25519.v +++ /dev/null @@ -1,91 +0,0 @@ -Require Import Crypto.Spec.ModularArithmetic. -Require Import Coq.PArith.BinPosDef. -Require Import Coq.ZArith.BinIntDef. -Require Import Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Spec.EdDSA. - -Require Crypto.Arithmetic.PrimeFieldTheorems. (* to know that Z mod p is a field *) -Require Crypto.Curves.Edwards.AffineProofs. - -(* these 2 proofs can be generated using https://github.com/andres-erbsen/safecurves-primes *) -Axiom prime_q : Znumtheory.prime (2^255-19). Global Existing Instance prime_q. -Axiom prime_l : Znumtheory.prime (2^252 + 27742317777372353535851937790883648493). Global Existing Instance prime_l. - -Section Ed25519. - - Local Open Scope Z_scope. - - Definition q : BinPos.positive := 2^255 - 19. - Definition Fq : Type := F q. - - Definition l : BinPos.positive := 2^252 + 27742317777372353535851937790883648493. - Definition Fl : Type := F l. - - Local Open Scope F_scope. - - Definition a : Fq := F.opp 1. - Definition d : Fq := F.opp (F.of_Z _ 121665) / (F.of_Z _ 121666). - - Local Open Scope nat_scope. - - Definition b : nat := 256. - Definition n : nat := b - 2. - Definition c : nat := 3. - - Context {SHA512: forall n : nat, Word.word n -> Word.word 512}. - - Local Instance char_gt_e : - @Ring.char_ge (@F q) eq F.zero F.one F.opp F.add F.sub F.mul - (BinNat.N.succ_pos BinNat.N.two). - Proof. eapply Hierarchy.char_ge_weaken; - [apply (_:Ring.char_ge q)|Decidable.vm_decide]. Qed. - - - Definition E : Type := E.point - (F:=Fq) (Feq:=Logic.eq) (Fone:=F.one) (Fadd:=F.add) (Fmul:=F.mul) - (a:=a) (d:=d). - - Local Obligation Tactic := Decidable.vm_decide. (* to prove that B is on curve *) - - Program Definition B : E := - (F.of_Z q 15112221349535400772501151409588531511454012693041857206046113283949847762202, - F.of_Z q 4 / F.of_Z q 5). - - Local Infix "++" := Word.combine. - Local Notation bit b := (Word.WS b Word.WO : Word.word 1). - - Definition Fencode {len} {m} : F m -> Word.word len := - fun x : F m => (Word.NToWord _ (BinIntDef.Z.to_N (F.to_Z x))). - Definition sign (x : F q) : bool := BinIntDef.Z.testbit (F.to_Z x) 0. - Definition Eenc : E -> Word.word b := fun P => - let '(x,y) := E.coordinates P in Fencode (len:=b-1) y ++ bit (sign x). - Definition Senc : Fl -> Word.word b := Fencode (len:=b). - - Lemma nonzero_a : a <> 0%F. - Proof using Type. Crypto.Util.Decidable.vm_decide. Qed. - Lemma square_a : exists sqrt_a : Fq, (sqrt_a * sqrt_a)%F = a. - Proof using Type. pose (@PrimeFieldTheorems.F.Decidable_square q _ ltac:(Crypto.Util.Decidable.vm_decide) a); Crypto.Util.Decidable.vm_decide. Qed. - Lemma nonsquare_d : forall x : Fq, (x * x)%F <> d. - Proof using Type. pose (@PrimeFieldTheorems.F.Decidable_square q _ ltac:(Crypto.Util.Decidable.vm_decide) d); Crypto.Util.Decidable.vm_decide. Qed. - - Let add := E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d). - Let zero := E.zero(nonzero_a:=nonzero_a)(d:=d). - (* TODO: move scalarmult_ref to Spec? *) - Let mul := ScalarMult.scalarmult_ref(zero:=zero)(add:=add)(opp:=AffineProofs.E.opp(nonzero_a:=nonzero_a)). - - Definition ed25519 (l_order_B: (mul l B = zero)%E) : - EdDSA (E:=E) (Eadd:=add) (Ezero:=zero) (ZEmul:=mul) (B:=B) - (Eopp:=Crypto.Curves.Edwards.AffineProofs.E.opp(nonzero_a:=nonzero_a)) (* TODO: move defn *) - (Eeq:=E.eq) (* TODO: move defn *) - (l:=l) (b:=b) (n:=n) (c:=c) - (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512). - Proof using Type. - split; try exact _. - Crypto.Util.Decidable.vm_decide. - Crypto.Util.Decidable.vm_decide. - Crypto.Util.Decidable.vm_decide. - Crypto.Util.Decidable.vm_decide. - Crypto.Util.Decidable.vm_decide. - exact l_order_B. - Qed. -End Ed25519. diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v deleted file mode 100644 index 268925167..000000000 --- a/src/Spec/EdDSA.v +++ /dev/null @@ -1,82 +0,0 @@ -Require bbv.WordScope Crypto.Util.WordUtil. -Require Import Coq.ZArith.BinIntDef. -Require Crypto.Algebra.Hierarchy Algebra.ScalarMult. -Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt. -Require Coq.Numbers.Natural.Peano.NPeano. - -Require Import Crypto.Spec.ModularArithmetic. - -Local Infix "-" := BinInt.Z.sub. -Local Infix "^" := BinInt.Z.pow. -Local Infix "mod" := BinInt.Z.modulo. -Local Infix "++" := Word.combine. -Local Notation setbit := BinInt.Z.setbit. - -Section EdDSA. - Class EdDSA (* *) - {E Eeq Eadd Ezero Eopp} {ZEmul} (* the underllying elliptic curve operations *) - - {b : nat} (* public keys are k bits, signatures are 2*k bits *) - {H : forall {n}, Word.word n -> Word.word (b + b)} (* main hash function *) - {c : nat} (* cofactor E = 2^c *) - {n : nat} (* secret keys are (n+1) bits *) - {l : BinPos.positive} (* order of the subgroup of E generated by B *) - - {B : E} (* base point *) - - {Eenc : E -> Word.word b} (* normative encoding of elliptic cuve points *) - {Senc : F l -> Word.word b} (* normative encoding of scalars *) - := - { - EdDSA_group:@Algebra.Hierarchy.group E Eeq Eadd Ezero Eopp; - EdDSA_scalarmult:@Algebra.ScalarMult.is_scalarmult E Eeq Eadd Ezero Eopp ZEmul; - - EdDSA_c_valid : c = 2 \/ c = 3; - - EdDSA_n_ge_c : n >= c; - EdDSA_n_le_b : n <= b; - - EdDSA_B_not_identity : not (Eeq B Ezero); - - EdDSA_l_prime : Znumtheory.prime l; - EdDSA_l_odd : BinInt.Z.lt 2 l; - EdDSA_l_order_B : Eeq (ZEmul l B) Ezero - }. - Global Existing Instance EdDSA_group. - Global Existing Instance EdDSA_scalarmult. - - Context `{prm:EdDSA}. - - Local Coercion Word.wordToNat : Word.word >-> nat. - Local Coercion BinInt.Z.of_nat : nat >-> BinInt.Z. - Local Notation secretkey := (Word.word b) (only parsing). - Local Notation publickey := (Word.word b) (only parsing). - Local Notation signature := (Word.word (b + b)) (only parsing). - - Local Arguments H {n} _. - Local Notation wfirstn n w := (@WordUtil.wfirstn n _ w _) (only parsing). - - Local Obligation Tactic := destruct prm; simpl; intros; Omega.omega. - - Program Definition curveKey (sk:secretkey) : BinInt.Z := - let x := wfirstn n (H sk) in (* hash the key, use first "half" for secret scalar *) - let x := x - (x mod (2^c)) in (* it is implicitly 0 mod (2^c) *) - setbit x n. (* and the high bit is always set *) - - Local Infix "+" := Eadd. - Local Infix "*" := ZEmul. - - Definition prngKey (sk:secretkey) : Word.word b := Word.split2 b b (H sk). - Definition public (sk:secretkey) : publickey := Eenc (curveKey sk*B). - - Program Definition sign (A_:publickey) sk {n} (M : Word.word n) := - let r := H (prngKey sk ++ M) in (* secret nonce *) - let R := r * B in (* commitment to nonce *) - let s := curveKey sk in (* secret scalar *) - let S := F.of_Z l (r + H (Eenc R ++ A_ ++ M) * s) in - Eenc R ++ Senc S. - - Definition valid {n} (message : Word.word n) pubkey signature := - exists A S R, Eenc A = pubkey /\ Eenc R ++ Senc S = signature /\ - Eeq (F.to_Z S * B) (R + (H (Eenc R ++ Eenc A ++ message) mod l) * A). -End EdDSA. -- cgit v1.2.3