形式化建模针对SSH的Terrapin攻击
Formally Modeling the Terrapin Attack on SSH
浏览论文内容
中文总结 AI 辅助
本文提出部分选择状态下的通道完整性形式化模型，分析SSH中八种AEAD模式，证明EtM模式和ChaCha20-Poly1305在仅密文模型下不安全，AES-GCM最安全，并发现对EaM-CBC的新型选择明文攻击。
中文摘要 AI 辅助
针对SSH通道完整性的Terrapin攻击（USENIX Security 2024）使用了一种新颖的攻击向量：对通道状态的攻击。令人惊讶的是，并非所有SSH的AEAD模式都同样受到此攻击的影响，并且“未受影响”是否意味着“安全”仍然是一个悬而未决的问题。现有的安全通道形式化模型基于有状态加密。然而，这些模型并未定义通道状态是什么，以及它如何作为不同AEAD模式的输入。在本文中，我们提出了一个在部分选择状态下的通道完整性形式化模型。应用于Terrapin攻击时，所选状态是SSH序列号。它使用一个抽象的有状态加密接口，我们为SSH中使用的八种最突出的AEAD模式提供了伪代码描述。通过改变SND预言机，我们可以对仅密文（CO；Terrapin攻击）、已知明文（KPA）和选择明文（CPA）攻击进行建模。这使我们能够为AEAD模式的安全性建立具体界限。我们发现，SSH中的所有三种Encrypt-then-MAC（EtM）模式和ChaCha20-Poly1305在CO模型中是不安全的。AES-GCM是唯一在所有三种模型变体中安全的密码。超越Terrapin，我们展示了使用CBC密码的Encrypt-and-MAC（EaM）即使在KPA模型中也是安全的。特别是，我们描述了一种新颖的类似BEAST的选择明文攻击，针对EaM-CBC的通道完整性，这将该方案的KPA和CPA模型区分开来。
英文摘要
The Terrapin attack against SSH channel integrity (USENIX Security 2024) used a novel attack vector: attacks on the channel state. Surprisingly, not all AEAD modes of SSH were equally affected by this attack, and it remained an open question if "unaffected" meant "secure". Existing formal models for secure channels are based on stateful encryption. However, these models do not define what the channel state is and how it is used as input to the different AEAD modes. In this paper, we propose a formal model for channel integrity under partially chosen state. Applied to the Terrapin attack, the chosen state is the SSH sequence number. It uses an abstract stateful encryption interface, for which we provide pseudocode descriptions for the eight most prominent AEAD modes used in SSH. By varying the SND oracle, we can model ciphertext-only (CO; the Terrapin attack), known-plaintext (KPA), and chosen-plaintext (CPA) attacks. This allows us to establish concrete bounds on the security of the AEAD modes. We find that all three Encrypt-then-MAC (EtM) modes and ChaCha20-Poly1305 in SSH are insecure in the CO model. AES-GCM is the only cipher secure in all three model variants. Going beyond Terrapin, we show that Encrypt-and-MAC (EaM) with a CBC cipher is secure, even in the KPA model. In particular, we describe a novel BEAST-like chosen-plaintext attack on the channel integrity of EaM-CBC, which separates the KPA and CPA models for this scheme.
发表机构
- Ruhr University Bochum（鲁尔大学波鸿分校）
机构由 AI 辅助整理，请以论文原文为准。
