Another Look at Provable Security
cacr.uwaterloo.ca
Another Look at Provable Security
1–10 of 22 posts
Re: Another Look at Provable Security
#2Very interesting. How does one get comfortable relying on cryptography that uses a method which lacks provable security? Simulating proof based on actual use?
Re: Another Look at Provable Security
#3Very interesting. How does one get comfortable relying on cryptography that uses a method which lacks provable security? Simulating proof based on actual use?
Two questions that I find myself asking:
1. Are proofs effective at judging the security of a protocol? For example many proofs rely on the random oracle model, yet the random oracle model is problematic. How can we construct convincing proofs?
2. Are there better measures of security? For example crypto-contests in which people try to break other peoples algorithms. Very little systems security relies on proofs (systems security is also almost always the weakest link).
My personal belief is: 1=yes, 2=maybe and it is worth it to develop alternative methods since they can be used in tandem with proofs.
Re: Another Look at Provable Security
#4This is what's known as "searching under the lamppost". Mathematicians would sometimes seek to prove only that which they suspect would be rather easy to prove, so they construct the problem in such a way that the perceived difficulty is exactly that which is easily provable, thereby solving the problem. They then shove everything else (that is hard to prove) under their assumptions (which are sometimes very well-hidden), and say the problem is now mathematically solved!
Figuring out whether the research is applicable in practice then becomes a game not of validating the proof, but of uncovering all the assumptions.
I see it in the PL community, too, where, rather than starting by analyzing where software bugs actually lie and how expensive each kind of bug turns out to be, and then see how most expensive bugs can be prevented, they start with a programming model which is very easy to prove, construct programs that are easily expressed by the model, and then claim they've found a provably bug-free way to program.
The question of how many real-world programs can be easily transformed into the model, at what costs, and whether it is the expensive bugs that are actually prevented by the proof or rather the trivial ones is left as an exercise to the reader.
Of course, I don't blame them. If you don't start with what you strongly suspect you'll be able to prove, you might not get any publishable results at all.
Re: Another Look at Provable Security
#5It's better to read the papers where they attempt provable security and then those published years later reviewing that work or those methods. Certain methods worked well, some failed over time, and so on. The lessons learned and looking back papers are where I find the most wisdom in this field. Naturally.
The papers on Orange Book-era B3 and A1 class systems along with the Common Criteria EAL6/EAL7 works taught me the most. They all required a clear, security policy and a strong argument the design/implementation embody it. The systems are modular, layered, internally simple, use structured programming style, use safer subsets of programming languages, often are state-machines, account for failure modes for everything, and trace each potential execution flow of the system. They also add, where possible, static analysis and covert channel analysis. Some did formal proofs but the above gets you 90-99% of the way.
So, the idea is that you design the system or algorithm in such a way that you can easily demonstrate it has certain properties. It was hard work. However, LOCK project even with proofs only cost around 30-40% extra on top of solid, development process. Another lesson is the specs, implementation, and proofs/arguments should always evolve side-by-side with plenty of communication between team members. This spots problems early. Analysis of various phases showed above methods caught all kinds of reliability and security flaws in actual systems with many doing excellent during years of pentesting. Proof themselves, on other hand, should only be used if the property is easy to model mathematically. Otherwise, you use a lot of effort with little gained. Final lesson came from TCB concept: focus all your provable security on mechanisms that are flexible and simple so the cost is spread over all projects benefiting from it. Security & separation kernels did this to a degree but I think CompCert compiler is best, modern example of ROI on high-assurance development.
Re: Another Look at Provable Security
#6There is a short discussion and links to their papers toward the bottom of the second section of this Wikipedia entry https://en.wikipedia.org/wiki/Provable_security
Re: Another Look at Provable Security
#7Some things that are important to remember:
(a) "Proof of security" is a term of art that doesn't mean what it sounds like. In cryptography, you "prove" specific things about an algorithm, often in the context of a "game" with one or more adversaries. You need to know more than that an algorithm has a proof; you also need to know which proofs those are, and how they apply to your application.
(b) Proofs generally apply to algorithms and low-level constructions. Once you start composing proven primitives into whole cryptosystems, typically, all bets are off. Proofs of entire protocols are an active research area.
(c) A proof will almost always apply to the abstract, mathematical notion of an algorithm or construction, not to the code that might implement it.
I apologize in advance at how little this has to do with the actual resource linked here; I'm just sort of predicting what the thread on HN, if any, would look like.
Re: Another Look at Provable Security
#8Very interesting. How does one get comfortable relying on cryptography that uses a method which lacks provable security? Simulating proof based on actual use?
Two questions that I find myself asking: 1. Are proofs effective at judging the security of a protocol? For example many proofs rely on the random oracle model, yet the random oracle model is problematic. How can we construct convincing proofs? 2. Are there better measures of security? For example crypto-contests in which people try to break other peoples algorithms. Very little systems security relies on proofs (sys…
What's an example of a protocol that has been well-served by formal methods prior to 2015?
Contests have fared well at selecting algorithms, but (prepared to be smacked back for this), ad hoc methods have done OK with algorithms as well --- you might say MD5 is an exception, but MD5 didn't have much competition when it was "selected". You might also say RC4, but RC4's history is very complicated.
Re: Another Look at Provable Security
#9Earlier quoted context omitted.
Two questions that I find myself asking: 1. Are proofs effective at judging the security of a protocol? For example many proofs rely on the random oracle model, yet the random oracle model is problematic. How can we construct convincing proofs? 2. Are there better measures of security? For example crypto-contests in which people try to break other peoples algorithms. Very little systems security relies on proofs (sys…
What's an example of a protocol that has been well-served by formal methods prior to 2015 ? Contests have fared well at selecting algorithms, but (prepared to be smacked back for this), ad hoc methods have done OK with algorithms as well --- you might say MD5 is an exception, but MD5 didn't have much competition when it was "selected". You might also say RC4, but RC4's history is very complicated.
Not sure what you mean by "well-served"? In terms of design, I've seen attempts at proofs discover attacks that likely would not have been otherwise found during development. In that case the proof served the designers in building a more secure protocol. Some of the early kerberos work could have benefited from making the designers prove or at very least justify their claims (say the use of xor fan-folding as a one-way function).
Does a proof increase your confidence in an algorithm? As someone that worked on MD6's proof of differential resistance it certainly increased my confidence in the protocols ability to resist certain types of attack.
By ad-hoc do you mean people selecting algorithms without a contest? If so I would counter with the following incomplete list of broken ad-hoc standards: DTD-1, FEAL, WEP, A5/1, A5/2, KASUMI, GOST 28147-89, Cryptomeria cipher, CCS, SHA-0.
The crypto that has held up, has generally held up and most of the other ones that haven't we don't use, so we may be biased toward remembering good ad-hoc crypto and forgetting the bad.
Re: Another Look at Provable Security
#10It's better to read the papers where they attempt provable security and then those published years later reviewing that work or those methods. Certain methods worked well, some failed over time, and so on. The lessons learned and looking back papers are where I find the most wisdom in this field. Naturally. The papers on Orange Book-era B3 and A1 class systems along with the Common Criteria EAL6/EAL7 works taught me…
Do you have any links/references to the papers you mention?