Timed Automata jako narzędzie weryfikacyjne dla protokolw bezpieczeństwa

Automatyka czasowa jest rozszerzeniem automatyki - teoretycznego podejcia do modelowania systemw czasu rzeczywistego, ktre wprowadza czas do klasycznej automatyki. Od czasu, gdy zostaa po raz pierwszy zaproponowana na pocztku lat dziewidziesitych, staa si wanym obszarem bada i bya szeroko badana zarwno w kontekcie jzykw formalnych, jak i modelowania i weryfikacji systemw czasu rzeczywistego. Automaty czasu rzeczywistego wykorzystuj gste modelowanie czasowe, pozwalajce na sprawne sprawdzanie modeli systemw wraliwych na czas, ktrych prawidowe funkcjonowanie zaley od waciwoci czasowych. Jednym z tych obszarw zastosowa jest weryfikacja protokow bezpieczestwa. Ksika ta koncentruje si na modelu automatyki czasowej i wykorzystuje go jako narzdzie weryfikacyjne dla protokow bezpieczestwa. Jako studium przypadku, Neuman-Stubblebine Repeated Authentication Protocol jest modelowany i weryfikowany z wykorzystaniem wraliwych czasowo waciwoci modelu. Wady protokou s analizowane i komentowane na temat korzyci i wyzwa zwizanych z modelem.