该论文针对 SSH 通道完整性，提出一个在“部分选定状态”（partially chosen state）下形式化建模的框架，以回答 Terrapin 攻击（USENIX Security 2024）留下的开放问题：在 Terrapin 攻击中，SSH 通道状态被当作攻击向量，不同 AEAD 模式受影响程度不一，而“未受影响”是否等于“安全”尚不明确。作者指出现有安全通道形式化模型基于有状态加密，却未定义通道状态是什么、以及状态如何作为不同 AEAD 模式的输入，因此无法精确刻画此类攻击。论文的核心方法是将 SSH 序列号建模为被攻击者部分选定的状态，并定义一个抽象的有状态加密接口，为 SSH 中八种最主流的 AEAD 模式给出伪代码描述。通过改变发送（SND）预言机，模型可覆盖仅密文（CO，即 Terrapin 攻击）、已知明文（KPA）与选择明文（CPA）三类攻击，从而给出各 AEAD 模式的具体安全界。主要发现：三种 Encrypt-then-MAC（EtM）模式与 ChaCha20-Poly1305 在 CO 模型下均不安全；AES-GCM 是唯一在三种模型变体下均安全的方案。进一步地，作者证明 Encrypt-and-MAC（EaM）配合 CBC 即使在 KPA 模型下仍安全，并提出一种新的类 BEAST 选择明文攻击，可破坏 EaM-CBC 的通道完整性，从而在该方案上区分 KPA 与 CPA 模型。该工作适合密码学与协议安全研究者、SSH 实现维护者及安全架构师阅读。