Sammendrag
Dette arbeidet handler om autentiseringsprotokoller og ulike formelle metoder som benyttes
i arbeidet med dem. I oppgaven benytter jeg de metodene ASM (Abstrakte tilstandsmaskiner),
og AsmL (Abstrakt tilstandsmaskinspråk) for å lage en kjørbar modell
av Needham-Schroeder protokollen for autentisering. Modellen er en spesifikasjon av protokollen
og kan brukes som utgangspunkt for videre arbeid i ulike retninger. Den er nyttig
i utviklingsarbeid, testing og vedlikehold av implementasjonen.
Oversikt over oppgaven:
Arbeidet er strukturert i 11 kapitler og ett tilleg. I kapittel 2 kommer en drøfting om
datasikkerhet basert på følgende hovedspørsmål. Hva legger vi i begrepet datasikkerhet?
Hvorfor trenger vi datasikkerhet og hvordan blir vi påvirket av ulike krav om datasikkerhet?
Jeg beskriver noen grunnleggende tjenester som regnes som basis for datasikkerhet.
Tjenestene handler henholdsvis om konfidensialitet, integritet og tilgjengelighet. Deretter
introduserer jeg et av kjernebegrepene i oppgaven, autentisering: Hva er autentisering for
oss i dagliglivet og hva er det i dataverdenen? Deretter følger en kort drøfting om hvorfor
den menneskelige faktoren er avgjørende i arbeidet med datasikkerhet.
Kapittel 3 gir en innføring i kryptografi. Med kryptografi tenker vi på teknikker for å
gjøre skrift uleselig for andre. Vi ser hvordan utviklingen av kryptografiske teknikker har
foregått, hvordan de brukes i dag og hvordan de danner grunnlaget for autentisering over
datanettverk.
Kapittel 4 beskriver hva en protokoll er, og hvilke ulike typer av protokoller som finnes. Vi
ser noen eksempler på ulike typer av protokoller og går igjennom hva som skjer ved bruk
av en autentiseringsprotokoll.
I kapittel 5 går vi igjennom hvilke feil og angrep som kan rettes mot protokoller generelt,
og autentiseringsprotokoller spesielt. Angrep og feil deles inn i ulike kategorier og det gir
noen eksempler på de ulike feilene og angrepene som kan opptre. Vi ser også kort på hva
2 KAPITTEL 1. INNLEDNING
vi mener med en angriper i et datanettverk. Hvilke handlinger kan angriperen foreta, og
hvilke ressurser er angriperen i besittelse av?
Kapittel 6 viser de ulike formelle metodene som brukes i arbeidet med autentiseringsprotokoller.
Hvorfor bruker vi formelle metoder for å designe og studere autentiseringsprotokoller?
Vi deler de formelle metodene inn i ulike kategorier og ser nærmere på hver enkelt.
Fordeler og ulemper ved de ulike metodene blir diskutert og vi kommer kort inn på hva
som kan være fornuftig anvendelse.
Needham-Schroeder protokollen for autentisering beskrives i kapittel 7. Vi går gjennom
noen av de feil og angrep som er rettet mot den og hvordan den er blitt forbedret. Vi
kommer tilbake til protokollen i min AsmL spesifikasjon av den.
Kapittel 8 beskriver nærmere Abstrakte tilstandsmaskiner (ASM), som er en av de formelle
metodene som kan brukes i arbeidet med autentiseringsprotokoller. Vi sier litt om hvorfor
en ønsker å bruke ASMer, og gir eksempler på hvordan en kan gå frem for å lage en ASM.
Bruken av ASM i akademia og i næringslivet beskrives kort. Verktøy som kan benyttes i
arbeidet med ASM blir også nevnt, i det neste kapittelet tar vi nærmere for oss et av disse
verktøyene.
Verktøyet i kapittel 9 AsmL, er et kjørbart spesifikasjonsspråk som bygger på ASM. I
kapittelet beskrives AsmL systemet og hvordan det kan brukes i design og utvikling av
protokoller, programmer og maskinvare. Vi ser på noen enkle eksempler på bruk av AsmL,
før vi går løs på en spesifikasjon av Needham-Schroeder protokollen for autentisering i
AsmL.
I kapittel 10 beskrives en modell for en enkel versjon av Needham-Schroeder protokollen
for autentisering som jeg har laget. Vi ser på de ulike delene den består av og hvordan
den kan kjøres. Arbeidet med spesifikasjonen kan sees på som en utviklingsprosess, hvor vi
starter med en enkel beskrivelse og går trinnvis over til en detaljert spesifikasjon. Videre
ser vi på hva som kan læres av arbeidet med en slik spesifikasjon, og hvilke muligheter vi
har for videre arbeid. Det videre arbeidet kan gå i flere retninger og vi ser nærmere på
disse retningene. Vi oppsumerer arbeidet som er gjort og ser på resultatene av det.