4 ms·

Very interesting. How does one get comfortable relying on cryptography that uses a method which lacks provable security? Simulating proof based on actual use?

EthanHeilman 11y ago
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.
- tptacek 11y ago
  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.
  - EthanHeilman 11y ago
    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.
    - tptacek 11y ago
      People have used formal methods to find flaws in protocols, but I'm unaware of a protocol that is assured formally in any meaningful way. Certainly not TLS or IPSEC. I guess I'm asking, is there a protocol you feel more comfortable working with due to formal assurance?

EthanHeilman 11y ago

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.

tptacek 11y ago
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.
- EthanHeilman 11y ago
  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.
  - tptacek 11y ago
    People have used formal methods to find flaws in protocols, but I'm unaware of a protocol that is assured formally in any meaningful way. Certainly not TLS or IPSEC. I guess I'm asking, is there a protocol you feel more comfortable working with due to formal assurance?