search

adampetcher / fcf

Foundational Cryptography Framework for machine-checked proofs of cryptography.
Other
48 stars 23 forks source link

getSupport purpose #1

Closed eshreveUTD closed 8 years ago

eshreveUTD commented 8 years ago

I'm working on a class project to use FCF to prove some things about the Luby-Rackoff construction (basically section 6 from the following paper http://www.shoup.net/papers/games.pdf).

I'm not sure about the purpose of getSupport but I see that it is used in a lot of places. Can you provide a description?

Thanks!

Erik

adampetcher commented 8 years ago

getSupport is a function that computes the support of the supplied distribution, in the form of a list. The support is defined as the set of values that have positive probability. You should do a "SearchAbout getSupport" to see all the theory available for this function, and be aware of the simp_in_support tactic that draws helpful conclusions from hypotheses like "In x (getSupport ...)."

That proof shouldn't be much of a problem. You should be able to follow the PRF encryption example and do most of the same things. I don't think FCF currently has a working random function/permutation switching lemma (section 5.1 of the paper). There is something in FCF/RandPermSwitching.v, but it looks like it is out of date. There should be plenty of theory lying around for you to reconstruct it, though. For instance, FCF/HasDups.v contains a theorem on the probability of encountering duplicates in a list of random values. I would offer to fix it for you, but I worry that this lemma may be the most interesting part of your project, and I don't want to deprive you.

I'm happy to answer any more questions you have. You can find my papers on FCF at adam.petcher.net. Please use the contact info on that site to send me future questions. This will make it more convenient for me to answer. If you don't need my help, please stay in touch and let me know how it goes.