Model atakującego Dolev–Yao i kryptografia symboliczna

Zaproponowany przez Danny'ego Doleva i Andrew Yao w 1983 roku model Doleva-Yao jest standardowym modelem przeciwnika stosowanym w symbolicznej analizie protokołów. Atakujący kontroluje całą sieć.

Atakujący w modelu Doleva-Yao może: przechwytywać dowolne wiadomości, przechowywać wiadomości, ponownie odtwarzać stare wiadomości, fałszować nowe wiadomości na podstawie znanych elementów, ale nie może łamać bazowych prymitywów kryptograficznych.

W modelach symbolicznych szyfrowanie jest idealną czarną skrzynką: atakujący nie może odszyfrować danych bez klucza, rozłożyć dużych liczb na czynniki ani sfałszować podpisów. Upraszcza to analizę, ale może pomijać ataki na poziomie implementacji.

Komunikaty są modelowane jako termy: enc(k, m), sig(sk, m), hash(m), pair(a, b). Atakujący zna określone termy i wyprowadza nowe, korzystając ze zdefiniowanych reguł (reguł dedukcji).

Wiedza atakującego jest domknięta względem dedukcji: jeśli zna enc(k,m) oraz k, może wyprowadzić m. Jeśli zna pair(a,b), może wyprowadzić a i b. Domknięcie wiedzy początkowej = wszystko, czego atakujący może się dowiedzieć.

Bezpieczeństwo protokołu definiuje się następująco: „wiedza atakującego nigdy nie zawiera sekretu s w żadnym osiągalnym stanie”. Poufność = osiągalność. Uwierzytelnianie = brak określonych wzorców niepożądanych śladów.

Protokół dwóch stron: A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B}. W algebrze termów: Alice wysyła enc(pubkey_B, pair(Na, A)). Weryfikujemy, że po zakończeniu wykonania tylko B zna Na.

Rachunek pi z zastosowaniami (Abadi i Fournet, 2001) to algebra procesów służąca do modelowania protokołów. Procesy komunikują się za pośrednictwem kanałów; atakujący kontroluje kanały publiczne. ProVerif i Tamarin korzystają z tego formalizmu.

Protokół bezpieczny w modelu Doleva-Yao może nadal być niebezpieczny obliczeniowo, jeśli zastosowana implementacja kryptografii jest słaba. Twierdzenie o poprawności obliczeniowej (Cortier i in.) łączy te dwa ujęcia dla określonych klas prymitywów.

Dolev-Yao nie potrafi modelować: właściwości algebraicznych (np. przemienności XOR), ataków wykorzystujących kanały boczne, błędów implementacji ani awarii probabilistycznych. Rozszerzenia, takie jak teoria równościowa, pozwalają modelować niektóre właściwości algebraiczne.

Jakiej możliwości NIE ma atakujący w modelu Doleva-Yao?

Model Doleva-Yao daje atakującemu pełną kontrolę nad siecią, ale zakłada doskonałą kryptografię. Komunikaty są termami w algebrze, a bezpieczeństwo jest właściwością osiągalności. Rachunek pi z zastosowaniami zapewnia język formalny. Ograniczenia: nie pozwala modelować zależności algebraicznych, kanałów bocznych ani błędów implementacji.