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.

翻译：本文旨在探讨安全证明可能失败的方式，以及它们对安全工程的更广泛启示。仅举一例：拉里·保罗森（Larry Paulson）于1999年使用其定理证明工具Isabelle证明了SSL/TLS的安全性，但此后该协议屡次出现漏洞，从时序攻击到心脏滴血（Heartbleed）漏洞。我们将回顾多个其他案例，以期阐明一般性原则。证明可能不相关、可能晦涩难懂、可能具有误导性，甚至可能本身就有误。为此，我们可以从数学哲学中寻求启示。但问题更为普遍。例如，当我们必须在依赖数学与依赖物理学之间做出选择时，会发生什么？基于纠缠的量子密码系统所声称的安全性证明引发了一些尖锐问题，并可能涉及物理哲学。此外还有其他类型的保证手段；我们将回顾对FIPS-140评估的依赖，而API攻击表明这种依赖可能被夸大了。当防御者将其保证工作集中于一个无法覆盖整个攻击面的子系统或模型时，他们可能只是在告诉攻击者应将精力集中在哪里。然而，我们认为问题比这更深刻、更广泛。我们试图依赖的证明与保证模型具有社会性的一面，我们可以从科学哲学或社会学、以及共享注意力的心理学等其他视角来理解这一方面。这些视角以不同方式表明，错误与异常的管理可能尤其糟糕。它们不仅涉及设计者未能适当考虑或完全未考虑的失效模式，还涉及设计者（或验证者）出于制度和文化原因而根本不愿考虑的失效模式。