Formally Modeling the Terrapin Attack on SSH
Researchers formally model the Terrapin SSH attack and show which AEAD modes remain secure.
An arXiv cs.CR paper formally models SSH channel integrity when an attacker can partially choose channel state, using the sequence number as in the 2024 Terrapin attack. It gives pseudocode for eight prominent SSH AEAD modes and varies the sending oracle across ciphertext-only, known-plaintext, and chosen-plaintext attacks. All three Encrypt-then-MAC modes and ChaCha20-Poly1305 are insecure in the ciphertext-only model, while AES-GCM is secure in all three. Encrypt-and-MAC with CBC remains secure under known plaintext, but a new BEAST-like chosen-plaintext attack breaks its channel integrity.
- The model treats the SSH sequence number as partially chosen state.
- Encrypt-then-MAC modes and ChaCha20-Poly1305 fail ciphertext-only security.
- AES-GCM stays secure in ciphertext-only, known-plaintext, and chosen-plaintext models.
- A BEAST-like chosen-plaintext attack breaks Encrypt-and-MAC with CBC.
Full article234 words · extracted from arxiv.org · click to collapse
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.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.26358