Przez protokoł kryptograficzny rozumiemy scenariusz wymiany komunikatow
pomiędzy uczestnikami. Dobry scenariusz powinien mieć wyspecyfikowany cel
bezpieczeństwa oraz dodane komentarze mowiące o tym w jakim kontekście
protokoł może być użyty, i ewentualnie jaki stopień zaufania przypisujemy
poszczegolnym 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 protokoł może prowadzić do niepożądanych efektow
zatem każdy użytkownik protokołu chiałby używać protokołow niezawodnych.
Niezawodność protokołow nie zależy jedynie od tego jak protokoł jest
zaprojektowany ale rownież jak jest zaimplementowany. Jednym z błędow
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 protokoł.
Potrzeba projektowania dobrych protokołow spowodowała rozwoj metod formalnej
weryfikacji protokołow. Wykład ten będzie przeglądem głownych metod,
paradygmatow specyfikacji i narzędzi do automatycznej weryfikacji protokołow.
