Formalne metody weryfikacji własności protokołów zabezpieczających w sieciach komputerowych.

okładka

Formalne metody weryfikacji własności protokołów zabezpieczających w sieciach komputerowych.

Produkt jest aktualnie niedostępny

Kliknij tutaj, jeśli chcesz otrzymać maila, gdy produkt stanie się ponownie dostępny

OPIS

1. Wprowadzenie
2. Wstęp do protokołów zabezpieczających
2.1. Elementy kryptografii 2.2. Protokoły - pojęcia podstawowe 2.3. Wiarygodność protokołów 2.4. Protokół Needhama-Schroedera z kluczem publicznym 2.5. Protokół Andrew RPC (wersja BAN) 2.6. Protokół Needhama-Schroedera z Centrum Certyfikacji 2.7. Znaczniki czasu - protokoły WMF i Kerberos 2.8. Protokół wymiany klucza z kluczem publicznym 2.9. Rodzaje ataków i modele Intruza 2.10. Podsumowanie
3. Metody specyfikacji protokołów zabezpieczających
3.1. Common Language 3.2. Język CAPSL 3.3. Projekt AVISPA i język HLPSL 3.4. Język ProToc 3.5. Podsumowanie
4. Metody weryfikacji protokołów zabezpieczających
4.1. Wstęp do meto weryfikacji 4.2. Metody indukcyjne i dedukcyjne (aksjomatyczne) 4.3. Weryfikacja modelowa (model checking) 4.4. Narzędzia AVISPA 4.5. Modelowanie i weryfikacja protokołów za pomocą automatów 4.6. Wyniki 4.7. Podsumowanie
5. Logiki uwierzytelniania stron
5.1. Logika BAN 5.2. Weryfikacja protokołów w logice BAN 5.3. Krytyka logiki BAN - Nessett'a 5.4. Logika GNY 5.5. Logika Abadi'ego i Tuttle'a 5.6. Inne systemy logik uwierzytelniania 5.7. Zalety i wady logik uwierzytelniania 5.8. Podsumowanie
6 Quasi-temporalna wiedzowa logika uwierzytelniania
6.1. Wprowadzenie 6.2. Syntaktyka logiki 6.3. System dedukcyjny logiki 6.4. Struktura obliczeniowa 6.5. Semantyka 6.6. Pełność 6.7. Rozstrzygalność 6.8. Złożoność obliczeniowa algorytmu rozstrzygania 6.9. Przekonania 6.10. Aspekty temporalne 6.11. Wyrażalność 6.12. Podsumowanie
7. Automatowa weryfikacja protokołów bezczasowych
7.1. Wprowadzenie 7.2. Syntaktyka dla protokołów bezczasowych 7.3. Struktura obliczeniowa 7.4. Modelowanie ataków 7.5. Sieci zsynchronizowanych automatów 7.6. Weryfikacja metodą indukcji odwrotnej 7.7. Wyniki eksperymentalne 7.8. Podsumowanie
8. Weryfikacja protokołów zależnych od czasu
8.1. Syntaktyka dla protokołów zależnych od czasu 8.2. Struktura obliczeniowa 8.3. Modelowanie ataków 8.4. Sieć zsynchronizowanych automatów czasowych 8.5. Weryfikacja protokołów zależnych od czasu metodą indukcji odwrotnej 8.6. Wyniki eksperymentalne 8.7. Podsumowanie
9. Modelowanie przez łańcuchy stanów
9.1. Modelowanie wykonań kroków protokołu przez łańcuchy stanów 9.2. Poprawne łańcuchy stanów 9.3. Algorytm weryfikacji 9.4. Wyniki eksperymentalne 9.5. Podsumowanie
10. Zakończenie 11. Załączniki
11.1. Logika zdaniowa 11.2. SAT i SAT-solvery 11.3. Specyfikacja protokołu NSPK w języku HLPSL 11.4. Gramatyka języka ProToc 11.5. Algorytm generowania wykonań i łańcuchów stanów
Literatura Indeks

DODATKOWE INFORMACJE

  • Format:165x235 mm
  • Liczba stron:216
  • Oprawa:miękka
  • ISBN-13:9788378370185
  • Data wydania:2013
  • Numer katalogowy:501270

RECENZJEjak działają recenzje?

Lista recenzji jest pusta

DOSTAWA

DARMOWA dostawa powyżej 299 zł!

Realizacja dostaw poprzez:

  • ups
  • paczkomaty
  • ruch
  • poczta

OPINIE

Nasza strona używa plików cookies, w celu ułatwienia Ci zakupów. Więcej informacji znajdziesz w polityce prywatności

© 2006-2024 Gildia Internet Services Sp. z o.o. and 2017-2024 Prószyński Media Sp z o.o. PgSearcher