Abstract
Vi kombinerer to varianter av pi-kalkylen, asynkron pi-kalkyle
og anvendt pi-kalkyle ("applied pi-calculus"), til en ny
kalkyle: anvendt asynkron pi-kalkyle. Kalkylen modellerer asynkron
kommunikasjon og tillater bruk av funksjoner, som er en naturlig
måte å modellere sikkerhetsmekanismer på. Vårt fokus i denne
oppgaven er modellering av asynkron sikker kommunikasjon, dog er
kalkylen generell og ikke begrenset til dette.
Maude er et deklarativt programmeringsspråk basert på matematisk
teori for omskrivningslogikk. Ligninger og omskrivningsregler
benyttes for å spesifisere henholdsvis likheter og mulige
omskrivninger mellom termer. Termer kan benyttes for å modellere
tilstander i systemer og omskrivningsregler beskriver da mulige
transisjoner fra en tilstand til en annen. Maude-systemet er
et kraftig verktøy for å utføre omskrivninger og søk i slike
spesifikasjoner.
Vi utvider en Maude-modell for asynkron pi-kalkyle til å bli en
modell av anvendt asynkron pi-kalkyle. Med denne modellen kan
Maude brukes som et verktøy for analyse i anvendt asynkron
pi-kalkyle og vi ser på flere eksempler på hvordan dette kan
gjøres.
Oppgaven gir en grundig innføring i pi-kalkylen og de to
variantene vi kombinerer. Videre gis en introduksjon av Maude
og begreper innen sikkerhet. Dette gir grunnlag for å resonnere
rundt sikkerhet i spesifikasjoner i vår modell.