Memodelkan Serangan Terrapin pada SSH secara Formal

Model formal untuk integritas kanal pada keadaan yang dipilih sebagian mengungkap batas keamanan untuk mode AEAD di SSH

Jörg Schwenk; Fabian Bäumer; Marcus Brinkmann· 2026· DOI 10.48550/arXiv.2609.26358

Masalah inti

Serangan Terrapin, yang dipresentasikan di USENIX Security 2024, mengeksploitasi vektor baru: serangan terhadap keadaan kanal di SSH. Teramati bahwa tidak semua mode AEAD terkena dampak yang sama, sehingga menyisakan pertanyaan apakah 'tidak terkena dampak' berarti 'aman'. Model formal yang ada untuk kanal aman mengasumsikan enkripsi stateful tetapi gagal mendefinisikan keadaan kanal dan perannya sebagai masukan bagi mode AEAD. Karya ini mengatasi celah tersebut dengan mengusulkan model formal untuk integritas kanal pada keadaan yang dipilih sebagian, yang secara khusus menyasar nomor urut SSH sebagai keadaan yang dipilih. Model ini menggunakan antarmuka enkripsi stateful abstrak, dengan pseudokode untuk delapan mode AEAD terkemuka yang digunakan di SSH. Dengan memvariasikan oracle SND, model ini menangkap serangan ciphertext-only (CO), known-plaintext (KPA), dan chosen-plaintext (CPA), sehingga memungkinkan batas keamanan yang konkret. Temuannya menunjukkan bahwa ketiga mode Encrypt-then-MAC (EtM) dan ChaCha20-Poly1305 tidak aman pada model CO, sedangkan AES-GCM aman pada ketiga model. Selain itu, Encrypt-and-MAC (EaM) dengan CBC aman bahkan pada model KPA, dan serangan chosen-pla

Analisis formal menghasilkan batas keamanan konkret untuk delapan mode AEAD. Temuan utamanya adalah: - Ketiga mode Encrypt-then-MAC (EtM) dan ChaCha20-Poly1305 tidak aman pada model ciphertext-only (CO), yang berarti rentan terhadap serangan Terrapin. - AES-GCM adalah satu-satunya cipher yang aman pada ketiga varian model (CO, KPA, CPA). - Encrypt-and-MAC (EaM) dengan cipher CBC aman bahkan pada model known-plaintext (KPA). - Serangan chosen-plaintext baru yang mirip BEAST pada EaM-CBC memisahkan model KPA dan CPA, yang menunjukkan bahwa EaM-CBC tidak aman pada model CPA. Hasil ini memberikan hierarki keamanan yang jelas: AES-GCM > EaM-CBC (aman KPA tetapi tidak aman CPA) > EtM dan ChaCha20-Poly1305 (tidak aman pada CO). Batas-batas dinyatakan dalam hal keunggulan penyerang, dengan parameter konkret. Misalnya, keunggulan terhadap mode EtM pada model CO tidak dapat diabaikan, sedangkan untuk AES-GCM dapat diabaikan di bawah asumsi standar.

Serangan Terrapin, yang dipresentasikan di USENIX Security 2024, mengeksploitasi vektor baru: serangan terhadap keadaan kanal di SSH. Teramati bahwa tidak semua mode AEAD terkena dampak yang sama, sehingga menyisakan pertanyaan apakah 'tidak terkena dampak' berarti 'aman'. Model formal yang ada untuk kanal aman mengasumsikan enkripsi stateful tetapi gagal mendefinisikan keadaan kanal dan perannya sebagai masukan bagi mode AEAD. Karya ini mengatasi celah tersebut dengan mengusulkan model formal untuk integritas kanal pada keadaan yang dipilih sebagian, yang secara khusus menyasar nomor urut SSH sebagai keadaan yang dipilih. Model ini menggunakan antarmuka enkripsi stateful abstrak, dengan pseudokode untuk delapan mode AEAD terkemuka yang digunakan di SSH. Dengan memvariasikan oracle SND, model ini menangkap serangan ciphertext-only (CO), known-plaintext (KPA), dan chosen-plaintext (CPA), sehingga memungkinkan batas keamanan yang konkret. Temuannya menunjukkan bahwa ketiga mode Encrypt-then-MAC (EtM) dan ChaCha20-Poly1305 tidak aman pada model CO, sedangkan AES-GCM aman pada ketiga model. Selain itu, Encrypt-and-MAC (EaM) dengan CBC aman bahkan pada model KPA, dan serangan chosen-plaintext baru yang mirip BEAST pada EaM-CBC memisahkan model KPA dan CPA.

Para penulis mengusulkan model formal untuk integritas kanal pada keadaan yang dipilih sebagian. Model ini mengabstraksi antarmuka enkripsi stateful, di mana keadaan (misalnya nomor urut SSH) dipilih sebagian oleh penyerang. Mereka menyediakan deskripsi pseudokode untuk delapan mode AEAD yang digunakan di SSH: AES-GCM, ChaCha20-Poly1305, serta berbagai konstruksi EtM dan EaM. Keamanan dianalisis dengan memvariasikan oracle SND untuk memodelkan kemampuan serangan yang berbeda: ciphertext-only (CO), known-plaintext (KPA), dan chosen-plaintext (CPA). Hal ini memungkinkan penurunan batas konkret pada keamanan setiap mode. Model formal didefinisikan menggunakan gagasan keamanan berbasis game, di mana penyerang berinteraksi dengan oracle untuk merusak integritas kanal. Model ini menangkap serangan Terrapin sebagai serangan CO, di mana penyerang dapat memanipulasi nomor urut. Analisis ini menghasilkan batas keamanan untuk setiap mode AEAD, mengidentifikasi mode mana yang aman pada model serangan mana. Metodologi ini mencakup serangan chosen-plaintext baru yang mirip BEAST pada EaM-CBC, yang menunjukkan pemisahan antara keamanan KPA dan CPA untuk skema tersebut.

Model formal makalah ini memperjelas keamanan mode AEAD SSH terhadap serangan integritas kanal. Temuan bahwa AES-GCM aman di semua model sangat penting, karena menunjukkan bahwa AES-GCM sebaiknya dipilih untuk implementasi SSH. Ketidakamanan mode EtM dan ChaCha20-Poly1305 pada model CO menyoroti perlunya pemilihan mode yang cermat. Serangan baru yang mirip BEAST pada EaM-CBC menunjukkan bahwa bahkan mode yang dianggap aman pada KPA dapat dipatahkan pada CPA, yang menekankan pentingnya mempertimbangkan model serangan yang lebih kuat. Abstraksi model terhadap keadaan yang dipilih sebagian dapat diterapkan pada protokol lain di mana keadaan digunakan sebagai masukan bagi enkripsi. Hasil ini juga berimplikasi pada desain protokol kanal aman di masa depan, yang menyarankan agar keadaan disertakan dengan cara yang tahan terhadap serangan keadaan terpilih. Para penulis mencatat bahwa model mereka tidak mencakup semua kemungkinan vektor serangan, seperti serangan timing, tetapi memberikan fondasi untuk menganalisis integritas kanal. Pemisahan antara KPA dan CPA untuk EaM-CBC adalah kontribusi baru, yang menunjukkan bahwa prinsip serangan BEAST meluas melampaui TLS ke SSH. Secara keseluruhan, makalah ini memberikan kerangka kerja yang ketat untuk mengevaluasi keamanan mode AEAD di SSH dan menawarkan rekomendasi konkret untuk konfigurasi yang aman.

Praktisi dan peneliti ilmu komputer

Membuka konten member…