Oppikerta 8, 30.2.1999

Yleistä protokollien suunnittelun systematisoinnista

Niin pian kuin nämä odotukset ja ominaisuudet on tyhjentävästi lueteltu vaatimusdokumentissa, voidaan validointiin käyttää tekniikkaa jota kutsutaan verifioinniksi. Sen tehtävänä on näyttää, että protokolla toteuttaa vaatimukset.

Verifiointimenetelmää kutsutaan formaaliksi (eli muodolliseksi), jos protokollan vaatimukset ja spesifikaatiot on kirjoitettu kielellä, jolla on formaali syntaksi ja (mielellään) sellainen formaali semantiikka, joka mahdollistaa spesifikaation kääntämisen algoritmiksi. Vaikka protokollien formalisointi tarjoaa käsitteellisen työkalun tai viitekehyksen joka auttaa suunnittelun henkistä prosessia, suurin hyöty systematisoinnista ja notaatiosta saavutetaan kuitenkin siitä, että ongelmia voidaan tämän jälkeen ratkoa automatisoidulla symbolisella laskennalla.

On olemassa monenlaisia formalismeja, menetelmiä edetä niistä verifiointiin sekä työkaluja, joilla menetelmiä voidaan automatisoida. Alaa pohtinut ACM:n työryhmä (1996) raportoi kuitenkin optimistisesti: "Overall, the myriad of formalisms had led to a healthy diversity rather than fragmentation of the discipline." Seuraavassa on tiivistelmä mainitussa raportissa esitetyistä ulottuvuuksista, joiden suhteen arvioidaan formalismeja, menetelmiä ja työkaluja. (Tähdellä on merkitty ne suunnat, joita jäljempänä käsiteltävä CSP edustaa.)

• Ensinnäkin formalismit perustuvat johonkin rinnakkaisuuden malliin ja nämä mallit voidaan luokitella seuraavien kolmen joko-tai-tyyppisen ulottuvuuden mukaan.
  • intensionaalisuus (sisäinen eli toiminnallinen näkökulma) --- (*) ekstensionaalisuus (ulkoinen eli havainnollinen eli denotationaalinen näkökulma).
  • rinnakkaisuuden luonne: todellinen --- (*) limitettu ('interleaved' - simuloitavissa yhdellä prosessorilla)
  • ajan luonne: (*) lineaarinen --- haarautuva (puumainen)
• Toiseksi (eli neljäntenä ulottuvuutena) formalismi voi käyttää joko
  • logiikkaa (erityisesti temporaalista) systeemin ominaisuuksien ilmaisemiseen, tai
  • (*) käyttäytymissuhteita, erityisesti ekvivalensseja ja järjestysominaisuuksia, joiden pohjalta järjestelmää verrataan spesifikaatioonsa. Askelittain hienontaminen (refinement) on tässä mahdollista.
• Kolmanneksi, verifiointimenetelmä voi perustua joko
  • todistusjärjestelmään, jossa on aksioomat ja päättelysäännöt, tai
  • (*) äärellistilaiseen siirtymäsysteemiin (finite-state transition system). Verifiointia kutsutaan tällöin mallin tarkistukseksi (model checking). Tutkittava ominaisuus ilmaistaan jonkin temporaalisen logiikan kaavana, ja tarkistuksen tehtävänä on selvittää mallintaako siirtymäsysteemi tätä kaavaa.
• Viimeiseksi: verifointityökaluja luokitellaan sen mukaan minkä verran ne vaativat käyttäjän vuorovaikutusta. Työkaluista on sanottu: "Tools are not the most important thing about formal methods. They are the only important thing." [Rushby & Shankar: Theorem Proving and Model Checking for Software, 1996: luento PS-muodossa] Työkalun tärkein ominaisuus on tietenkin sen tehokkuus.

Kryptograafisten protokollien formaali verifiointi

1. Mallinnetaan ja verifioidaan protokolla käyttäen spesifikaatiokieliä ja verifiointityökaluja, joita ei ole nimenomaan suunniteltu kryptograafisia protokollia varten. Tässä voidaan hyödyntää kohdejärjestelmän erityisrakennetta vaimentamaan tila-avaruuden räjähtämistä, mikä on tyypillistä automaattisessa verifioinnissa. Tietoturvaprotokollat voivat usein olla siedettäviä tässä suhteessa sillä niissä on yleensä vain harvoja toimijoita ja viestejä. Toisaalta tarkastelu pitää ulottaa viestien sisältöön, vaikka kryptosysteemien yksityiskohtia ei otettaisikaan huomioon. Tätä lähestymistapaa edustaa CSP.
2. Laaditaan asiantuntijajärjestelmä, jota protokollan suunnittelija voi käyttää luomaan erilaisia tilanteita ja tutkimaan niitä.
3. Mallinnetaan protokollaperheen vaatimukset käyttäen logiikkaa, joka soveltuu tiedon ja uskomuksen analysointiin (episteeminen logiikka). Varhaisin ja monista ehdotetuista laajennuksista huolimatta suosituin tällainen on BAN-logiikka (viime kerran aihe). Se käsittelee uskomusta, eikä tästä syystä sovellu yksityisyyttä koskevaan päättelyyn. Tämä lähestymistapa edellyttää idealisaatiovaihetta, jossa kukin protokollan viesti muunnetaan kaavoiksi, jotka koskevat tätä viestiä.
4. Kehitetään formaali menetelmä joka perustuu algebrallisille kryptograafisten systeemien terminkorvausominaisuuksille (term-rewriting properties). Vaikka tähän lähestymistapaan käytännössä liittyy tilakone, korostus on sanoissa, joita toimijat voivat luoda, ja tavoitteena on selvittää, onko näiden joukossa myös sellaisia, joita niiden ei pitäisi pystyä generoimaan.

• saada tietää mikä tahansa viesti;
• pysäyttää mikä tahansa viesti (paitsi broadcast-tyyppinen);
• muodostaa uusia viestejä;
• purkaa viestin salaus, mutta vain jos sillä on tiedossa asiaankuuluva avain;
• uudelleenlähettää (replay) mikä tahansa viesti, riippumatta siitä ymmärtääkö se viestin sisällön.

CSP kryptograafisten protokollien mallinnuksessa

• Steve Schneider: Security properties and CSP (1996, = tämän kerran artikkeli), Verifying authentication protocols with CSP (1997) ja Formal analysis of a non-repudiation protocol (1998). Näihin on linkit kirjoittajan kotisivulta.
• Gavin Lowe: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR (1996) A Hierarchy of Authentication Specifications (1997), Casper: A Compiler for the Analysis of Security Protocols (1997). Näihin on linkit kirjoittajan sivulta.

Vertaa tätä seuraavaan CSP-esitykseen:

User_A = []_{i: USER}
trans.A!i!p_i(n_A.A) -->
rec.A.i?p_A(n_A.x.i) -->
trans.A!i!p_i(x) --> Stop.

User_B =
rec.B?j!p_B(y.j) -->
trans.B!j!p_j(y.n_B.B) -->
rec.B.j.p_B(n_B) --> Stop.

ENEMY(S) =
trans?i?j?m --> ENEMY( S U {m} )
  []
[]_{i,j:USER , S |- m} rec.i!j!m --> ENEMY(S)

NET = (User_A ||| User_B) |[ trans, rec ]| ENEMY

Oletetaan nyt yleisesti, että olet laatinut jonkin tietoturvatavoitteen toteuttamiseksi kryptograafisen protokollan ja haluat varmistua, että voimakaskaan hyökkääjä ei pysty estämään tavoitteesi toteutumista eli murtamaan protokollaasi.

Oletetaan lisäksi, että käytössäsi on ultrasupertietokone, jolla voit kohtuuajassa käydä läpi mittaamattoman (joskin äärellisen) määrän erilaisia tapauksia - eli kaikenlaisia tilanteita, joita protokollan ympärillä voi syntyä. Nämä tilanteet pitäisi luoda sillä tavalla, että jos hyökkäys voi onnistua, sitä vastaava tilanne tulee mukaan ja pystytään tunnistamaan. Käyttäen mallina edellä olevaa CSP-esimerkkiä pohdi,

• miten lähtisit luomaan tilanteita? Toisin sanoen miten mallintaisit protokollaa ja sen toimintaa?
• Millaiseen ympäristöön asetat protokollan? Mitä toimijoita siinä on?
• Mistä osista yksi "tilanne" muodostuu? Miten tila(ntee)sta päästään uuteen tilaan?
• Miten viestien lähettäminen ja vastaanottaminen vaikuttaa? Missä määrin voit abstrahoida viestien sisältöä?
• Hyökkääjä pitää olla, mutta onko niitä oltava useita? Miten hyökkääjän hallussa oleva tieto mallittuu?
• Hyökkääjä ei varmaankaan noudata protokollaa, mutta missä määrin lailliset osapuolet noudattavat sitä?
• Miten ilmenee onnistunut hyökkäys? Voiko protokollan tavoite jäädä saavuttamatta vaikka onnistunutta hyökkäystä ei löydykään?
• Voisiko mallia analysoida jotenkin muutenkin kuin käymällä koneellisesti läpi kaikenlaiset vaihtoehdot.

Yleisesti CSP:stä

FDR (failures divergences refinement) on mallintarkistaja (model checker), joka toimii siten, että se käy läpi tila-avaruuden kaikki tilat (soveltaen kaikkia allamainittuja CSP-semantiikan näkökulmia). Näin ollen se voi käsitellä vain äärellistilaisia systeemejä (muutamaan miljoonaan tilaan asti). Siispä menetelmää voidaan käyttää vain sellaisen systeemin tutkimiseen, jossa on rajattu määrä osapuolia, käytännössä vain muutama. Protokollan sinänsä pitää toimia käytännössä rajattoman toimijajoukon puitteissa.

CSP-kuvauksen laatimista varten on olemassa myös kääntäjä, Casper. Sen syötteenä on tekstitiedosto, jossa kuvataan protokolla melko tavalliseen tyyliin ja myös tutkittava systeemi osapuolineen, avaimineen yms. Tuloksena on vastaava CSP-kuvaus.

CSP on prosessialgebra ja sitä voisi karkeasti verrata Boolen algebraan seuraavasti:

Ilmiö	Boole	CSP
aakkosto	muuttujat vakiot	tapahtumat
operaatiot	disjunktio, konjunktio negaatio,...	peräkkäisyys: --> vaihtoehtoisuus: [] (neliö, ulkoisesti valittu) ja [¯] (hakanen, epädeterm.); rinnakkaisuus: |[ tapahtumia ]| , ||| (jos synkronoitavia tapahtumia ei ole), ...
laskusäännöt	kommutatiivisuus distributiivisuus de Morgan, ...	kommutatiivisuus, distributiivisuus, ..., rekursiivisten määrittelyjen käsittelyssä kiintopisteen periaate
semantiikka, merkitys	muuttujien ja vakioiden kuvaus totuusarvoiksi; totuusarvoja yleensä ajatellaan myös silloin, kun näennäisesti vain pyöritellään kaavoja. Totuusarvojen joukko voidaan esittää graafisesti Boolen hilana.	operationaalinen (lähellä implementaatiota): esitettävissä siirtymäkaavioina (LTS, labelled transition system) denotationaalinen: vastaa lähinnä kuvausta totuusarvoiksi, joita tässä tapauksessa edustavat jäljet (traces) eli mahdolliset tapahtumien ketjut. Näille tarvitaan usein pareiksi 'failures' eli ne tapahtumat, jotka kulloinkin ovat mahdottomia. Kolmantena komponenttina voivat olla 'divergences' (~ ikisilmukat). algebrallinen: tietyt laskusäännöt otetaan aksioomiksi. Kielen merkitys muodostuu sitten samaan tapaan kuin esim. kokonaislukujen abstrakti merkitys rakentuu niiden aksioomista.

Viime kerralla esitetyssä BAN-logiikassa analyysin vaiheet olivat: protokollan idealisaatio uskomuksia käsitteleviksi (ajattomiksi) kaavoiksi, alkuoletusten kirjaaminen, tavoitelauseiden johtaminen päättelysäännöillä. Nyt protokolla mallinnetaan määrittämällä osapuolet, hyökkääjä ja verkko (media) prosesseiksi, joissa tapahtumina ovat tietynmuotoiset viestit, jotka "lähetetään" kanavia pitkin. Mitään lähetyksiä ei tietenkään tapahdu ja puhe kanavista on vain havainnollistus. Kyse on tapahtumien tietotyypeistä eli äärellisistä joukoista, joiden alkioita tapahtumat ovat. Joukot voivat kasvaa tapahtumien edetessä. Tällä voidaan mallintaa esim. sitä, että hyökkääjä pystyy johtamaan (ja sitten myös lähettämään) uusia viestejä aiemmin kuulemistaan. Tietojen koostumista mallinnetaan kieliopin tapaan ja informaatiosysteemin avulla voidaan ratkaista, onko jokin tieto johdettavissa aiemmista.

Verkon sijasta voidaan toimijat kytkeä suoraan toisiinsa esim. siten, että hyökkääjä = media (kuten edellä). Tai sitten otetaan toimijoiden (noodien) taakse vielä käyttäjä (kuten tämän päivän artikkelissa tehdään: kanavat in.i ja out.i)

Uskomuksia ei tarvitse mallintaa, vaan tietoturvatavoitteet ilmaistaan vaatimuksina sille, mitä ominaisuuksia jäljillä pitää olla. Siis kaikkien mahdollisten tapahtumaketjujen pitää toteuttaa joitakin ominaisuuksia.

1. Luottamuksellisuuden tapauksessa tällainen ominaisuus on se, että salaiseksi tarkoitettu viesti (eli tapahtuman tietyn kentän arvot tietystä joukosta) ei koskaan esiinny hyökkääjään vastaanottamia viestejä kuvaavissa tapahtumissa. Tämän kerran artikkeli kehittelee tälle vaatimukselle useita vaihtoehtoisia formalisointeja.
2. Autenttisuus edellyttää sitä, että jälki ei sisällä tiettyä tapahtumaa T ellei jotain muuta tapahtuma R esiinny ennen sitä. Tämän merkitys on: T autentikoi R:n. Prosessialgebrallinen formalisointi: P [| R,T |] Stop = P [| R |] Stop.

Vastauksen etsiminen tähän on samaa toimintaa mitä pitää tehdä kun protokollaa verifioidaan. Erityisesti voidaan todistaa, että autentikoiduksi tulee tapahtuma trans.A.B.p_B(n_B), mikä merkitsee, että A on vastannut B:n nonce-haasteeseen. Toisin (ja tarkemmin) sanoen, protokollan lopussa B tietää että myös A on päässyt loppuun ja että A uskoi kommunikoineensa B:n kanssa. Ellei toisen viestin lopussa olisi mainittu B:n nimeä, tätä tavoitetta ei saavutettaisi.

Autentikoinnin (tiukimman tason, ajastamaton) vaatimus mallinnettuna Lowen mukaan:

Agreement(B-role, A-role, {d1,d2}) (B) =
signal.Running.B-role.B?A?e1?e2 -->
signal.Commit.A-role.A.B.e1.e2 --> Stop.

Tässä erotellaan, missä rooleissa osapuolet osallistuvat protokollaan. Kanavan signal viestit ovat protokollan mallinnuksessa esiintyviä aputapahtumia, joilla osapuolet ikäänkuin välittävät uskomuksiaan (!) tarkkailijalle. Merkitys on seuraava: Jos A ilmaisee, että hän on suorittanut loppuun protokollan ("Commit") kommunikoiden A-roolissa B:n kanssa käyttäen tietoalkioita e1 ja e2, niin B on tätä ennen ajanut protokollaa kommunikoiden B-roolissa A:n kanssa samoja tietoalkoita käyttäen.

Olkoon mallinnettu jokin protokolla prosessina SYSTEM (kuten "NET" alun esimerkissä) siten, että signal-kanavaa käytetään asianmukaisissa paikoissa. Toteuttaako protokolla tällaisen autenttisuuden, testataan kysymällä FDR:ltä, onko prosessi SYSTEM - (S - X) hienonnus (eli refinement) prosessille Agreement(B-role, A-role, {d1,d2}) (B). Tässä X tarkoittaa niitä tapahtumia, joita jälkimmäisen prosessin aakkostoon kuuluu ja S on kaikkien tapahtumien joukko, SYSTEM -(S-X) tarkoittaa siis sellaista prosessia josta on piilotettu kaikki muut tapahtumat (sisäisiksi, näkymättömiksi) paitsi ne jotka kuuluvat X:ään

Harjoitus Seuraavassa on äskeiseen liittyvä esimerkki Lowen notaatiolla, jossa viestien rakenne on kryptauksen osalta hieman aiemmasta poikkeava. Isolla kirjoitetut tietoalkiot edustavat vakioarvoja ja pienellä kirjoitetut muuttujia. Vertaa tätä protokollan aloittajaprosessia aiempaan esimerkkiin (prosessiin User_A). Kiinnitä huomiosi siihen, miten signaalit Running ja Commit sijoittuvat.

INITIATOR(A,na,pka) =
[]_B:Agent env.A.(Env0.B) -->
comm.A.B.(Msg1.Encrypt.(PK(B), <na,nb>)) -->
[]_nb:Nonce comm.B.A.(Msg2,Encrypt.(pka.<na,nb,B>)) -->
signal.Running.INIT-role.A.B.na.nb -->
comm.A.B.(Msg3,Encrypt.(PK(B),<nb>)) -->
signal.Commit.INIT-role.A.B.na.nb -->
SKIP

Toisenlainen esimerkki signal-kanavien tapaisista protokollan ulkopuolisista tapahtumista on evidence-kanava, jollaista voidaan käyttää kiistämättömyysvaatimuksen mallintamisessa. Tällaisessa tapauksessa ei riitä, että tarkoitetut toimijat noudattavat protokollaa. Semantiikkaan puolestaan pitää ottaa mukaan failures ja divergences (eli "estymät" ja "pillastumat").