  In this paper we're going to explore the ways in which security proofs can
fail, and their broader lessons for security engineering. To mention just one
example, Larry Paulson proved the security of SSL/TLS using his theorem prover
Isabelle in 1999, yet it's sprung multiple leaks since then, from timing
attacks to Heartbleed. We will go through a number of other examples in the
hope of elucidating general principles. Proofs can be irrelevant, they can be
opaque, they can be misleading and they can even be wrong. So we can look to
the philosophy of mathematics for illumination. But the problem is more
general. What happens, for example, when we have a choice between relying on
mathematics and on physics? The security proofs claimed for quantum
cryptosystems based on entanglement raise some pointed questions and may engage
the philosophy of physics. And then there's the other varieties of assurance;
we will recall the reliance placed on FIPS-140 evaluations, which API attacks
suggested may have been overblown. Where the defenders focus their assurance
effort on a subsystem or a model that cannot capture the whole attack surface
they may just tell the attacker where to focus their effort. However, we think
it's deeper and broader than that. The models of proof and assurance on which
we try to rely have a social aspect, which we can try to understand from other
perspectives ranging from the philosophy or sociology of science to the
psychology of shared attention. These perspectives suggest, in various ways,
how the management of errors and exceptions may be particularly poor. They do
not merely relate to failure modes that the designers failed to consider
properly or at all; they also relate to failure modes that the designers (or
perhaps the verifiers) did not want to consider for institutional and cultural
reasons.
