En Maude-modell for sikker asynkron kommunikajon i pi-kalkylen

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.