Protokół Needhama-Schroedera i ataki

Protokół Needhama–Schroedera (1978) był jedną z pierwszych formalnych prób zaprojektowania kryptograficznego protokołu uwierzytelniania z użyciem zaufanej strony trzeciej (TTP). Jego celem było umożliwienie dwóm stronom wzajemnego uwierzytelnienia i ustanowienia wspólnego klucza sesyjnego za pośrednictwem zaufanego serwera uwierzytelniania (AS), który współdzieli z każdym podmiotem długoterminowy klucz. Protokół powstał przed infrastrukturą klucza publicznego, ale wprowadził koncepcje — nonce'y zapewniające świeżość oraz dystrybucję kluczy za pośrednictwem zaufanego serwera — które nadal stanowią podstawę nowoczesnych protokołów, takich jak Kerberos. Zrozumienie protokołu NS i jego błędów wpłynęło na całą dziedzinę analizy protokołów.

Symetryczny protokół klucza NS przebiega w pięciu krokach. (1) Alice wysyła do AS komunikat {A, B, Na}, żądając klucza sesyjnego do komunikacji z Bobem. (2) AS odpowiada Alicji komunikatem {Na, B, Kab, {Kab, A}_Kb}_Ka — zawierającym klucz sesyjny Kab i bilet dla Boba, przy czym całość jest zaszyfrowana długoterminowym kluczem Alicji Ka. (3) Alice przekazuje Bobowi bilet {Kab, A}_Kb. (4) Bob odszyfrowuje bilet, uzyskuje Kab i wysyła Alicji komunikat {Nb}_Kab (wyzwanie). (5) Alice odpowiada {Nb-1}_Kab, dowodząc, że posiada Kab. Nonce Nb zapobiega powtórzeniu kroku 4. Ten protokół jest podatny na znany atak powtórzeniowy opisany przez Denninga i Sacco (1981).

Denning i Sacco (1981) odkryli błąd: odpowiedź AS w kroku 2 nie zapewnia świeżości — nie zawiera znacznika czasu ani nonce'a wygenerowanego przez serwer. Atakujący Mallory, który wcześniej przechwycił stary klucz sesyjny Kab (po naruszeniu bezpieczeństwa wcześniejszej sesji), może w dowolnym późniejszym momencie ponownie wysłać stary bilet {Kab, A}_Kb do Boba. Bob, otrzymując bilet wyglądający na prawidłowy bilet od Alicji, używa do sesji przejętego klucza Kab. Poprawka zaproponowana przez Denninga i Sacco polegała na dodaniu znacznika czasu do odpowiedzi AS i biletu. Rozwiązanie to przyjęto w Kerberosie — znaczniki czasu są umieszczane w biletach, aby ograniczyć okres ich ważności.

Protokół klucza publicznego NS (również z 1978 roku) zaprojektowano do wzajemnego uwierzytelniania dwóch stron z użyciem kryptografii klucza publicznego. (1) Alice wysyła Bobowi komunikat {Na, A}_PKb (nonce Na zaszyfrowany kluczem publicznym Boba). (2) Bob odpowiada {Na, Nb}_PKa (oba nonce'y zaszyfrowane kluczem publicznym Alicji). (3) Alice odpowiada {Nb}_PKb (odsyłając nonce Boba zaszyfrowany jego kluczem publicznym). Po tej wymianie obie strony posiadają oba nonce'y (Na, Nb) i mogą wyprowadzić klucz sesyjny. Przez 17 lat protokół uznawano za bezpieczny — aż do ataku Lowe’a z 1995 roku.

Gavin Lowe (1995) odkrył krytyczny błąd, korzystając z weryfikatora modeli Failures in Compositional Reasoning (FDR). Mallory może podszyć się pod Boba wobec Alicji, przekazując wiadomości uczciwemu Bobowi. Krok 1: Alice wysyła do Mallory komunikat {Na, A}_PKm, sądząc, że rozmawia z Bobem. Mallory przekazuje do Boba komunikat {Na, A}_PKb. Krok 2: Bob odpowiada {Na, Nb}_PKa, a Mallory odszyfrowuje go i ponownie szyfruje dla Alicji: {Na, Nb}_PKa. Alice odszyfrowuje komunikat i uzyskuje Nb. Krok 3: Alice wysyła {Nb}_PKm, sądząc, że komunikat trafi do Boba. Mallory odszyfrowuje go i przekazuje Bobowi jako {Nb}_PKb. Bob sądzi, że zakończył wzajemne uwierzytelnianie z Alicją — jednak Alice w rzeczywistości uwierzytelnia się z Mallory. Poprawka polega na tym, że w kroku 2 Bob musi dołączyć własną tożsamość: {Na, Nb, B}_PKa.

Poprawka Lowe’a do protokołu NSPK jest prosta, ale ma fundamentalne znaczenie: odpowiedź Boba w kroku 2 musi zawierać tożsamość Boba B, dzięki czemu ma postać {Na, Nb, B}_PKa. Gdy Alicja odbiera odpowiedź, sprawdza, czy zawarta w niej tożsamość B odpowiada stronie, z którą zamierzała się skontaktować. Mallory nie może podstawić własnej odpowiedzi — musiałby znać klucz prywatny Alicji, aby skonstruować poprawny komunikat {Na, Nb, M}_PKa przechodzący weryfikację Alicji. Lekcja ta jest uogólniana jako zasada Needhama-Abadiego: komunikaty uwierzytelniające muszą jawnie wiązać tożsamość nadawcy, a nie polegać wyłącznie na kontekście w celu jego identyfikacji.

Odkrycie luki w NSPK przez Lowe’a było możliwe między innymi dzięki weryfikatorowi modeli FDR (Failures-Divergences Refinement), który wyczerpująco analizuje wszystkie możliwe wykonania protokołu, w tym ingerencje przeciwnika. Przyczyniło się to do rozwoju formalnych narzędzi analizy protokołów: Proverif, oparty na rachunku pi, pozwala dowodzić lub obalać własności uwierzytelniania i poufności w nieskończonej liczbie sesji. Tamarin Prover wykorzystuje przepisywanie multizbiorów i obsługuje złożone protokoły, takie jak TLS 1.3 i Signal. Innymi narzędziami są AVISPA i Scyther. Współczesne projekty protokołów, takie jak TLS 1.3, Signal i Noise, przechodzą formalną weryfikację przed wdrożeniem — jest to bezpośrednie dziedzictwo wydarzeń związanych z NS i Lowe’em.

Ataki na NS doprecyzowały różnicę między celami uwierzytelniania. Uwierzytelnianie podmiotu polega na wykazaniu, że dana strona jest obecnie aktywna i uczestniczy w protokole (istotna jest świeżość). Uwierzytelnianie pochodzenia danych polega na wykazaniu, że konkretny komunikat został utworzony przez określoną stronę (nie musi to oznaczać jej aktywnego udziału). Atak Lowe’a narusza uwierzytelnianie podmiotu — Alicja sądzi, że uwierzytelnia się z Bobem, ale w rzeczywistości uwierzytelnia się z Mallorym, który przekazuje komunikaty Bobowi. Współczesne specyfikacje protokołów precyzyjnie określają cele: "Alicja jest uwierzytelniona względem Boba jako inicjatorka tej sesji". Nieprecyzyjne cele prowadzą do niejednoznacznych specyfikacji, które przechodzą nieformalny przegląd, ale zawodzą w formalnej analizie.

Inną klasą ataków związanych z NS są ataki odbicia: Mallory ponownie wysyła komunikaty Alicji do Alicji. Jeśli protokół jest symetryczny (obie strony używają tego samego klucza i formatu komunikatów), Alicja może zaakceptować własne wyzwanie jako poprawną odpowiedź od Boba. Obrona polega na użyciu różnych kierunków kluczy (oddzielnych kluczy szyfrowania i deszyfrowania dla każdego kierunku) albo na dołączaniu do komunikatów oznaczeń ról (szyfrujący dołącza do komunikatu "I am initiator"). Współczesne protokoły, takie jak TLS, zawierają etykiety zależne od roli w kluczach wyprowadzanych za pomocą HKDF (z użyciem "c e traffic" dla klienta i "s hs traffic" dla serwera), aby zapobiegać odbiciu.

Ataki przeplatania łączą komunikaty z wielu równoczesnych sesji protokołu w celu sfałszowania uwierzytelniania. Jeśli Alicja prowadzi dwie jednoczesne sesje, Mallory może mieszać komunikaty z obu z nich, tworząc spójną, lecz nieprawidłową połączoną sesję, w której uwierzytelniony zostaje Mallory. Obrona polega na wiązaniu z sesją — każdy komunikat musi być kryptograficznie powiązany z kontekstem swojej sesji (na przykład zawierać identyfikator sesji albo korzystać z unikatowego klucza dla każdej sesji). TLS zapobiega przeplataniu za pomocą komunikatu Finished, który jest kodem MAC obliczonym dla pełnego transkryptu bieżącej sesji. Każdy przepleciony komunikat zmienia transkrypt, unieważniając wartość Finished.

Protokoły Needhama-Schroedera bezpośrednio wpłynęły na projekt Kerberos (znaczniki czasu zapobiegające powtórzeniom, zaczerpnięte z poprawki Denninga-Sacco), TLS (kod MAC transkryptu w komunikacie Finished zapobiega przeplataniu i odbiciu), Signal Protocol (wiązanie z sesją za pomocą stanu ratchet) oraz Noise Protocol Framework (wiązanie tożsamości we wzorcach uzgadniania). Ataki na NS wykazały, że nieformalne argumenty dotyczące bezpieczeństwa są niewystarczające — każdy protokół należy analizować pod kątem aktywnego przeciwnika, który kontroluje sieć i może ponownie odtwarzać, zmieniać kolejność oraz modyfikować komunikaty. Taki model przeciwnika (Dolev-Yao) jest obecnie standardem w formalnej weryfikacji protokołów.

Jaką prostą zmianę zaproponował Lowe, aby naprawić lukę w protokole klucza publicznego NS?

Protokół symetryczny Needhama-Schroedera (1978) wprowadził dystrybucję kluczy sesyjnych opartą na TTP. Atak Denninga-Sacco (1981) ujawnił podatność na atak powtórzeniowy — naprawiono ją za pomocą znaczników czasu w Kerberosie. Publicznokluczowy protokół NSPK był podatny na atak MITM odkryty przez Lowe’a (1995) za pomocą sprawdzania modelu — naprawiono go przez uwzględnienie tożsamości nadawcy w komunikatach. Ataki te ustanowiły formalną weryfikację (Proverif, Tamarin) jako niezbędny element projektowania protokołów. Najważniejsze wnioski: komunikaty muszą wiązać tożsamość nadawcy, sesje muszą być od siebie odizolowane, atakom odbicia zapobiega się przez kierunkowe wyprowadzanie kluczy, a atakom przeplatania — przez kody MAC transkryptu.