Tomasz Truderung, Institute of Computer Science, Wroclaw Uniwersity, Poland
Kontakt
Zobacz także
Najczęściej używane protokoły

Formalna weryfikacja protokołów kryptograficznych

Protokoły kryptograficzne

Z protokołami kryptograficznymi stykamy się często, być może nie zawsze sobie to uświadamiając. Dzieje się tak na przykład, gdy używamy telefonu komórkowego, korzystamy z karty płatniczej, czy za pomocą Internetu sprawdzamy stan konta bankowego. To właśnie protokoły kryptograficzne mają gwarantować, że wykonując te zwykłe czynności, nie będziemy narażeni na nadużycia i straty.

Formalna weryfikacja

Źle skonstruowany protokół naraża swoich uczestników na wymierne i czasami bardzo dotkliwe straty. Dlatego niezwykle ważne jest osiągnąć pewność, że protokół którego używamy jest rzeczywiście bezpieczny, że rzeczywiście można polegać na gwarancjach, jakich udziela.

Okazuje się jednak, że na pytanie, czy protokół jest wiarygodny, bardzo trudno uzyskać pewną odpowiedź. Jest tak nawet w przypadku prostych protokołów, których struktura wydaje się zupełnie przekonująca i przejrzysta. Znanych jest wiele przykładów protokołów, które przez lata uchodziły za bezpieczne, zanim nie znaleziono w nich luk umożliwiających poważne nadużycia.

Potrzeba uwiarygadniania protokołów stała się impulsem dla rozwoju metod formalnej i automatycznej weryfikacji. Metody te skupiają się głównie na takich błędach w protokołach, które nie są związane z niedoskonałościami używanych metod kryptograficznych (jak szyfrowanie czy kryptograficzne funkcje skrótu) lecz raczej z wadliwym sposobem ich użycia. Inaczej mówiąc, chodzi nam tu o błędy w logicznej strukturze protokołu. Okazuje się, że większość błędów wykrytych w opublikowanych protokołach ma taką właśnie naturę: protokoły te nie są bezpieczne nawet wtedy, gdy założymy, że używane w nich metody kryptograficzne działają w sposób idealny.

W dziedzinie formalnej weryfikacji protokołów wypracowano już sporo teoretycznych i praktycznych narzędzi (jak programy weryfikujące poprawność protokołów), które udowodniły swoją użyteczność w wyszukiwaniu błędów i luk w protokołach. Narzędzia te nie sprawiają, że konstruowanie dobrych protokołów kryptograficznych staje się łatwe. Umożliwiają jednak w coraz większym zakresie weryfikowanie ich poprawności. Metody te pozwalają tym samym opierać nasze zaufanie do protokołów kryptograficznych na solidniejszych podstawach.

Moje wyniki