[cryptolib] generalize PRF definitions, PRP<->PRF - #1028
Conversation
39abad4 to
2ca18f4
Compare
| (* FIXME: lift out and share with Strong RP RF *) | ||
| local lemma notin_supportIP (P : 'a -> bool) (d : 'a distr): | ||
| (exists a, support d a /\ !P a) <=> mu d P < mu d predT. | ||
| proof. | ||
| rewrite (mu_split _ predT P) /predI /predT /predC /=. | ||
| rewrite (exists_eq (fun a => support d a /\ !P a) (fun a => !P a /\ a \in d)) /=. | ||
| + by move=> a /=; rewrite andbC. | ||
| by rewrite -(witness_support (predC P)) -/(predC _) /#. | ||
| qed. | ||
|
|
||
| local lemma excepted_lossless (m:(D,D) fmap): | ||
| (exists x, x \notin m) => | ||
| mu (dD \ (rng m)) predT = 1%r. | ||
| proof. | ||
| move=> /endo_dom_rng [x h]; rewrite dexcepted_ll // 1:dD_ll. | ||
| by rewrite -dD_ll; apply: notin_supportIP; exists x; rewrite dD_fu. | ||
| qed. |
There was a problem hiding this comment.
Lift these out to a reasonable place. The first seems OK in distribution or in conditional. The second is specialised to endomaps... Perhaps sitting alongside the random permutation definition? (The lemma is key to proving losslessness.)
| @@ -130,447 +249,181 @@ qed. | |||
|
|
|||
| lemma excepted_lossless (m:(D,D) fmap): | |||
| (exists x, x \notin m) => | |||
| mu (uD \ (rng m)) predT = 1%r. | |||
| mu (dD \ (rng m)) predT = 1%r. | |||
| proof. | |||
| move=> /endo_dom_rng [x h]; rewrite dexcepted_ll //. | |||
| + smt(uD_uf_fu). | |||
| have [?[<- @/is_full Hsupp]]:= uD_uf_fu. | |||
| apply/notin_supportIP;exists x => />;apply Hsupp. | |||
| move=> /endo_dom_rng [x h]; rewrite dexcepted_ll // 1:dD_ll. | |||
| by rewrite -dD_ll; apply: notin_supportIP; exists x; rewrite dD_fu. | |||
| qed. | |||
| local lemma rng_set_subset_rngU1 (m : ('a, 'b) fmap) (x : 'a) y: | ||
| forall z, rng m.[x <- y] z => predU (rng m) (pred1 y) z. | ||
| proof. | ||
| proc; seq 1: (exists x, support uD x /\ !X x)=> //=. | ||
| + by rnd (predT); skip; smt(uD_uf_fu). | ||
| if=> //=. | ||
| + rnd (predT); skip. | ||
| move=> /> &0; rewrite dexceptedE predTI mu_not. | ||
| move=> x x_in_uD x_notin_X r_in_X. | ||
| apply/mulrV/ltr0_neq0/subr_gt0/notin_supportIP. | ||
| by exists x. | ||
| by hoare; rnd=> //=; skip=> &hr ->. | ||
| move=> z; rewrite /predU /pred1 /= (rngE m.[_ <- _])=> /= - [] x0. | ||
| rewrite get_setE; case: (x0 = x)=> |> _ m_x0; left; rewrite rngE /=. | ||
| by exists x0. | ||
| qed. | ||
|
|
||
| lemma PRPi'_Indirect_f_ll: islossless PRPi'(Indirect).f. | ||
| local lemma frng_set_subset_rngU1 (m : ('a, 'b) fmap) (x : 'a) y: | ||
| frng m.[x <- y] \subset frng m `|` fset1 y. | ||
| proof. | ||
| proc; if=> //=; auto; call Indirect_ll. | ||
| skip=> /> &hr x_notin_m. | ||
| have [x0] x0_notinr_m := endo_dom_rng PRPi.m{hr} _; first by exists x{hr}. | ||
| by exists x0; rewrite x0_notinr_m /=; smt(uD_uf_fu). | ||
| by move=> z; rewrite in_fsetU1 !mem_frng=> /rng_set_subset_rngU1. | ||
| qed. |
There was a problem hiding this comment.
These look like they could belong in FMap.
|
@ahuelsing and @mbbarbosa does this change (also to the PRP-PRF switching lemma and its weak version) look like it's going in the right direction, in terms of making the libraries more usable in a broader variety of contexts?
I think I should also generalise over the input type of the distinguisher. (Generalising over the distringuisher's output type then also requires generalising over the event, and that degrades usability again, I think.) Once the API is firmed up, I'll clear up any leftover internal gunk, add |
ahuelsing
left a comment
ahuelsing
left a comment
There was a problem hiding this comment.
I feel the definition is so cluttered that it is hard to read for a cryptographer... What about a comment in the beginning of the file pointing to the main defs and explaining the context?
| proc sample(X) = { | ||
| var r; | ||
|
|
||
| r <@ S.direct((), fun _=> X); |
There was a problem hiding this comment.
It comes from the clone, but it's only a proof artefact (it comes from a local clone inside a section, so it's kept in a separate namespace that becomes unreachable at section end).
I wasn't planning to document the proof, only the definitions and the main exported results, using Matthias's docgen.
| proc sample(X) = { | ||
| var r; | ||
|
|
||
| r <@ S.indirect((), fun _=> X); |
There was a problem hiding this comment.
Again, I did not see an S before
|
Making draft again: I want to document more. |
b1bf3e1 to
695f04d
Compare
|
This will break a lot of external proofs. I expect SHA2 to be particularly hard to adapt due to the intricacy of counting there. Overall, the fix should be a simplification (see the fix for MEE CBC) since this removes the need to change the behaviour of oracle's for adversaries that exceed their query quota. However, it doesn't eliminate the need to reason about the query count, simply pushing it to the point where the switching lemma is applied, rather than to the point where it is instantiated. (This is a slight oversimplification of where the difference lies, but the point is "a problem with the proof will be detected later than it was before, and it may be less clear that what causes breakage is the query counting.) In other words: I wouldn't be against a fix to the SHA3 proof that simply wraps this new library into a compatibility layer. |
This takes a swipe at cleaning up the PRF and PRP theories, as well as the associated switching lemmas. This should bring them more in line with modern EasyCrypt practice while also making them better examples of modern EasyCrypt development themselves—perhaps serving as advanced tutorials.
695f04d to
43e952f
Compare
2 participants
This generalises the definition of PRFs to not require keygen to sample from a distribution, and to not require a deterministic PRF. This (standard but relatively) specialist definition can be recovered when instantiating with a concrete PRF.
This is a breaking change.