11–20 of 22 posts
For instance, to my knowledge the Hashed El Gamal proof in Easycrypt checkes the whole proof, not just the hops. (If I understood Remark 2 correctly)
Some 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 app…
[1] https://en.wikipedia.org/wiki/Agda_(programming_language)
Earlier quoted context omitted.
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-w…
1) "Provable security" is a misleading term. Those well versed in the field understand that it is a computational proof of a mathematical object, not in anyway a statement of the practical security of an algorithm when implemented in computer code. However, many people misunderstand this to mean "unbreakable" or "perfect". Menezes and Koblitz see it as too frequently acting as a marketing gimmick, something that allows vendors trying to sell security software to say "it's based on provably secure algorithms" without anyone understanding what that means. To them, the misleading quality of the term outweighs its value. I generally disagree with them on this point, not because the point isn't well taken, but because it is far too common for phrases from academic discourse to be misunderstood outside the specific field (e.g., teleportation in quantum mechanics) for such a semantic argument to carry any weight with the specific case of provable security.
(2) Provable security proofs have frequent gaps/the authors do not recognize important assumptions they are operating under. Their "Another look..." papers focus on these cases, and it is somewhat widespread. Most of the concerns tend to be completely academic, and don't open any practical attack vectors, however their point tends to be that computational proofs are dependent on assumptions that allow a positive proof of a negative, and if the methods of the proofs sufficiently obfuscate those assumptions to where their practitioners frequently miss them, it calls the validity of the arguments into suspect. The best example of this is probably their discussion in the original 'Another look at "provable security"' article linked to on the right of the proof of Optimal Asymmetric Encryption Padding (OAEP, required since textbook RSA and other asymmetric encryption algorithms leak information about the plaintext, in RSA's case, the Jacobi symbol). It's hard to argue with their evidence, and their work has definitely led to a much more critical eye of the proof justifications and assumption discussions given in newer articles.
(3) "Provable security" misses the point. To Menezes and Koblitz, the goals of cryptography mean it shouldn't be treated as a discipline of mathematics, and while academic cryptographers chase the abstract goal of provable security and debate the philosophical strengths of computational vs. information theoretic arguments, "real-world" cryptographers, including those working for the intelligence establishments, focus on useful goals like efficiency and ease of implementation in software and hardware. To them, building cryptosystems using primitives with strong heuristic arguments for their security which are easy to implement is far more beneficial for security than the most perfectly crafted mathematical algorithm will be. In addition, although the academic field of cryptography can easily adapt to any new result which challenges basic assumptions (say, a result attacking the hardness of the DLP or factoring), all the systems relying on those assumptions in practice will be broken or greatly damaged, so holding those assumptions as central to total security is problematic. As someone particularly interested in how cryptographic systems delegate and understand trust, this argument carries a lot of weight with me, and is part of the reason that although I consider having a solid understanding of the theory and practice of provable security to be a necessary piece to greater understanding of the field, my short and longer term interests in cryptography are focusing around secondary qualities cryptosystems and their primitives.
Some 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 app…
Regarding (c), if your program is written say Agda[1], the code can come with a proof that it has the mathematical properties you want. Or rather, your implementation might simply be the proof. [1] https://en.wikipedia.org/wiki/Agda_(programming_language)
This 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-hid…
Ten earnest mathematicians try. 9 fail. The tenth structures the problem in such a way that the solution is meaningless but not obviously so-- his work gets published. But he doesn't know and certantly never intended to produce a meaningless proof.
When useful proofs are harder to construct than difficult to detect as not useful trivial proofs, we should expect lots of the latter, even just by chance.
Some 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 app…
Regarding (c), if your program is written say Agda[1], the code can come with a proof that it has the mathematical properties you want. Or rather, your implementation might simply be the proof. [1] https://en.wikipedia.org/wiki/Agda_(programming_language)
This 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-hid…
Your description sounds like intent, but it's important to keep in mind there is a selection force here. Ten earnest mathematicians try. 9 fail. The tenth structures the problem in such a way that the solution is meaningless but not obviously so-- his work gets published. But he doesn't know and certantly never intended to produce a meaningless proof. When useful proofs are harder to construct than difficult to detec…
Also, I don't think that such work is meaningless in any way. Any discovery in math is meaningful in itself. It just isn't as applicable in real life as advertised (or the application is much more difficult than advertised).
It'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?
http://www.iwia.org/2005/Schell2005.PDF Describes GEMSOS security kernel (A1 class) with nice graphics to illustrate the approach.
http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf VAX Security Kernel (A1 class). Pay special attention to the layering of the kernel, coding strategy, and assurance section.
http://cisr.nps.edu/downloads/sdm/SEKE08-Shaffer.pdf Shaffer's Alloy technique elaborates a bit on how state machines are useful in security arguments, even without full formal.
http://cryptosmith.org/docs/Lock-eff-acm.pdf Costs and effectiveness of assurance activities for LOCK system (A1 class).
http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf Modern effort (seL4) to exceed EAL7 by bringing verification to code itself. Note that some A1 projects had close to 1-to-1 spec to implementation mapping. So, full formal might be replaced by low-level, verified specs and matching code verified by inspection, etc.
http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf Rockwell Collin's EAL7 framework for AAMP7G processor and CRYPTOL integration
http://www.crash-safe.org/assets/verified-ifc-long-draft-201... Previous work proved kernels supported MLS or MILS models. This is better given it's proving a hardware mechanism both enforces a security requirement and meets functional requirements. Significant given SAFE (see crash-safe.org) makes inherently secure apps easier to write.
http://goto.ucsd.edu/quark/usenix12.pdf Proving security properties of a web browser. Typically, you know the work is legit if it spends time talking about the flaws formal verification caught. I don't see so much of that in this but they might have omitted that to publish what worked instead.
http://www.cse.chalmers.se/~andrei/jsac.pdf A significant amount of recent work builds it in the language itself.
http://web.archive.org/web/20130718103347/http://cygnacom.co... Cygnacom's breakdown of Evaluation Assurance Level's is pretty nice. Shows the extra efforts put in and what you get.
http://pastebin.com/y3PufJ0V My framework compliments that and reminds that it must be applied to every layer down to the gates.
So, although my sharing is limited by paywalls, I hope you find these interesting and can see the different perspectives of highly assured security. There have been numerous successes in independent testing, pen-testing, and field use. Also remember that this is only provable security rather than verification of properties in general. The field of verification and correctness assurance has progressed quite a bit (see CompCert, SPARK, Esterel, etc). Have fun.
Earlier quoted context omitted.
Do you have any links/references to the papers you mention?
Most of the best papers are behind paywalls, unfortunately. I do have a small sampling on-hand from there and now that illustrate some of the high-assurance methods. http://www.iwia.org/2005/Schell2005.PDF Describes GEMSOS security kernel (A1 class) with nice graphics to illustrate the approach. http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf VAX Security Kernel (A1 class). Pay special attention to the lay…
In this ppt http://usacac.army.mil/cac2/cew/repository/presentations/3_H...
there is mention of an interesting tool/language called Spark Ada: http://www.spark-2014.org/
It makes me think that maybe my next study topic should be Spark or Esterel instead of Rust/Golang/some JS thing.