Automatyka czasowa jest rozszerzeniem automatyki - teoretycznego podejscia do modelowania systemow czasu rzeczywistego, ktore wprowadza czas do klasycznej automatyki. Od czasu, gdy zostala po raz pierwszy zaproponowana na poczatku lat dziewiecdziesiatych, stala sie waznym obszarem badan i byla szeroko badana zarowno w kontekscie jezykow formalnych, jak i modelowania i weryfikacji systemow czasu rzeczywistego. Automaty czasu rzeczywistego wykorzystuja geste modelowanie czasowe, pozwalajace na sprawne sprawdzanie modeli systemow wrazliwych na czas, ktorych prawidlowe funkcjonowanie zalezy od wlasciwosci czasowych. Jednym z tych obszarow zastosowan jest weryfikacja protokolow bezpieczenstwa. Ksiazka ta koncentruje sie na modelu automatyki czasowej i wykorzystuje go jako narzedzie weryfikacyjne dla protokolow bezpieczenstwa. Jako studium przypadku, Neuman-Stubblebine Repeated Authentication Protocol jest modelowany i weryfikowany z wykorzystaniem wrazliwych czasowo wlasciwosci modelu. Wady protokolu sa analizowane i komentowane na temat korzysci i wyzwan zwiazanych z modelem.