9.01.2003

Weryfikacja protokołów uwierzytelniania metodą indukcji odwrotnej

W badaniach nad poprawnoscia protokolow uwierzytelniania stron istotna role odgrywaja metody oparte na weryfikacji modelowej (ang. model checking). Polegaja one na konstruowaniu odpowiednich przestrzeni stanow osiagalnych opisujacych rzeczywistosc uwierzytelniania (wykonywania odpowiednich protokolow) w rzeczywistych sieciach komputerowych. Przeszukiwanie tych struktur umozliwia badanie, czy istnieje mozliwosc symulacji takiego wykonania (lub przeplotu wielu wykonan) protokolu, w wyniku ktorego cel protokolu nie zostaje zrealizowany.

W referacie przedstawiona zostanie metoda badania wlasnosci protokolow uwierzytelniania stron bedaca pewnym rodzajem weryfikacji modelowej. Podane zostana motywacje i konstrukcja modelu matematycznego przestrzeni stanow osiagalnych opisujacych wykonania protokolow w rzeczywistych sieciach komputerowych. W rozwazaniach zostanie wykorzystana redukcja czesciowo porzadkowa przestrzeni stanow. W skonstruowanym formalizmie podamy warunki poprawnosci protokolow uwierzytelniania stron. Podczas weryfikacji tych warunkow poslugiwac sie bedziemy metoda wnioskowania nie wprost. Do przeszukiwania skonstruowanego drzewa wykonan protokolu zastosujemy metode indukcji odwrotnej (ang. backward induction). Omowione zostanie zastosowanie metody do automatycznej weryfikacji wlasnosci protokolow. Przedstawiony zostanie algorytm i jego implementacja, a takze wyniki eksperymentalne dla kilku znanych z literatury protokolow.