Modelowanie i weryfikacja protokołów bezpieczeństwa za pomocą Applied Pi Calculus i ProVerif

Oryginalny tytuł:

Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif

Zawartość książki:

Weryfikacja protokołów bezpieczeństwa jest aktywnym obszarem badań od lat 90-tych. Temat ten jest interesujący z kilku powodów.

Protokoły bezpieczeństwa są wszechobecne: są używane między innymi w handlu elektronicznym, sieciach bezprzewodowych, kartach kredytowych, głosowaniu elektronicznym. Projektowanie protokołów bezpieczeństwa jest notorycznie podatne na błędy. Błędy te mogą mieć również poważne konsekwencje.

Dlatego też formalna weryfikacja protokołów jest szczególnie pożądana.

Niniejszy przegląd skupia się na weryfikacji specyfikacji protokołów w modelu symbolicznym. Mimo że jest on dość abstrakcyjny, ten poziom weryfikacji jest istotny w praktyce, ponieważ umożliwia wykrycie wielu ataków.

ProVerif to automatyczny weryfikator protokołów symbolicznych. Obsługuje szeroki zakres prymitywów kryptograficznych, zdefiniowanych przez reguły przepisywania lub równania. Może udowodnić różne właściwości bezpieczeństwa: tajność, uwierzytelnianie i równoważność procesów, dla nieograniczonej przestrzeni komunikatów i nieograniczonej liczby sesji.

Jako dane wejściowe przyjmuje opis protokołu do weryfikacji w dialekcie stosowanego rachunku pi, będącego rozszerzeniem rachunku pi o kryptografię. Automatycznie tłumaczy ten opis protokołu na klauzule Horna i określa, czy pożądane właściwości bezpieczeństwa są spełnione poprzez rozwiązanie tych klauzul. Niniejszy przegląd przedstawia przegląd badań nad ProVerif i jest najbardziej kompleksowym tekstem dostępnym na ten temat.