Protokol Needham-Schroeder dan Serangan

Protokol Needham-Schroeder (1978) merupakan salah satu usaha formal terawal untuk mereka bentuk protokol pengesahan kriptografi menggunakan pihak ketiga yang dipercayai (TTP). Matlamatnya adalah untuk membolehkan dua pihak, Alice dan Bob, mengesahkan identiti satu sama lain serta mewujudkan kunci sesi yang dikongsi menggunakan Pelayan Pengesahan (AS) yang dipercayai, yang berkongsi kunci jangka panjang dengan setiap entiti. Protokol ini wujud sebelum infrastruktur kunci awam, tetapi memperkenalkan konsep seperti nilai sekali guna untuk memastikan kesegaran dan pengedaran kunci melalui pelayan yang dipercayai, yang kekal penting dalam protokol moden seperti Kerberos. Pemahaman terhadap NS dan kegagalannya membentuk keseluruhan bidang analisis protokol.

Protokol kunci simetri NS terdiri daripada lima langkah. (1) Alice menghantar {A, B, Na} kepada AS untuk meminta kunci sesi bagi komunikasi dengan Bob. (2) AS membalas Alice dengan {Na, B, Kab, {Kab, A}_Kb}_Ka — kunci sesi Kab, tiket untuk Bob, semuanya disulitkan menggunakan kunci jangka panjang Alice, Ka. (3) Alice memajukan tiket {Kab, A}_Kb kepada Bob. (4) Bob menyahsulit tiket tersebut, mendapatkan Kab dan menghantar {Nb}_Kab kepada Alice sebagai cabaran. (5) Alice membalas dengan {Nb-1}_Kab untuk membuktikan bahawa beliau memegang Kab. Nilai sekali guna Nb menghalang ulangan langkah 4. Protokol ini terdedah kepada serangan ulangan yang dieksploitasi oleh Denning dan Sacco (1981).

Denning dan Sacco (1981) menemukan kelemahan: respons AS dalam langkah 2 tidak menjamin kesegaran — respons itu tidak mengandungi cap masa atau nilai sekali guna yang disumbangkan oleh pelayan. Penyerang Mallory yang sebelum ini memintas kunci sesi lama Kab (dengan menjejaskan keselamatan sesi terdahulu) boleh mengulang tiket lama {Kab, A}_Kb kepada Bob pada bila-bila masa akan datang. Apabila menerima sesuatu yang kelihatan seperti tiket sah daripada Alice, Bob menggunakan kunci Kab yang telah terjejas untuk sesi tersebut. Penyelesaian Denning dan Sacco adalah dengan menambahkan cap masa pada respons AS dan tiket. Pendekatan ini diterapkan dalam Kerberos — cap masa disematkan dalam tiket untuk mengehadkan tempoh sahnya.

Protokol kunci awam NS, yang turut diperkenalkan pada 1978, direka untuk pengesahan bersama dua pihak menggunakan kriptografi kunci awam. (1) Alice menghantar {Na, A}_PKb kepada Bob (nilai sekali guna Na yang disulitkan menggunakan kunci awam Bob). (2) Bob membalas dengan {Na, Nb}_PKa (kedua-dua nilai sekali guna, disulitkan menggunakan kunci awam Alice). (3) Alice membalas dengan {Nb}_PKb (mengembalikan nilai sekali guna Bob yang disulitkan menggunakan kunci awamnya). Selepas pertukaran ini, kedua-dua pihak memiliki kedua-dua nilai sekali guna (Na, Nb) dan boleh menghasilkan kunci sesi. Protokol ini kelihatan selamat selama 17 tahun — sehingga serangan Lowe pada 1995.

Gavin Lowe (1995) menemukan kelemahan kritikal menggunakan pemeriksa model FDR. Mallory boleh menyamar sebagai Bob kepada Alice sambil menyampaikan semula mesej kepada Bob yang jujur. Langkah 1: Alice menghantar {Na, A}_PKm kepada Mallory kerana menyangka beliau sedang bercakap dengan Bob. Mallory memajukan {Na, A}_PKb kepada Bob. Langkah 2: Bob membalas dengan {Na, Nb}_PKa, yang dinyahsulitkan oleh Mallory dan disulitkan semula untuk Alice: {Na, Nb}_PKa. Alice menyahsulitkannya lalu mendapatkan Nb. Langkah 3: Alice menghantar {Nb}_PKm kerana menyangka mesej itu dihantar kepada Bob. Mallory menyahsulitkannya dan memajukan {Nb}_PKb kepada Bob. Bob percaya bahawa beliau telah melengkapkan pengesahan bersama Alice — tetapi Alice sebenarnya mengesahkan identiti Mallory. Penyelesaiannya: dalam langkah 2, Bob mesti menyertakan identitinya sendiri: {Na, Nb, B}_PKa.

Pembaikan Lowe terhadap protokol NSPK adalah mudah tetapi mendalam: respons Bob pada langkah 2 mesti menyertakan identiti Bob, B, lalu menjadikannya {Na, Nb, B}_PKa. Kini apabila Alice menerima respons itu, dia memeriksa bahawa identiti B yang disertakan sepadan dengan pihak yang ingin dihubunginya. Mallory tidak boleh menggantikan responsnya — Mallory memerlukan kunci peribadi Alice untuk membina {Na, Nb, M}_PKa yang sah dan melepasi pemeriksaan Alice. Pelajaran ini digeneralisasikan sebagai Prinsip Needham-Abadi: mesej pengesahan mesti mengikat identiti pengirim secara jelas, bukan bergantung pada konteks semata-mata untuk mengenal pasti pengirim.

Penemuan Lowe tentang kecacatan NSPK dibantu oleh penyemak model FDR (Penambahbaikan Kegagalan-Penyimpangan), yang meneroka secara menyeluruh semua pelaksanaan protokol yang mungkin, termasuk campur tangan pihak lawan. Hal ini mendorong pembangunan alat analisis protokol formal: Proverif, yang berasaskan kalkulus pi gunaan, boleh membuktikan atau menyangkal sifat pengesahan dan kerahsiaan dalam sesi tanpa had. Tamarin Prover menggunakan penulisan semula multiset dan menyokong protokol kompleks seperti TLS 1.3 dan Signal. AVISPA dan Scyther ialah alat lain. Reka bentuk protokol moden seperti TLS 1.3, Signal dan Noise menjalani pengesahan formal sebelum digunakan — warisan langsung daripada peristiwa NS/Lowe.

Serangan NS menjelaskan perbezaan antara matlamat pengesahan. Pengesahan entiti: membuktikan bahawa sesuatu pihak sedang aktif dan mengambil bahagian dalam protokol (kebaruan adalah penting). Pengesahan asal data: membuktikan bahawa mesej tertentu dicipta oleh pihak tertentu (mungkin tidak membuktikan keaktifan). Serangan Lowe menjejaskan pengesahan entiti — Alice menyangka dia sedang mengesahkan Bob, tetapi sebenarnya dia sedang mengesahkan Mallory, yang menyampaikan semula mesej kepada Bob. Spesifikasi protokol moden menyatakan matlamat dengan tepat: "Alice disahkan kepada Bob sebagai pemula sesi ini." Matlamat yang kabur membawa kepada spesifikasi yang samar, yang lulus semakan tidak formal tetapi gagal dalam analisis formal.

Satu lagi kelas serangan berkaitan NS ialah serangan pantulan: Mallory memainkan semula mesej daripada Alice kepada Alice. Jika protokol itu simetri (kedua-dua pihak menggunakan kunci dan format mesej yang sama), Alice mungkin menerima cabarannya sendiri sebagai respons yang sah daripada Bob. Pertahanan: gunakan arah kunci yang berbeza (kunci penyulitan dan penyahsulitan yang berasingan bagi setiap arah) atau sertakan penunjuk peranan dalam mesej (pihak penyulit menyertakan "Saya ialah pemula" dalam mesej). Protokol moden seperti TLS menyertakan rentetan label khusus peranan dalam kunci terbitan HKDF (menggunakan "c e traffic" untuk pelanggan dan "s hs traffic" untuk pelayan) bagi mencegah pantulan.

Serangan penyelangan menggabungkan mesej daripada beberapa sesi protokol serentak untuk memalsukan pengesahan. Jika Alice menjalankan dua sesi pada masa yang sama, Mallory mungkin mencampurkan mesej daripada kedua-duanya untuk menghasilkan sesi gabungan yang konsisten tetapi tidak sah, lalu mengesahkan Mallory. Pertahanan: pengikatan sesi — setiap mesej mesti terikat secara kriptografi pada konteks sesinya (contohnya, menyertakan ID sesi atau menggunakan kunci unik bagi setiap sesi). TLS mencegah penyelangan melalui mesej Finished, yang merupakan MAC terhadap keseluruhan transkrip sesi semasa. Sebarang mesej yang diselangkan akan mengubah transkrip dan menyebabkan nilai Finished tidak sah.

Protokol Needham-Schroeder mempengaruhi secara langsung reka bentuk Kerberos (cap masa untuk mencegah pengulangan, yang dipinjam daripada pembaikan Denning-Sacco), TLS (MAC transkrip Finished mencegah penyelangan dan pantulan), Signal Protocol (pengikatan sesi melalui keadaan ratchet), serta Noise Protocol Framework (pengikatan identiti dalam corak jabat tangan). Serangan NS membuktikan bahawa hujah keselamatan tidak formal tidak mencukupi — setiap protokol mesti dianalisis terhadap pihak lawan aktif yang mengawal rangkaian serta boleh memainkan semula, menyusun semula dan mengubah mesej. Model pihak lawan ini (Dolev-Yao) kini menjadi standard dalam pengesahan protokol formal.

Protokol simetri Needham-Schroeder (1978) memperkenalkan pengagihan kunci sesi berasaskan TTP. Serangan Denning-Sacco (1981) menemui kelemahan pengulangan — yang dibaiki dengan cap masa dalam Kerberos. Protokol kunci awam NSPK mengalami serangan MITM yang ditemui oleh Lowe (1995) melalui pemeriksaan model — yang dibaiki dengan menyertakan identiti pengirim dalam mesej. Serangan ini menjadikan pengesahan formal (Proverif, Tamarin) penting untuk reka bentuk protokol. Pengajaran utama: mesej mesti mengikat identiti pengirim, sesi mesti diasingkan antara satu sama lain, serangan pantulan dicegah melalui penerbitan kunci berarah, dan serangan penyelangan dicegah melalui MAC transkrip.