POLECAMY
Koszyk
Formalne metody weryfikacji własności protokołów zabezpieczających w sieciach komputerowych
Autor:
Format:
ibuk
Nie bez powodu mówi się dzisiaj, że najbardziej cennym towarem na świecie jest informacja. Media nieustannie donoszą o kolejnych przypadkach wzlotów i upadków ludzi, firm, czy nawet państw. Bardzo często powodem tych zmian zachodzących w codziennym życiu jest posiadanie lub brak odpowiedniej informacji. Dlatego jednym najważniejszych problemów jest wiarygodność informacji oraz jej bezpieczeństwo. W pierwszym przypadku chodzi oczywiście o odpowiednią weryfikację informacji. Może tutaj chodzić o jej prawdziwość lub adekwatność. W drugim mamy do czynienia z takim problemem, że nie każda informacja ma pozostawać jawna, dostępna dla wielu lub wszystkich. W niniejszej rozprawia przedstawione są problemy związane z weryfikacją protokołów zabezpieczających w sieciach komputerowych.
| Rok wydania | 2014 |
|---|---|
| Liczba stron | 216 |
| Kategoria | Inne |
| Wydawca | Akademicka Oficyna Wydawnicza EXIT Andrzej Lang |
| ISBN-13 | 978-83-7837-526-5 |
| Numer wydania | 1 |
| Język publikacji | polski |
| Informacja o sprzedawcy | ePWN sp. z o.o. |
Ciekawe propozycje
Spis treści
| 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 | |
Wypożyczaj w abonamencie!
Już od 2,66 zł za ebooka
