diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-06-27 18:22:37 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-06-27 18:22:37 -0400 |
commit | b3d0b26ee3f97b1afade0880540d6d87e0cef03f (patch) | |
tree | 2bbcf725916c2d3d4029ffb194ff3bd8b62cfb36 /src/Experiments | |
parent | 1459a1487e20f0173dd457b15b236a153c083b8c (diff) |
eddsa refinement setup
Diffstat (limited to 'src/Experiments')
-rw-r--r-- | src/Experiments/EdDSARefinement.v | 38 |
1 files changed, 37 insertions, 1 deletions
diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v index cf9083061..c8de64895 100644 --- a/src/Experiments/EdDSARefinement.v +++ b/src/Experiments/EdDSARefinement.v @@ -16,6 +16,7 @@ Section EdDSA. Local Notation valid := (@valid E Eeq Eadd EscalarMult b H l B Eenc Senc). Local Infix "*" := EscalarMult. Local Infix "+" := Eadd. Local Infix "++" := combine. Local Notation "P - Q" := (P + Eopp Q). + Local Arguments H {_} _. Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}. Context {Proper_Eopp : Proper (Eeq==>Eeq) Eopp}. @@ -43,7 +44,7 @@ Section EdDSA. option_rect (fun _ => bool) (fun A : E => weqb (split1 b b sig) - (Eenc (S * B - (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ pk ++ message))) mod l * A)) + (Eenc (S * B - (wordToNat (H (split1 b b sig ++ pk ++ message))) mod l * A)) ) false (decE pk) ) false (decS (split2 b b sig)) . @@ -93,4 +94,39 @@ Section EdDSA. | rewrite scalarmult_assoc, mult_comm, <-scalarmult_assoc, EdDSA_l_order_B, scalarmult_zero_r; reflexivity ]. Qed. + + Section ChangeRep. + Context {A Aeq Aadd Aid Aopp} {Agroup:@group A Aeq Aadd Aid Aopp}. + Context {EtoA} {Ahomom:@is_homomorphism E Eeq Eadd A Aeq Aadd EtoA}. + + Context {Aenc : A -> word b} {Proper_Aenc:Proper (Aeq==>Logic.eq) Aenc} + {Aenc_correct : forall P:E, Eenc P = Aenc (EtoA P)}. + + Context {S Seq} `{@Equivalence S Seq} {natToS:nat->S} + {SAmul:S->A->A} {Proper_SAmul: Proper (Seq==>Aeq==>Aeq) SAmul} + {SAmul_correct: forall n P, Aeq (EtoA (n*P)) (SAmul (natToS n) (EtoA P))} + {SdecS} {SdecS_correct : forall w, (decS w) = (SdecS w)} (* FIXME: equivalence relation *) + {natToS_modl : forall n, Seq (natToS (n mod l)) (natToS n)}. + + Create HintDb hintsEtoA discriminated. + Hint Rewrite + Aenc_correct + homomorphism + homomorphism_id + homomorphism_inv + SAmul_correct + SdecS_correct + natToS_modl + : hintsEtoA. + + Definition verify_using_representation + {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) + : { answer | answer = verify message pk sig }. + Proof. + eexists. + cbv [verify]. + (rewrite_strat topdown hints hintsEtoA). + reflexivity. + Defined. + End ChangeRep. End EdDSA. |