Model Dolewa-Yao
Doleva -Yao , nazwany na cześć jego autorów Danny'ego Doleva i Andrew Yao , jest formalnym modelem używanym do udowodnienia właściwości interaktywnych protokołów kryptograficznych.
Sieć
Sieć jest reprezentowana przez zestaw abstrakcyjnych maszyn, które mogą wymieniać komunikaty. Komunikaty te składają się z terminów formalnych. Terminy te ujawniają część wewnętrznej struktury wiadomości, ale niektóre części, miejmy nadzieję, pozostaną nieprzejrzyste dla przeciwnika.
Przeciwnik
Przeciwnik w tym modelu może podsłuchać, przechwycić i zsyntetyzować dowolną wiadomość i jest ograniczony jedynie ograniczeniami zastosowanych metod kryptograficznych. Innymi słowy: „atakujący niesie wiadomość”.
tej wszechmocy było bardzo trudne, a wiele modeli zagrożeń upraszcza ją, tak jak zrobiono to z atakującym we wszechobecnych komputerach .
Model algebraiczny
Prymitywy kryptograficzne są modelowane przez operatory abstrakcyjne. użytkownika jest przez funkcję szyfrowania deszyfrowania skład funkcją tożsamości ( wiadomość nic ujawnia o \ Inaczej niż w prawdziwym świecie, przeciwnik nie może ani manipulować reprezentacją bitową szyfrowania, ani odgadnąć klucza. Atakujący może jednak ponownie wykorzystać wszelkie wysłane wiadomości, które w związku z tym staną się znane. Atakujący może je zaszyfrować lub odszyfrować dowolnymi znanymi sobie kluczami, aby sfałszować kolejne wiadomości.
Protokół jest modelowany jako zestaw kolejnych uruchomień, naprzemiennie między zapytaniami (wysyłanie wiadomości przez sieć) i odpowiedziami (uzyskiwanie wiadomości z sieci).
Uwaga
Symboliczny charakter modelu Doleva-Yao sprawia, że jest on łatwiejszy w zarządzaniu niż modele obliczeniowe i dostępny dla metod algebraicznych , ale potencjalnie mniej realistyczny. Jednak oba rodzaje modeli protokołów kryptograficznych zostały powiązane. Ponadto modele symboliczne bardzo dobrze nadają się do pokazania, że protokół jest uszkodzony , a nie bezpieczny, przy danych założeniach dotyczących możliwości atakujących.