Dlaczego nieformalne dowody nie wystarczają

Projektanci protokołów regularnie tworzą nieformalne argumenty dotyczące bezpieczeństwa — opisowe uzasadnienia, dlaczego atakujący nie może odnieść sukcesu. Historia pokazuje, że takie argumenty często są błędne, nawet w przypadku protokołów zaprojektowanych przez ekspertów.

Protokół Needham-Schroeder (1978) zaprojektowano do wzajemnego uwierzytelniania. W 1995 roku Gavin Lowe znalazł atak typu man-in-the-middle za pomocą automatycznej weryfikacji — 17 lat po publikacji protokołu. W nieformalnym dowodzie pominięto subtelny atak powtórzeniowy.

WEP został zatwierdzony przez IEEE w 1997 roku wraz z nieformalnymi deklaracjami bezpieczeństwa. Do 2001 roku badacze wykryli ponowne użycie strumienia klucza RC4, kolizje IV i brak integralności — co pozwalało złamać protokół w ciągu kilku minut. Nieformalne rozumowanie nie wykryło żadnego z tych problemów.

Bezpieczeństwo protokołów zależy od interakcji między wieloma równoczesnymi sesjami, aktywnymi atakującymi i założeniami kryptograficznymi. Ludzkie rozumowanie ma trudności z eksplozją liczby stanów i przeplatanymi równoczesnymi wykonaniami.

Metody formalne modelują protokół matematycznie i dowodzą prawdziwości lub obalają własności bezpieczeństwa (tajność, uwierzytelnianie, utajnienie przekazywane) dla wszystkich możliwych strategii atakującego, a nie tylko tych rozważonych przez projektanta.

Symboliczne (Dolev-Yao): kryptografia jest doskonałą czarną skrzynką, a nacisk kładzie się na logikę protokołu. Obliczeniowe: rzeczywiste probabilistyczne gry bezpieczeństwa, bliższe gwarancjom ze świata rzeczywistego. Oba podejścia wykrywają rzeczywiste błędy.

POODLE (2014) wykorzystywał wyrocznię dopełnienia w CBC protokołu SSL 3.0. Luka wynikała z błędu w projekcie na poziomie protokołu, a nie z błędu implementacji. Formalna analiza specyfikacji SSL 3.0 wykryłaby tę wyrocznię przed wdrożeniem.

TLS 1.3 (RFC 8446) zaprojektowano równolegle z analizami formalnymi z użyciem ProVerif i miTLS. Specyfikację iteracyjnie ulepszano na podstawie wyników formalnych — był to przełomowy moment w przyjęciu metod formalnych przez organizacje normalizacyjne.

Narzędzia formalne weryfikują model protokołu, a nie implementację. Formalnie zweryfikowany protokół nadal może mieć niebezpieczną implementację. F* / HACL* rozszerza weryfikację na sam kod kryptograficzny.

Weryfikacja formalna jest kosztowna: modelowanie protokołu trwa tygodnie i wymaga specjalistycznej wiedzy. Jednak w przypadku celów o wysokiej wartości (TLS, SSH, Signal) koszt ten jest uzasadniony — jedna wada protokołu może dotknąć miliardów użytkowników.

Co sprawiło, że odkrycie przez Lowe'a w 1995 roku ataku na protokół Needham-Schroeder było tak istotne?

Nieformalne dowody zawodzą, ponieważ ludzkie rozumowanie pomija interakcje między równoczesnymi sesjami i strategie atakujących. Protokoły Needham-Schroeder, WEP i POODLE miały nieformalne argumenty dotyczące bezpieczeństwa. TLS 1.3 uwzględniał analizę formalną już na etapie projektowania. Narzędzia formalne wykrywają błędy na poziomie protokołu przed wdrożeniem.