Przestrzenie nici stanowią ogólne ramy modelowania protokołów i potwierdzania poprawności protokołów. Brak udowodnienia poprawności daje wgląd w możliwe wady protokołów. Model wykorzystuje reprezentację graficzną, aby pokazać związek przyczynowy między terminami w protokole. Narzędzia takie jak Athena , ASPECT i inne, wykorzystywane do analizy bezpieczeństwa protokołów, są oparte na przestrzeniach nici. Takie narzędzia analizują protokoły reprezentowane w notacji przestrzeni pasm i obliczają, czy protokoły spełniają warunki bezpieczeństwa, czy nie. Jeśli nie, obliczenia dają wgląd w typy ataków, które mogą być możliwe w tych protokołach. Dostępność takich narzędzi i prostota reprezentacji to główne powody, dla których wybraliśmy przestrzenie pasm dla ram zaproponowanych w tym rozdziale. Członkowie grupy w protokole byliby określani jako podmioty główne w reprezentacji protokołu w przestrzeni pasm. Załóżmy, że zbiór A reprezentuje wszystkie możliwe terminy, które mogą być wysyłane i odbierane w protokole. Ślad wszystkich czynności wykonywanych przez instancję pryncypała lub penetratora jest reprezentowany jako pasmo. Każda nić składa się z sekwencji węzłów połączonych symbolem „⇒”. Każdy węzeł reprezentuje działanie podjęte przez mocodawcę. Akcja może polegać na wysyłaniu lub odbieraniu. Jeśli jednostka główna wysyła termin t z węzła n1 i to samo jest odbierane przez węzeł n2, wówczas termin (n1) = + t i termin (n2) = −t, a węzeł n1 jest połączony z węzłem n2 symbolem „→. ” Przestrzenie pasm modelują zdolność przeciwnika (tj. Penetratora lub intruza) za pomocą pasm penetratorów. Penetrator, jak określono , jest przystosowany do odgadnięcia wiadomości tekstowej (M), odgadnięcia nonce, znanego tylko jemu w tym czasie (R), łączenia dwóch z otrzymanych terminów (C), rozdzielania otrzymanych terminów na składniki (S) , odgadywanie klucza (K), szyfrowanie terminu znanym kluczem (E), deszyfrowanie terminu kluczem znanym penetratorowi (D), odgadywanie terminu DH (F), podpisywanie terminu znanym kluczem podpisu ( σ), wyodrębnianie zwykłego tekstu z podpisanych terminów (X) i haszowanie dowolnego terminu (H). W związku z tym ślady nici penetratora zawierałyby węzły, takie jak:
- M, wiadomość tekstowa: <+ t>, gdzie t Є T
- R, świeża liczba nonce: <+r>, gdzie r Є RP oznacza zbiór znanych wartości nonce do penetratora
- C, konkatenacja: <−g, −h, + gh>
- S, rozdział na składniki: <-gh, + g, + h>
- K, klucz: <+ K>, gdzie K Є KP oznacza zestaw kluczy znanych programowi penetrator
- E, szyfrowanie: <−K, −h, + {h}K>
- D, – deszyfrowanie: <−K-1, – {h} K, + h>
- F, świeża wartość DH: <+ gp>
- σ, podpisywanie: <-K, -h, + [h] K>, gdzie K Є KSig. KSig to zestaw kluczy używanych przez uczestników do podpisywania wiadomości
- X, wyodrębnianie zwykłego tekstu z podpisów: <-[h]K, + h>
- H, hashowanie: <−g, + hash (g)>.
Atak na protokół jest modelowany poprzez przeplatanie nici zwykłych uczestników z wątkami penetratora. Zbiór wszystkich węzłów wraz ze zbiorem wszystkich krawędzi → ∪ ⇒ tworzą graf skierowany. Skończony, acykliczny podgraf powyższego grafu nazywany jest wiązką, jeśli spełnione są dwa następujące warunki:
- Dla wszystkich obecnych węzłów odbiorczych odpowiednie są węzły nadawcze obecne również w pakiecie.
- Dla wszystkich obecnych węzłów, ich bezpośrednimi poprzednikami są również obecne w pakiecie.
Jeśli zbiór S jest właściwym podzbiorem zbioru → ∪ ⇒, to symbol ≤S oznacza zwrotne, przechodnie domknięcie S. Załóżmy, że C jest wiązką. Wtedy ≤ C jest relacją częściowego porządku, a każdy niepusty podzbiór węzłów w C ma ≤C minimalne elementy członkowskie. Uważa się, że termin pochodzi z węzła, jeśli którykolwiek z terminów, z których można wywnioskować, pochodzi z węzła [15]. W związku z tym, używając przestrzeni pasm, okazuje się, że termin jest tajny, również przez udowodnienie, że nie pochodzi z wiązki. Reprezentacja protokołów w przestrzeni nici może być używana w połączeniu z narzędziami, takimi jak Athena , do analizy poprawności protokołów i znajdowania możliwych ataków w protokole. Podstawowy model przestrzeni nici nie został wykorzystany do oceny poufności przekazywania protokołów. W tym rozdziale przedstawiono rozszerzenia modelu przestrzeni pasm w celu stworzenia struktury do analizy poufności przekazywania protokołów. Rozszerzenia są podane w następnej sekcji jako część opisu struktury do analizy poufności przekazywania protokołów.
.