Needham-Schroeder Protokolü ve Saldırıları

Needham-Schroeder protokolü (1978), güvenilir bir üçüncü taraf (TTP) kullanarak kriptografik bir kimlik doğrulama protokolü tasarlamaya yönelik ilk biçimsel girişimlerden biriydi. Amaç, iki tarafın birbirlerinin kimliğini doğrulamasını ve her bir tarafla uzun süreli anahtarlar paylaşan güvenilir bir Kimlik Doğrulama Sunucusu (AS) kullanarak ortak bir oturum anahtarı oluşturmasını sağlamaktı. Protokol, açık anahtar altyapısından önce geliştirilmiş olsa da günümüzde Kerberos gibi protokollerin temelini oluşturan tazelik için tek kullanımlık değerler ve güvenilir sunucu aracılığıyla anahtar dağıtımı gibi kavramları ortaya koydu. NS'yi ve başarısızlıklarını anlamak, protokol analizi alanının tamamını şekillendirdi.

NS simetrik anahtar protokolü beş adımda işler. (1) Alice, Bob'la iletişim için bir oturum anahtarı talep ederek {A, B, Na} değerini AS'ye gönderir. (2) AS, Alice'e {Na, B, Kab, {Kab, A}_Kb}_Ka yanıtını gönderir; bu yanıtta bir oturum anahtarı olan Kab ve Bob için bir bilet bulunur ve tümü Alice'in uzun süreli anahtarı Ka ile şifrelenmiştir. (3) Alice, {Kab, A}_Kb biletini Bob'a iletir. (4) Bob bileti çözer, Kab'ı çıkarır ve bir sınama olarak {Nb}_Kab değerini Alice'e gönderir. (5) Alice, Kab'a sahip olduğunu kanıtlayarak {Nb-1}_Kab ile yanıt verir. Nb tek kullanımlık değeri, 4. adımın tekrar oynatılmasını önler. Bu protokolde, Denning ve Sacco'nun (1981) yararlandığı bilinen bir tekrar oynatma açığı vardır.

Denning ve Sacco (1981) bir kusur buldu: 2. adımdaki AS yanıtı yeni değildir; sunucu tarafından sağlanan bir zaman damgası veya tek kullanımlık değer içermez. Daha önce eski bir oturum anahtarı olan Kab'ı ele geçirmiş bir saldırgan olan Mallory, eski {Kab, A}_Kb biletini gelecekte herhangi bir zamanda Bob'a tekrar gönderebilir. Bob, Alice'ten geliyormuş gibi görünen meşru bir bilet aldığında, oturum için ele geçirilmiş Kab anahtarını kullanır. Denning ve Sacco'nun çözümü, AS yanıtına ve bilete bir zaman damgası eklemekti. Bu çözüm Kerberos'ta benimsendi; geçerlilik aralıklarını sınırlamak için zaman damgaları biletlere gömülür.

NS açık anahtar protokolü (yine 1978), açık anahtarlı kriptografi kullanarak iki taraf arasında karşılıklı kimlik doğrulama sağlamak amacıyla tasarlandı. (1) Alice, {Na, A}_PKb değerini Bob'a gönderir; Na tek kullanımlık değeri Bob'un açık anahtarıyla şifrelenmiştir. (2) Bob, {Na, Nb}_PKa değerini yanıt olarak gönderir; her iki tek kullanımlık değer de Alice'in açık anahtarıyla şifrelenmiştir. (3) Alice, Bob'un tek kullanımlık değerini onun açık anahtarıyla şifrelenmiş olarak {Nb}_PKb biçiminde geri gönderir. Bu alışverişten sonra her iki taraf da her iki tek kullanımlık değere (Na, Nb) sahip olur ve bir oturum anahtarı türetebilir. Protokol, Lowe'un 1995'teki saldırısına kadar 17 yıl boyunca güvenli göründü.

Gavin Lowe (1995), Bileşimsel Akıl Yürütmedeki Hatalar (FDR) model denetleyicisini kullanarak kritik bir kusur buldu. Mallory, mesajları dürüst Bob'a aktarırken Alice'e karşı Bob'un kimliğine bürünebilir. 1. adım: Alice, Bob'la konuştuğunu sanarak {Na, A}_PKm değerini Mallory'ye gönderir. Mallory, {Na, A}_PKb değerini Bob'a iletir. 2. adım: Bob, {Na, Nb}_PKa ile yanıt verir; Mallory bu yanıtı çözer ve Alice için yeniden şifreler: {Na, Nb}_PKa. Alice yanıtı çözer ve Nb'yi çıkarır. 3. adım: Alice, bunun Bob'a gittiğini sanarak {Nb}_PKm değerini gönderir. Mallory bunu çözer ve {Nb}_PKb değerini Bob'a iletir. Bob, Alice ile karşılıklı kimlik doğrulamayı tamamladığına inanır; oysa Alice aslında Mallory ile kimlik doğrulaması yapmaktadır. Çözüm şudur: 2. adımda Bob kendi kimliğini de eklemelidir: {Na, Nb, B}_PKa.

Lowe'un NSPK protokolü için çözümü basit ama derindir: 2. adımdaki Bob'un yanıtı, Bob'un kimliği B'yi içermeli ve {Na, Nb, B}_PKa biçiminde olmalıdır. Alice yanıtı aldığında, artık iletideki B kimliğinin iletişim kurmayı amaçladığı tarafla eşleştiğini denetler. Mallory kendi yanıtını yerine koyamaz — Alice'in denetiminden geçen geçerli bir {Na, Nb, M}_PKa oluşturmak için Mallory'nin Alice'in özel anahtarına ihtiyacı olur. Bu ilke, Needham-Abadi İlkesi olarak genellenir: kimlik doğrulama iletileri, gönderenin kimliğini açıkça bağlamalı; tanımlama için yalnızca bağlama güvenmemelidir.

Lowe'un NSPK'deki açığı keşfetmesine, tüm olası protokol yürütmelerini saldırgan müdahaleleri de dâhil olmak üzere kapsamlı biçimde inceleyen FDR (Başarısızlıklar-Ayrışmalar İyileştirmesi) model denetleyicisi yardımcı oldu. Bu durum, biçimsel protokol analizi araçlarının geliştirilmesini teşvik etti: Proverif (uygulamalı pi hesabını temel alır), sonsuz oturumlarda kimlik doğrulama ve gizlilik özelliklerini kanıtlayabilir veya çürütebilir. Tamarin Prover, çoklu-küme yeniden yazımını kullanır ve TLS 1.3 ile Signal gibi karmaşık protokolleri destekler. AVISPA ve Scyther de diğer araçlardır. Modern protokol tasarımları (TLS 1.3, Signal, Noise), kullanıma sunulmadan önce biçimsel doğrulamadan geçer — NS/Lowe olayının doğrudan mirası.

NS saldırıları, kimlik doğrulama hedefleri arasındaki ayrımı netleştirdi. Varlık kimlik doğrulaması: bir tarafın o anda canlı olduğunu ve protokole katıldığını kanıtlama (tazelik önemlidir). Veri kaynağı kimlik doğrulaması: belirli bir iletinin belirli bir tarafça oluşturulduğunu kanıtlama (canlılık anlamına gelmeyebilir). Lowe'un saldırısı varlık kimlik doğrulamasını tehlikeye atar — Alice Bob'la kimlik doğrulaması yaptığını sanır, ancak aslında Bob'a aktarma yapan Mallory ile kimlik doğrulaması yapmaktadır. Modern protokol belirtimleri hedefleri kesin biçimde ifade eder: "Alice, bu oturumun başlatıcısı olarak Bob'a karşı kimlik doğrulamasından geçmiştir." Belirsiz hedefler, gayriresmî incelemeden geçen ancak biçimsel analizde başarısız olan muğlak belirtimlere yol açar.

NS ile ilgili saldırıların bir başka sınıfı yansıtma saldırısıdır: Mallory, Alice'ten gelen iletileri Alice'e geri oynatır. Protokol simetrikse (her iki taraf da aynı anahtarı ve ileti biçimini kullanıyorsa), Alice kendi sorgusunu Bob'dan gelen geçerli bir yanıt olarak kabul edebilir. Savunma yöntemi, farklı anahtar yönleri kullanmak (her yön için ayrı şifreleme ve şifre çözme anahtarları) veya iletilerde rol göstergeleri bulundurmaktır (şifreleme yapan taraf, iletiye "Başlatan benim" ifadesini ekler). TLS gibi modern protokoller, yansıtmayı önlemek için HKDF'den türetilen anahtarlarda role özgü etiket dizeleri kullanır (istemci için "c e traffic", sunucu için "s hs traffic").

Araya girme saldırıları, kimlik doğrulamayı sahtelemek için birden çok eşzamanlı protokol oturumundan gelen iletileri birleştirir. Alice iki eşzamanlı oturum yürütüyorsa Mallory, her ikisinden gelen iletileri karıştırarak tutarlı görünen ancak geçersiz bir birleşik oturum oluşturup Mallory'nin kimliğini doğrulatabilir. Savunma yöntemi, oturum bağlamadır — her ileti, oturum bağlamına kriptografik olarak bağlanmalıdır (örneğin bir oturum ID'si içermeli veya her oturum için benzersiz bir anahtar kullanmalıdır). TLS, mevcut oturumun tam ileti dökümü üzerinde hesaplanan bir MAC olan Finished iletisi aracılığıyla araya girmeyi önler. Araya giren herhangi bir ileti dökümü değiştirir ve Finished değerini geçersiz kılar.

Needham-Schroeder protokolleri, Kerberos'un tasarımını (yeniden oynatmayı önleyen ve Denning-Sacco çözümünden alınan zaman damgaları), TLS'nin tasarımını (araya girmeyi ve yansıtmayı önleyen Finished ileti dökümü MAC'i), Signal Protokolü'nün tasarımını (anahtar zinciri durumu aracılığıyla oturum bağlama) ve Noise Protokol Çerçevesi'nin tasarımını (el sıkışma örüntülerinde kimlik bağlama) doğrudan etkiledi. NS saldırıları, gayriresmî güvenlik savlarının yetersiz olduğunu ortaya koydu — her protokol, ağı denetleyen ve iletileri yeniden oynatabilen, yeniden sıralayabilen ve değiştirebilen etkin bir saldırgana karşı analiz edilmelidir. Bu saldırgan modeli (Dolev-Yao), biçimsel protokol doğrulamasında artık standarttır.

Lowe, NS açık anahtarlı protokolündeki güvenlik açığını düzeltmek için hangi basit değişikliği önerdi?

Needham-Schroeder simetrik protokolü (1978), TTP tabanlı oturum anahtarı dağıtımını tanıttı. Denning-Sacco saldırısı (1981), yeniden oynatma açığını ortaya çıkardı — bu açık, Kerberos'ta zaman damgalarıyla düzeltildi. NSPK açık anahtarlı protokolünde, Lowe'un 1995'te model denetimiyle keşfettiği bir MITM saldırısı vardı — bu da iletilere gönderen kimliği eklenerek düzeltildi. Bu saldırılar, biçimsel doğrulamayı (Proverif, Tamarin) protokol tasarımı için zorunlu hâle getirdi. Temel dersler: iletiler gönderenin kimliğini bağlamalı, oturumlar birbirinden yalıtılmalı, yansıtma saldırıları yönlü anahtar türetmeyle önlenmeli ve araya girme saldırıları ileti dökümleri üzerindeki MAC kullanımıyla önlenmelidir.