Referat będzie składał sie z dwóch części. W pierwszej zostanie
krótko omówiony problem weryfikacji modelowej i system weryfikacyjny
Verics rozwijany w IPI PAN. Zostaną przedstawione dwie metody
weryfikacji BMC i UMC, bazujące na translacji do problemu SAT.
W drugiej części referatu będą omówione znane metody i systemy
wykorzystywane do weryfikacji protokołów kryptograficznych.
Następnie zostanie przestawiona nowa metoda weryfikacji, wykorzystująca
zależności czasowe w celu sprawdzenia czy czas wykonania protokółu
może być zmieniony wskutek działania Intruza.
Wykład zakończy prezentacja wyników eksperymentalnych uzyskanych
z wykorzystaniem systemu Verics i Kronos.
|
Seminaria \ Seminarium Instytutowe \ Archiwum - 2007/2008 \ 6.12.2007 Wojciech Penczek 
