Weryfikacja bezpieczeństwa kryptograficznych protokołów komunikacyjnych przy pomocy SPINA

Wprowadzenie

Wszystkie rozwiązania mające zapewnić bezpieczeństwo w rozproszonych systemach są oparte na jakimś rodzaju protokołu kryptograficznego, używającego podstawowych operacji kryptograficznych takich jak kodowanie i podpisy cyfrowe. Mimo, że operacje te nie są bardzo skomplikowane, to jednak są źródłem wielu błędów i zagrożeń. Głównym powodem tego jest fakt, że bardzo trudno przewidzieć wszystkie możliwe formy ataku. Dlatego prowadzone są prace nad formalnymi metodami weryfikacji i analizy własności protokołów.

Rozważano metody oparte zarówno na dowodzeniu teoretycznym własności, jak i na analizie własności modeli protokołów. Niektórzy badacze zajmujący się analizą modeli stworzyli narzędzia, które służą właśnie temu celowi, takie jak FDR i Murphi. Jednak my zajmiemy się poźniejszym podejściem i zobaczymy jak można wykorzystać uniwersalne narzędzie jakim jest Spin do analizy i weryfikacji protokołów kryptograficznych. Zamiast przenosić podejście z wyspecjalizowanych narzędzi spróbujemy dokonać własnej statycznej analizy sytuacji aby otrzymać jak najprostszy model. Głównym pomysłem na oszczędności jest rozbiór przepływu danych w protokole, co może prowadzić do uproszczenia reprezentacji wiedzy jaką może posiąść intruz. Na przykład możemy zaoszczędzić unikając reprezentowania wiedzy, której on nigdy nie zdobędzie. Podobnie możemy wyeliminować komunikaty, które wygenerowane przez intruza, nigdy nie zostaną zaakceptowane przez żadnego z agentów.

Protokół Needhama-Schroedera

Protokół Needhama-Schroedera jest dobrze znaną, opartą na na kluczu publicznym i prywatnym, metodą autoryzacji, która powstała w roku 1978. Jego celem jest ustanowienie wzajemnej autoryzacji między inicjatorem A a odbiorcą B, po której może nastąpić sesja, podczas której A i B będą wymieniać wiadomości.

Tak jak sugeruje nazwa protokół używa klucza publicznego, każdy agent H posiada klucz publiczny oznaczany jako PK(H) i klucz prywatny SK(H), który może zostać użyty do rozszyfrowania wiadomości zakodowanych przy pomocy PK(H). Podczas gdy SK(H) powinien być znany tylko H, każdy inny agent może pozyskać PK(H) z serwera kluczy. Każdy agent może zaszyfrować wiadomość x używając klucza publicznego H aby uzyskać zakodowaną wiadomość {x}PK(H). Tylko agent znający klucz prywatny H może zdekodować tą wiadomość otrzymując x. Ta własność powinna zapewnić bezpieczeństwo x. Jednocześnie każdy agent H może podpisać wiadomość x kodując ją przy pomocy swojego klucza prywatnego do {x}SK(H) aby zapewnić integralność x. Każdy agent może rozszyfrować {x}SK(H) używając klucza publicznego H.

Kompletny przebieg protokołu wymaga 7 kroków:

Każdorazowo rozpoczynany jest przez A, który prosi zaufany serwer kluczy S o klucz publiczny B (1). S wysyła podpisaną wiadomość zawierającą klucz publiczny PK(B) i identyfikator B (2). Jeżeli S jest godny zaufania to powinno to zapewnić, że A, że posiada prawdziwy PK(B). Kiedy ma już klucz publiczny B wybiera przypadkowo wygenerowany znacznik Na i wysyła wiadomość (3) do B. Wiadomość ta może zostać zdekodowana tylko przez B ponieważ została zaszyfrowana przy pomocy jego klucza publicznego i oznacza, że ktoś, prawdopodobnie A chce dokonać autoryzacji z B. Po otrzymaniu wiadomości B rozszyfrowuje ją przy pomocy swojego klucza prywatnego aby otrzymać znacznik Na i prosi serwer S o klucz publiczny A (4 i 5). Następnie B wysyła znacznik Na do A razem z nowym znacznikiem Nb zaszyfrowane przy pomocy klucza publicznego A (6). Aby zakończyć przebieg protokołu A zwraca znacznik Nb aby dokonać autoryzacji siebie u B (7).

Łatwo zauważyć, że cztery z siedmiu kroków mogą zostać wyeliminowane, jeśli przyjmiemy, że A i B znają swoje klucze publiczne. Kroki 1, 2, 4 i 5 służą właśnie pozyskaniu kluczy publicznych, podczas, gdy prawdziwa autoryzacja odbywa się w krokach 3, 6 i 7. Przyjmiemy, że agenci znają wzajemnie swoje klucze publiczne i skupimy się na protokole o mniejszej ilości kroków:

Modelowanie kryptograficznych protokołów w PROMELI

Formalne modele protokołów kryptograficznych składają się zwykle z zestawu składowych wysyłających do siebie wzajemnie wiadomości i intruza, który reprezentuje działalność wszystkich potencjalnych atakujących. Ponieważ takie modele mają sprawdzić działanie protokołów, a nie systemów szyfrujących i deszyfrujących przyjmujemy, że takie systemy są idealne, czyli:

jedyną metodą rozkodowania zaszyfrowanej wiadomości jest znajomość odpowiedniego klucza;
zaszyfrowana wiadomość nie zdradza przy użyciu którego klucza została zakodowana;
istnieje możliwość sprawdzenia przez algorytm rozszyfrowujący, czy wiadomość została zakodowana przy użyciu odpowiedniego klucza.

Założenia te nie są całkowicie prawdziwe dla rzeczywistych systemów kryptograficznych, ale pozwalają rozróżnić defekty samych systemów od wad protokołów, co jednak powoduje, że samo sprawdzenie systemu tą metodą może okazać się niewystarczające.

Komunikacja

Zarówno składowe jak i intruz są reprezentowane w naszym modelu jako Promelowe procesy, które komunikują się między sobą przez współdzielone kanały. Dokładniej mówiąc, mamy osobne procesy dla każdej roli w protokole i jeden proces intruza. Zaczynamy więc od zestawu nazw, z których pierwsze trzy to identyfikatory stron i intruza:

mtype = {A, B, I, Na, Nb, gD, R};

Składowe nie komunikują się między sobą bezpośrednio, ale wszystkie wiadomości są przechwytywane przez intruza i ewentualnie przesyłane dalej do adresata. To podejście pozwala uniknąć redundantnych przeplotów wykonania.

chan ca = [0] of {mtype, mtype, mtype, mtype};
chan cb = [0] of {mtype, mtype, mtype};

W naszym modelu będziemy przesyłać wiadomości dwóch rodzajów: {a, b}PK(c), które będziemy transportować przez ca i {a}PK(b) przez cb. Aby wysłać wiadomość {Na, A}PK(B) musimy wykonać następujące polecenie:

ca ! A, Na, A, B

Gdzie pierwsze A identyfikuje odbiorcę lub nadawcę, natomiast pozostałe trzy są treścią przesyłanej wiadomości. B oznacza, ona zaszyfrowana przy pomocy PK(B). Podobnie wyrażamy przyjmowanie komunikatów. Na przykład, żeby zapisać fakt, że A musi otrzymać wiadomość typu {x1,x2}PK(x3), gdzie x1 = Na i x3 = A napiszemy:

ca ? eval(A), eval(Na), x2, eval(A);

Gdzie x1 to zmienna lokalna. Generalnie wszystkie wiadomości wysyłane przez intruza mają na pierwszym miejscu adresata, co odpowiada sytuacji, że normalny użytkownik siecie sprawdza czy przesyłka była zaadresowana do niego. Natomiast wszystkie komunikaty wysyłane przez strony protokołu mają na pierwszym miejscu nadawcę wiadomości, bo i tak odbiera je intruz, a unikamy w ten sposób bezpośredniego przesyłania sobie komunikatów i nie musimy tworzyć dodatkowych kanałów.

Strony protokołu

Zaczniemy od strony inicjującej protokół. Jego definicja to sekwencja działań jakie ma wykonywać w przebiegu protokołu zapisana w Promeli, należy jeszcze pamiętać o warunkach, które przydadzą się przy weryfikowaniu właściwości bezpieczeństwa protokołu. W naszym wypadku będzie wyglądać to tak:

proctype PIni (mtype self; mtype party; mtype nonce)
{
  mtype g1;

	atomic {
	       IniRunning(self, party);
	       ca ! self, nonce, self, party;
	}

	atomic {
	       ca ? eval (self), eval (nonce), g1, eval(self);
	       IniCommit(self, party);
	       cb ! self, g1, party;
	}
}

Parametr self identyfikuje nazwę inicjującego proces, a party jego partnera. Nonce to znacznik, którego inicjujący będzie używał podczas przebiegu protokołu. Atomowe sekwencje zostały użyte aby zmniejszyć liczbę przeplotów.

Makra IniRunnin i IniCommit służą do zmian zmiennych globalnych, które służą do weryfikacji bezpieczeństwa protokołu:

#define IniRunning(x, y) if \
			 :: ((x == A) && (y == B)) -> IniRunningAB = 1 \
			 :: else skip \
			 fi

#define IniCommit(x, y) if \
			:: ((x == A) && (y == B)) -> IniCommitAB = 1 \
			:: else skip \
			fi

Mamy cztery takie zmienne:

bit IniRunningAB = 0; /* Zainicjowany protokół po stronie inicjatora */
bit IniCommitAB = 0;  /* Zatwierdzony protokół po stronie inicjatora */
bit ResRunningAB = 0; /* Zainicjowany protokół po stronie odbiorcy */
bit ResCommitAB = 0;  /* Zatwierdzony protokół po stronie odbiorcy */

Bezpieczeństwo może zostać wyrażone w postaci dwóch formuł LTL:

[] (([] !IniCommitAB) || (!IniCommitAB U ResRunningAB))
[] (([] !ResCommitAB) || (!ResCommitAB U IniRunningAB))

Odbiorcę definiujemy analogicznie:

proctype PRes(mtype self; mtype nonce)
{

	mtype g2, g3;
	
	atomic {
	       ca ? eval (self), g2, g3, eval (self);
	       ResRunning(g3, self);

	       ca ! self, g2, nonce, g3;
	}

	atomic {
	       cb ? eval (self), eval (nonce), eval (self);
	       ResCommit(g3, self);
	}
}

I dwa brakujące makra:

#define ResRunning(x, y) if \
			 :: ((x == A) && (y == B)) -> ResRunningAB = 1 \
			 :: else skip \
			 fi

#define ResCommit(x, y) if \
			:: ((x == A) && (y == B)) -> ResCommitAB = 1 \
			:: else skip \
			fi

Intruz

Intruz może wykonywać wszystkie czynności, jakich się spodziewamy po atakującym. Oto długa lista wiadomości rozsyłanych przez naszego intruza z przykładu:

:: ca ! B, gD, A, B
:: ca ! B, gD, B, B
:: ca ! B, gD, I, B
:: ca ! B, A, A, B
:: ca ! B, A, B, B
:: ca ! B, A, I, B
:: ca ! B, B, A, B
:: ca ! B, B, B, B
:: ca ! B, B, I, B
:: ca ! B, I, A, B
:: ca ! B, I, B, B
:: ca ! B, I, I, B

Jednak w tym samym czasie może się zachowywać jak normalny użytkownik sieci. Z tego powodu możliwe jest, że któryś z normalnych użytkowników rozpocznie przebieg protokołu właśnie z intruzem.

if
:: run PIni (A, I, Na)
:: run PIni (A, B, Na)
fi;

W każdej chwili zachowanie intruza zależy od wiedzy ją posiadł. Przed rozpoczęciem przebiegu protokołu zakładamy, że intruz zna tylko dany mu przez nas zestaw wiedzy. Przykładowo taki zestaw może zwierać: identyfikator intruza, jego klucz publiczny i prywatny, identyfikatory pozostałych biorących udział w przebiegu, ich klucze publiczne, jeśli współdzieli on jakieś klucze prywatne ze stronami w protokole to również powinien je znać.

/* Intruz zna A, B, I PK(A), PK(B), PK(I), SK(I) i gD */
bit kNa = 0;		     /* czy zna Na */
bit kNb = 0;		     /* czy zna Nb */
bit k_Na_Nb__A = 0;	     /* czy zna {Na, Nb}{PK(A)} */
bit k_Na_A__B = 0;	     /* czy zna {Na, A}{PK(B)} */
bit k_Nb__B = 0;	     /* czy zna {Nb}{PK(B)} */

Za każdym razem, gdy intruz przechwytuje wiadomość, może powiększyć zestaw swojej wiedzy.

:: d_step {
     ca ? _, x1, x2, x3;      
     if
     :: (x3 == I) -> k(x1);k(x2)
     :: else k3(x1, x2, x3)
     fi;
     x1 = 0;
     x2 = 0;
     x3 = 0;
   }
:: d_step {
     cb ? _, x1, x2;	      
     if
     :: (x2 == I) -> k(x1)
     :: else k2(x1, x2)
     fi;
     x1 = 0;
     x2 = 0;
   }

Samo pozyskiwanie wiedzy ukryte jest w makrach:

#define k(x1)	if \
		:: (x1 == Na) -> kNa = 1 \
		:: (x1 == Nb) -> kNb = 1 \
		:: else skip \
		fi;

#define k2(x1, x2)      if \
			:: (x1 == Nb && x2 == B) -> k_Nb__B = 1 \
			:: else skip \
			fi

#define k3(x1, x2, x3)	if \
			:: (x1 == Na && x2 == A && x3 == B) \
			       -> k_Na_A__B = 1 \
			:: (x1 == Na && x2 == Nb && x3 == A) \
			       -> k_Na_Nb__A = 1 \
			:: else skip \
			fi

Wiadomości i pozyskiwaną z nich wiedzę można przedstawić tabelą:

Następnie intruz może swoją wiedzę wykorzystać:

:: ca ! (kNa -> A : R), Na, Na, A
:: ca ! (((kNa && kNb) || k_Na_Nb__A) -> A : R), Na, Nb, A
:: ca ! (kNa -> A : R), Na, gD, A
:: ca ! (kNa -> A : R), Na, A, A
:: ca ! (kNa -> A : R), Na, B, A
:: ca ! (kNa -> A : R), Na, I, A
:: ca ! ((kNa || k_Na_A__B) -> B : R), Na, A, B
:: ca ! (kNa -> B : R), Na, B, B
:: ca ! (kNa -> B : R), Na, I, B
:: ca ! (kNb -> B : R), Nb, A, B
:: ca ! (kNb -> B : R), Nb, B, B
:: ca ! (kNb -> B : R), Nb, I, B
:: cb ! ((k_Nb__B || kNb) -> B : R), Nb, B

Weryfikacja

Spin znajduje niebezpieczną sytuację w modelu, na niewielkiej głębokości:

Sztuczka polega na tym, że intruz nie próbuje złamać ani poznać kluczy prywatnych stron protokołu, a jedynie sprytnie wymieniając wiadomości poszywa się pod biorących udział w przebiegu i uzyskuje Na i Nb i B myśli że ma zaautoryzowaną sesję z A.

Poprawki w protokole

W ramach eksperymentów poprawiłem protokół. Poprawka polega na dodaniu w drugim kroku do wiadomości identyfikatora nadającego. Wysyłany jest komunikat {Na, Nb, B}PK(A) i intruz nie jest w stanie podmienić identyfikatora B na I bez rozszyfrowywania wiadomości, a tego nie jest w stanie zrobić. Spin nie znajduje już niebezpieczeństw, jednak może się okazać, że jest to wynikiem mojego przeoczenia (trzeba przewidzieć jakie wiadomości może umieścić teraz intruz w cztero-miejcowym kanale). Na pewno model który, zapisałem jest w stanie przeprowadzić poprawną autoryzację stron protokołu:

Źródła

Autor: Piotrek Witusowski