Przez protokół kryptograficzny rozumiemy scenariusz wymiany komunikatów
pomiędzy uczestnikami. Dobry scenariusz powinien mieć wyspecyfikowany cel
bezpieczeństwa oraz dodane komentarze mówiące o tym w jakim kontekście
protokół może być użyty, i ewentualnie jaki stopień zaufania przypisujemy
poszczególnym rolom.
Z protokołami spotykamy się w wielu sytuacjach życiowych np sprawdzając przez
internet stan konta bankowego lub wykonując operacje finansowe kartą
płatniczą. Źle zaprojektowany protokół może prowadzić do niepożądanych efektów
zatem każdy użytkownik protokołu chiałby używać protokołów niezawodnych.
Niezawodność protokołów nie zależy jedynie od tego jak protokół jest
zaprojektowany ale również jak jest zaimplementowany. Jednym z błędów
powodujących podatność protokołu na ataki jest błąd przepełnienia bufora
Unikanie tego typu błędu właściwie nie należy do zadań projektanta protokołu
ale do konstruktora kompilatora oraz do programisty implementującego protokół.
Potrzeba projektowania dobrych protokołów spowodowała rozwój metod formalnej
weryfikacji protokołów. Wykład ten będzie przeglądem głównych metod,
paradygmatów specyfikacji i narzędzi do automatycznej weryfikacji protokołów.
