Protokol Needham-Schroeder dan Serangan

Protokol Needham-Schroeder (1978) merupakan salah satu upaya formal pertama untuk merancang protokol autentikasi kriptografis menggunakan pihak ketiga tepercaya (TTP). Tujuannya adalah memungkinkan dua pihak, Alice dan Bob, saling mengautentikasi dan menetapkan kunci sesi bersama menggunakan Authentication Server (AS) tepercaya yang berbagi kunci jangka panjang dengan setiap pihak. Protokol ini mendahului infrastruktur kunci publik, tetapi memperkenalkan konsep—nilai sekali pakai untuk menjamin kebaruan dan distribusi kunci melalui server tepercaya—yang tetap menjadi inti protokol modern seperti Kerberos. Pemahaman terhadap NS dan kegagalannya membentuk seluruh bidang analisis protokol.

Protokol kunci simetris NS berlangsung dalam lima langkah. (1) Alice mengirim {A, B, Na} ke AS untuk meminta kunci sesi bagi komunikasi dengan Bob. (2) AS merespons Alice dengan {Na, B, Kab, {Kab, A}_Kb}_Ka—kunci sesi Kab, tiket untuk Bob, dan semuanya dienkripsi menggunakan kunci jangka panjang Alice Ka. (3) Alice meneruskan tiket {Kab, A}_Kb kepada Bob. (4) Bob mendekripsi tiket, mengambil Kab, lalu mengirim {Nb}_Kab kepada Alice (sebuah tantangan). (5) Alice merespons {Nb-1}_Kab untuk membuktikan bahwa ia memegang Kab. Nilai sekali pakai Nb mencegah pemutaran ulang langkah 4. Protokol ini memiliki serangan pemutaran ulang yang telah diketahui, yang dimanfaatkan oleh Denning dan Sacco (1981).

Denning dan Sacco (1981) menemukan sebuah kelemahan: respons AS pada langkah 2 tidak mutakhir—respons tersebut tidak mengandung penanda waktu atau nilai sekali pakai yang diberikan server. Penyerang bernama Mallory, yang sebelumnya mencegat kunci sesi lama Kab (dengan menyusupi sesi terdahulu), dapat memutar ulang tiket lama {Kab, A}_Kb kepada Bob kapan saja di masa mendatang. Bob, yang menerima sesuatu yang tampak seperti tiket sah dari Alice, menggunakan kunci Kab yang telah disusupi untuk sesi tersebut. Perbaikan dari Denning dan Sacco adalah menambahkan penanda waktu ke respons AS dan tiket. Perbaikan ini diterapkan dalam Kerberos—penanda waktu disematkan dalam tiket untuk membatasi masa berlakunya.

Protokol kunci publik NS (juga pada 1978) dirancang untuk autentikasi timbal balik dua pihak menggunakan kriptografi kunci publik. (1) Alice mengirim {Na, A}_PKb kepada Bob (nilai sekali pakai Na dienkripsi dengan kunci publik Bob). (2) Bob merespons {Na, Nb}_PKa (kedua nilai sekali pakai dienkripsi dengan kunci publik Alice). (3) Alice merespons {Nb}_PKb (mengembalikan nilai sekali pakai Bob yang dienkripsi dengan kunci publiknya). Setelah pertukaran ini, kedua pihak memegang kedua nilai sekali pakai (Na, Nb) dan dapat menurunkan kunci sesi. Protokol ini tampak aman selama 17 tahun—hingga serangan Lowe pada 1995.

Gavin Lowe (1995) menemukan kelemahan kritis menggunakan pemeriksa model Kegagalan dalam Penalaran Komposisional (FDR). Mallory dapat menyamar sebagai Bob di hadapan Alice sambil meneruskan pesan kepada Bob yang jujur. Langkah 1: Alice mengirim {Na, A}_PKm kepada Mallory (karena mengira sedang berbicara dengan Bob). Mallory meneruskan {Na, A}_PKb kepada Bob. Langkah 2: Bob merespons {Na, Nb}_PKa, yang didekripsi Mallory dan dienkripsi kembali untuk Alice: {Na, Nb}_PKa. Alice mendekripsinya dan mengambil Nb. Langkah 3: Alice mengirim {Nb}_PKm (karena mengira pesan ini dikirim kepada Bob). Mallory mendekripsi dan meneruskan {Nb}_PKb kepada Bob. Bob meyakini telah menyelesaikan autentikasi timbal balik dengan Alice—tetapi sebenarnya Alice sedang mengautentikasi Mallory. Perbaikannya: pada langkah 2, Bob harus menyertakan identitasnya sendiri: {Na, Nb, B}_PKa.

Perbaikan Lowe pada protokol NSPK sederhana namun mendalam: respons Bob pada langkah 2 harus menyertakan identitas Bob, B, sehingga menjadi {Na, Nb, B}_PKa. Sekarang, ketika Alice menerima respons tersebut, ia memeriksa bahwa identitas B yang disertakan cocok dengan pihak yang hendak dihubunginya. Mallory tidak dapat mengganti respons tersebut—Mallory memerlukan kunci privat Alice untuk membuat {Na, Nb, M}_PKa yang valid dan lolos pemeriksaan Alice. Pelajaran ini digeneralisasi sebagai Prinsip Needham-Abadi: pesan autentikasi harus mengikat identitas pengirim secara eksplisit, bukan hanya mengandalkan konteks untuk mengenali pengirim.

Penemuan Lowe tentang kelemahan NSPK dibantu oleh pemeriksa model FDR (Penyempurnaan Kegagalan-Divergensi), yang menjelajahi secara menyeluruh semua kemungkinan pelaksanaan protokol, termasuk intervensi lawan. Hal ini mendorong pengembangan alat analisis protokol formal: Proverif (berdasarkan kalkulus pi terapan) dapat membuktikan atau menyangkal properti autentikasi dan kerahasiaan dalam sesi tak terbatas. Tamarin Prover menggunakan penulisan ulang multiset dan mendukung protokol kompleks seperti TLS 1.3 dan Signal. AVISPA dan Scyther adalah alat lainnya. Rancangan protokol modern (TLS 1.3, Signal, Noise) menjalani verifikasi formal sebelum diterapkan—warisan langsung dari peristiwa NS/Lowe.

Serangan terhadap NS memperjelas perbedaan antara tujuan-tujuan autentikasi. Autentikasi entitas: membuktikan bahwa suatu pihak sedang aktif dan berpartisipasi dalam protokol (kebaruan penting). Autentikasi asal data: membuktikan bahwa pesan tertentu dibuat oleh pihak tertentu (tidak selalu berarti pihak tersebut sedang aktif). Serangan Lowe merusak autentikasi entitas—Alice yakin sedang melakukan autentikasi dengan Bob, padahal ia sebenarnya sedang melakukan autentikasi dengan Mallory, yang meneruskan pesan kepada Bob. Spesifikasi protokol modern menyatakan tujuan secara tepat: "Alice terautentikasi kepada Bob sebagai pemrakarsa sesi ini." Tujuan yang samar menghasilkan spesifikasi ambigu yang lolos tinjauan informal tetapi gagal dalam analisis formal.

Kelas serangan lain yang berkaitan dengan NS adalah serangan refleksi: Mallory memutar ulang pesan dari Alice kembali kepada Alice. Jika protokol bersifat simetris (kedua pihak menggunakan kunci dan format pesan yang sama), Alice mungkin menerima tantangannya sendiri sebagai respons yang sah dari Bob. Pertahanan: gunakan arah kunci yang berbeda (kunci enkripsi dan dekripsi terpisah untuk setiap arah) atau sertakan penanda peran dalam pesan (pihak yang mengenkripsi menyertakan "I am initiator" dalam pesan). Protokol modern seperti TLS menyertakan string label khusus peran dalam kunci yang diturunkan HKDF (menggunakan "c e traffic" untuk klien dan "s hs traffic" untuk peladen) guna mencegah refleksi.

Serangan pencampuran sesi menggabungkan pesan dari beberapa sesi protokol yang berlangsung bersamaan untuk memalsukan autentikasi. Jika Alice menjalankan dua sesi secara bersamaan, Mallory dapat mencampur pesan dari keduanya untuk membuat sesi gabungan yang konsisten tetapi tidak valid, yang mengautentikasi Mallory. Pertahanan: pengikatan sesi—setiap pesan harus terikat secara kriptografis pada konteks sesinya (misalnya, menyertakan ID sesi atau menggunakan kunci unik untuk setiap sesi). TLS mencegah pencampuran sesi melalui pesan Finished, yang merupakan MAC atas seluruh transkrip sesi saat ini. Pesan apa pun yang dicampur dari sesi lain akan mengubah transkrip dan membuat nilai Finished tidak valid.

Protokol Needham-Schroeder secara langsung memengaruhi rancangan Kerberos (stempel waktu untuk mencegah pemutaran ulang, diambil dari perbaikan Denning-Sacco), TLS (MAC transkrip Finished mencegah pencampuran sesi dan refleksi), Signal Protocol (pengikatan sesi melalui keadaan ratchet), dan Noise Protocol Framework (pengikatan identitas dalam pola jabat tangan). Serangan NS menunjukkan bahwa argumen keamanan informal tidak memadai—setiap protokol harus dianalisis terhadap lawan aktif yang mengendalikan jaringan dan dapat memutar ulang, mengurutkan ulang, serta mengubah pesan. Model lawan ini (Dolev-Yao) kini menjadi standar dalam verifikasi formal protokol.

Perubahan sederhana apa yang diusulkan Lowe untuk memperbaiki kerentanan protokol kunci publik NS?

Protokol simetris Needham-Schroeder (1978) memperkenalkan distribusi kunci sesi berbasis TTP. Serangan Denning-Sacco (1981) menemukan kerentanan pemutaran ulang—diperbaiki dengan stempel waktu dalam Kerberos. Protokol kunci publik NSPK mengalami serangan MITM yang ditemukan Lowe (1995) melalui pemeriksaan model—diperbaiki dengan menyertakan identitas pengirim dalam pesan. Serangan-serangan ini menetapkan verifikasi formal (Proverif, Tamarin) sebagai hal penting dalam rancangan protokol. Pelajaran utama: pesan harus mengikat identitas pengirim, sesi harus diisolasi satu sama lain, serangan refleksi dicegah melalui derivasi kunci terarah, dan serangan pencampuran sesi dicegah melalui MAC transkrip.