軟問題：缺乏數學嚴謹性導致安全漏洞的例子？
即使在安全證明缺乏數學嚴謹性或完全缺失的情況下，加密工具也經常被採用。
行業中是否存在著名的安全漏洞案例，其中基礎加密（在此之前）被認為是安全的？
SSH 協議具有復雜的記錄格式，具有加密的消息長度、可變填充、加密和 MAC等。 這個複雜的系統是在沒有任何將系統安全性與建構塊安全性相關的正式分析的情況下設計的，事實證明，它很容易受到利用 MAC 驗證作為獲取明文資訊的預言機的攻擊（免付費牆），導致在 OpenSSH 等流行實現中對 SSH 進行明文恢復攻擊。
SSL/TLS 協議在非正式設計方面有著悠久而骯髒的歷史，導致了多種攻擊：
- Bleichenbacher RSAES-PKCS1-v1_5 padding oracle攻擊破壞了未經形式分析設計的基於 RSA 的加密方案，在 1998 年破壞了帶有 RSA 密鑰協議的 SSLv3，然後在 2014 年再次利用POODLE 攻擊破壞了安全破壞協議兼容性備份，然後在 2018 年再次通過ROBOT 攻擊打破了它。
- BEAST 攻擊已被 Phil Rogaway 在 2002 年註意到並在 2004 年針對 SSL/TLS 進行了理論上的記錄，該攻擊利用 SSL/TLS 未能遵循 CBC 的安全合約，這要求 IV 對於每條消息都是不可預知的。 ——該協議在沒有正式分析如何選擇 IV 的情況下部署了 CBC。
- Lucky 13 攻擊（網站）通過使用填充驗證的時序作為 CBC 填充預言來恢復明文，這源於 CBC 填充機制的設計，甚至沒有對其時序特徵進行簡單的形式分析。
- TLS 重新協商攻擊利用 TLS 協議中涉及密鑰重新協商和身份驗證的複雜狀態機（從未對其安全屬性進行過正式分析），在沒有通知的情況下偽造發送給 TLS 對等方的消息。
OpenPGP 協議是由90 年代的特設風格組合設計的，由通用且難以理解的公鑰加密和簽名建構塊組成，沒有正式處理它們如何組合在一起。
- “相當好的隱私”最初的承諾是保持電子郵件的私密性。但是，在 OpenPGP 中，將 RSA 等花哨的數學原語和 AES 等標準對稱密碼學結合起來加密長消息的方法是在沒有將它們與建構塊的安全性相關的正式分析的情況下設計的。
事實證明，這種方法實際上可以在真正的電子郵件客戶端中被利用，這種攻擊稱為EFAIL，可以洩漏消息內容（我對此的回答）。自 2002 年首次在理論上報告該問題後，OpenPGP 世界花了 15 年的時間才趕上 2018 年在實踐中發布的攻擊。
- PGP 的第二個承諾是防止私人電子郵件中的偽造。但是沒有正式的從 Alice 到 Bob的消息的概念——只有一條加密的消息給 Bob，以及一個來自 Alice 的簽名消息，可以隨意嵌套* …並且通常嵌套的方式是 Charlie 可以接收 Alice 發送給的消息並讓Bob 看起來就像是 Alice 將它發送給 Bob 一樣。當然，Alice 可以採取額外的步驟來命名消息中的收件人，而Bob 可以採取額外的步驟來檢查他的名字。該軟體也可以做到這一點。OpenPGP 設計者可以嘗試將與人類相關的互動形式化並分析它們的安全屬性，並且可以設計密碼學來支持人類使用。
但是，當遇到這個問題時，OpenPGP 設計者反而放棄了這一責任，聲稱密碼學不能解決適當使用技術的問題。直到今天，OpenPGP 協議還沒有正式的從 Alice 到 Bob的消息的概念——這可以通過標準的眾所周知的公鑰認證加密來實現——儘管它名義上是用於私人電子郵件。
- OpenPGP 中選擇的公鑰加密和簽名方案本身是在沒有任何正式分析的情況下設計的，將它們與經過充分研究的難題（如 RSA 問題或離散對數問題）相關聯，結果證明，特定的Elgamal 簽名方案和RSA 加密OpenPGP 使用的方案有問題。
我不清楚這些是否會導致對 OpenPGP 的實際利用——可能除了 GnuPG 中的實現錯誤，即使用相同的每消息秘密進行 Elgamal 簽名和加密，這說明了在不證明程式碼實現的情況下證明協議安全的危險協議正確。
這些攻擊都是針對由ad hoc工程設計的協議，沒有正式的分析來保證協議相對於其建構塊的安全性的安全性。但是原始的建構塊——比如 $ x^3 \bmod{pq} $ , 對一個秘密素數的乘積進行模立方；喜歡 $ g^x \bmod p $ , 以安全素數為模的標準基數的取冪；像 AES-256 排列系列；就像 Keccak 排列一樣——沒有正式的分析來保證它們相對於任何事物的安全性。是什麼賦予了？
協議的形式分析或可證明的安全性，由將協議的安全性與其建構塊的安全性相關的定理組成，只是獲得對密碼學安全性的信心的全球社會學系統的一部分：
- 我們懷疑 RSA 問題很難解決的原因是，地球上一些最聰明的密碼分析家幾十年來一直有強烈的動機去研究它，而且他們留下了幾十年來未能找到破解（比如說）RSA的方法的記錄。 -2048 成本低於 $ 2^{100} $ 每個鍵。對於某些組中的離散日誌，AES-256等也是如此。
- 使用 RSA 和 AES 對協議的形式分析使密碼分析者能夠集中精力，因此他們不必浪費時間研究 SSH、研究 OpenPGP、研究 SSLv3、研究 TLS、研究 WPA等，以尋找是否有某種方法打破這些協議。如果形式分析做得足夠好，密碼分析者可以將他們的精力花在少數原語上，而他們在未能破解這些原語上花費的精力越多，我們對原語以及建立在它們之上的一切的信心就越大。
像 SSH、OpenPGP、SSL/TLS等協議，沒有正式的分析，是社會對世界密碼分析員供應的巨大浪費。 形式化分析可以更有效地利用世界資源——而且它會得到回報，因為幾乎所有上述攻擊都可以通過研究所涉及協議的安全屬性和建構塊的安全合約來擷取：CBC在具有可預測 IV 的 TLS 中，PGP 中的公鑰加密未通過 IND-CCA 標準，PGP 和 TLS 中基於 RSA 的加密方案，而不降低 RSA 安全性，將 SSH 和 TLS 中的錯誤響應表示為選定密文的預言對手。
並非所有協議在設計後都易於進行正式分析（例如 TLS 重新協商的 trainwreck），但協議可以由易於理解的可組合部分設計，具有明確的安全契約以促進正式分析，而不是像加密小工具這樣的臨時聚集體90 年代，今天有像雜訊協議框架這樣的工具和雜訊資源管理器來組合具有內置形式分析的協議。
*有時無限嵌套！
在選擇用於橢圓曲線密碼學的曲線時，一些人建議使用各種類型的曲線，以避免某些會使系統容易受到攻擊的“壞”屬性。
MOV 攻擊在稱為超奇異曲線的類上破壞了 ECDSA。為了避免這種情況，一些人建議使用另一類稱為異常曲線的曲線，這些曲線保證不會是超奇異的。
然而，隨後發現這些曲線遭受了Smart 攻擊所利用的一個可以說是更嚴重的缺陷，這也破壞了 ECDSA。
我不知道在此期間是否有人按照使用這些的建議採取了行動，但它表明橢圓曲線非常微妙的數學特性會對整個系統產生巨大影響，並且不能充分理解這些特性可能產生嚴重的後果。