This article has a bit of an "ivory tower" reek to it, I don't wholly buy it. Some points are clearly valid: use modern crypto primitives if you can, and know t

This article has a bit of an "ivory tower" reek to it, I don't wholly buy it. Some points are clearly valid: use modern crypto primitives if you can, and know their properties. But things are more complicated than that. First, even if you say that proofs are enough, you got to know what you're proving. The problem is that, AFAIK, most security properties are actually defined as absence of a particular attack (or a class thereof). Thus knowing the properties you want to achieve is equivalent to knowing the attacks you want to avoid. In other words, even if I build my system to have a property A, I might not know that I also need to attain property B (thus securing it against the complement of B). Second, if you do want actual proofs, well, good luck. You start off with the indistinguishability stuff, which is not easy in itself. Toss in the distributed aspects of Internet applications and you've got yourself a proper mess. Case distinctions abound, this stuff slowly crosses into the domain of intractable. If you look at the game-based security proofs, well, for anything non-trivial, who can really be confident that the proofs are correct? Machine verification would help, but our tools are both still too weak, and still only a domain of select few specialists. Third, even if you do get your proofs, well, more likely than not, these are going to be based on a simplified model which will sweep a lot of stuff under the rug. E.g. I don't know of works which address things like timing attacks in anything of even remotely practical value. And there's a bunch of other stuff, keys distributed, management, etc. Lastly, as lot of other commenters have pointed out, you are also more likely than not to deal with existing codebases at some point, where you might end up plugging the holes rather than constructing.