Kryptoprotokollat, luento 10 (A) 20.4.2009

Yleistä protokollien suunnittelun systematisoinnista

Kun protokollaa laaditaan, keskeinen tavoite on että siitä tulee luotettava. Tämä tarkoittaa että protokolla todella ratkaisee käsillä olevan ongelman, eli yhtäpitävästi: sillä on kaikki toivotut ominaisuudet - siten kuin ne ilmenevät inhimilliselle tarkkailijalle tai protokollan käyttäjälle. Validointi määritellään prosessiksi, jolla vakuututaan siitä, että protokolla vastaa inhimillisiä odotuksia sen suhteen, mikä oikeastaan on ongelman ratkaisu tai mikä on toivottu ominaisuus.

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.

Suurimman hankaluuden protokollien suunnittelulle, niin yleisesti tietoliikenteessä kuin tietoturvamielessäkin, aiheuttaa niissä esiintyvä rinnakkaisuus. Ei ole olemassa mitään yhtä tapaa, jolla sen voisi pelkistää ja saada hallintaansa. Päinvastoin on olemassa kovin monenlaisia formalismeja, menetelmiä edetä niistä verifiointiin sekä työkaluja, joilla menetelmiä voidaan automatisoida. Rinnakkaislaskennan kenttää pohtinut ACM:n strategiatyö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 rinnakkaisuuden käsittelyyn käytettäviä formalismeja, menetelmiä ja työkaluja. Tähdellä on merkitty ne suunnat, joita kurssilla erikseen esiteltävä CSP edustaa. Toinen kurssilla käsiteltävä menetelmä, BAN-logiikka, ei oikeastaan mallinna rinnakkaisuutta, joten sitä ei kannata luokitella tässä yhteydessä.

Mainitun raportin mukaan yksi tietojenkäsittelytieteen haasteista on etsiä keinoja, joilla voitaisiin yhdistää rinnakkaisten systeemien suunnittelun ja verifioinnin metodologioita.

Kryptografisten protokollien formaali verifiointi

Päähuomio formaalien menetelmien soveltamisessa tietoturvaprotokolliin on ollut autentikoinnissa ja avaimenvaihdossa. Schneier mainitsee neljä lähestysmistapaa [Schn96]. Näistä ensimmäinen on se, jota edellä käsiteltiin yleisemmin.
  1. Mallinnetaan ja verifioidaan protokolla käyttäen spesifikaatiokieliä ja verifiointityökaluja, joita ei ole nimenomaan suunniteltu kryptografisia 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 tai doxastinen logiikka). Varhaisin ja monista ehdotetuista laajennuksista huolimatta suosituin tällainen on BAN-logiikka. Se käsittelee uskomusta, eikä tästä syystä sovellu yksityisyyttä ja tiedon salassapysymistä 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 kryptografisten systeemien terminkorvausominaisuuksille (term-rewriting properties). Vaikka tähän lähestymistapaan käytännössä liittyy tilakone, korostus on sanoissa, joita toimijat voivat luoda. Tavoitteena on selvittää, onko näiden sanojen joukossa myös sellaisia, joita toimijoiden ei pitäisi pystyä generoimaan.
Kaikissa näissä menetelmissä mallin pitää jollain tavalla sisältää hyökkääjä, jolle on mallinnettava kyky Monissa menetelmissä käytetään lähtökohtana Dolev-Yao -mallia vuodelta 1983. Siinä protokollasta voi olla useita samanaikaisia suorituksia käynnissä ja kryptoalgoritmit käyttäytyvät kuin "mustat laatikot", jotka noudattavat tiettyjä algebrallisia ominaisuuksia. Malliin kuuluu oleellisena osana myös em. kaltainen hyökkääjä. Yksi hyökkääjän lisärooli voi tietysti olla, että se pystyy kontrolloimaan jotain järjestelmän normaalia osapuolta, mikä on käytännössä sama asia kuin jos kyseinen osapuoli olisi hyökkääjä.

Esimerkkejä siitä, miltä formaalit menetelmät näyttävät, löytyy artikkelista C.J.F. Cremers, S. Mauw & E.P. de Vink: Formal Methods for Security Protocols: Three Examples of the Black-Box Approach (2003). Tässä ovat esillä samat kolme menetelmää kuin kurssin B-osassa, eli BAN-logiikka, CSP-algebra ja tuorein menetelmä "ranta-avaruudet" (strand spaces.) Viime kerran GSM-anonymisoinnin (JLC-) artikkelista löytyy BAN-käsittely.

Formaalien menetelmien ongelmista

Kuten viimeistään kurssin B-osan materiaalista voi havaita, formaalien menetelmien ongelmia ovat niiden käsitteellinen tai ainakin merkinnällinen hankaluus, laskennallinen mutkikkuus ja niitä koskevan kehitystyön osittainen keskeneräisyys. Toisaalta se, että esim. autenttisuuden käsitteestä on useita variaatioita, ei ole suinkaan formaalien menetelmien vika.

Ryan ja Schneider toteavatkin artikkelissaan "Process algebras and non-interference" (1999), että turvallisuuskäsitteen määrittelystä ei olla yksimielisiä, eikä edes luottamuksellisuudesta, joka on vain turvallisuuden osa-alue, ja sellaisena varmaankin yksinkertaisempi kuin autenttisuus.

Kuten edelläkin nähtiin, hyvin luonnollinen ajatus on, että luottamuksellisuus on sitä, että tietynlaista tietovirtaa ei esiinny, nimittäin sitä, jossa salaiseksi tarkoitettua tietoa pääsee asiattomien haltuun. Kirjoittajat toteavat että tietovirtojen määrittelykin on puutteellinen. Tätä aihepiiriä on muuten sivuttu TTJ-kurssilla, jossa puhuttiin luottamuksellisuuden hierarkkisista tasoista ja tietovirtojen rajoittamiseen mainittiin mm. säännöt NRU ja NWD (no read up ja no write down).

Tietovirtojen puuttumisen käsittely voidaan kirjoittajien mukaan palauttaa (redusoida) järjestelmien ekvivalenttisuuden tutkimiseen. Tämä onkin sitten juuri sellaista toimintaa, jota prosessialgebrassa tehdään.

Yleisemmin formaalien menetelmien ongelmia, ja samalla uusia suuntauksia, käsittelee artikkeli C. Meadows: Open issues in Formal Methods for Cryptographic Protocol Analysis. Proceedings of the DISCEX 2000, IEEE Comp.Soc.Press Jan. 2000, 237-250. Meadows päivitti artikkeliaan kolme vuotta myöhemmin ja esittää nyt enimmäkseen samat asiat "esiinnousevina tutkimusalueina". Kyseinen artikkeli on Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends. IEEE J. Selected Areas in Comm. Jan, 2003.

Seuraavanlaisissa yhä tavallisemmiksi tulleissa tilanteissa formaalit menetelmät joutuvat vaikeuksiin. Jaottelu on kohtaa 4 lukuunottamatta peräisin vanhemmasta artikkelista, mutta vastaavat asiat esiintyvät myös uudemmassa (luvut III ja IV).

  1. Avoimet protokollat (open-ended), eli sellaiset joissa voi olla ennalta arvaamaton määrä osapuolia tai viestin tietokenttiä. Edellisestä ovat esimerkkejä broadcast, ryhmäviestintä ja anonymisointi usean palvelimen kautta. Monenlaisia tietokenttiä esiintyy esim., kun IPSecin IKE-protokollassa sovitaan turvaparametreista (jotka muodostavat SA:n eli Security Associationin).

  2. Palvelun esto. Tässä on useita puolia. Yksinkertaisempi havainto on se, että viestin estämisellä aiheutetaan tietyn protokollan tiettyä viestiä koskeva palvelun esto. Formaaleissa menetelmissä kuten BAN:ssa tai CSP:ssä laadittavat mallit eivät edes ota huomioon sitä, että viestit estyisivät, koska se ei ole kiinnostavaa tarkasteltavien "tärkeämpien" turvatavoitteiden kannalta.

    Vaikeampi ilmiö muodostuu nykyään tavanomaiseksi muodostuneesta palvelunestosta. Siinä uhri kuluttaa resurssejaan (prosessoritehoa, muistia) hyökkääjän palvelemiseen, myös esim. virheellisten autentikoitumisten tarkastamiseen, siinä määrin, ettei pysty palvelemaan normaaleja käyttäjiä. Suosittu lähestymistapa on suunnitella protokolla siten, että hyökkääjä joutuu kuluttamaan omia resurssejaan suhteellisen paljon ennen kuin se saa palvelimen kuluttamaan merkittävästi resursseja. Jotta tästä voitaisiin vakuuttua, pitäisi voida mallintaa osapuolien toimenpiteet ja näiden toimenpiteiden aiheuttamat kulut. Nykyiset työkalut eivät suoraan sovellu tähän.

  3. Anonymisointi. Anonymisoinnilla on useita ominaisuuksia, jotka tekevät siitä vaikean analysoida. Ensinnäkin, anonymoisoiva protokolla vaatii muutakin verkkoliikennettä, jotta anonymiteetti voidaan saavuttaa. Toiseksi, vahvemmat anonymiteettiprotokollat vaativat, että liikennöinti tapahtuu mielivaltaisen monen solmun välillä. Useimmat protokollat, joita on tähän asti analysoitu, olettavat että solmuja on vain kaksi tai kolme. Kolmanneksi, systeemin pitäisi näyttää hyökkääjälle samalta riippumatta siitä, ketkä ovat viestiliikenteen osapuolina. Neljänneksi, koska anonymiteetiprotokollat yrittävät säilyttää tietoa salaisena hajauttamalla sitä useisiin säilytyskohteisiin, analyysissa on olennaista, minkälaisia oletuksia hyökkääjän mahdollisuuksista tehdään. Ei liene realistista, että hyökkääjällä olisi pääsy kaikkiin verkon solmuihin muttei sekään, että hänellä olisi pääsy vain yhteen solmuun. Ääripäiden välisen kompromissin löytäminen on siis avainasemassa.

  4. Sähköinen kaupankäynti. Useat sähköisessä kaupankäynnissä haluttavat ominaisuudet kuten reiluus ja väärinkäytöksen mahdottomuus, ovat vaikeita tai mahdottomia analysoida nykyisillä työkaluilla. Joillakin työkaluilla voidaan approksimoida kyseisiä ominaisuuksia niillä, joita kyseiset työkalut voivat tarkistaa.

  5. Yksityiskohtaisuus (high fidelity): Järjestelmiä analysoidaan usein niin korkealla abstraktiotasolla, että protokollan toteutusyksityiskohdat jäävät piiloon ja siten myös niissä mahdollisesti sijaitsevat turva-aukot. Esimerkiksi kryptoalgoritmeja ei voi kaikissa tapauksissa pitää pelkkinä mustina laatikoina, sillä niillä voi olla vuorovaikutusta keskenään. Myös protokollan ja algoritmien vuorovaikutus voi tuottaa haavoittuvuuden, jos vaikkapa protokolla tuottaa "valittua selkotekstiä" algoritmille, joka ei kestä sen kautta tapahtuvaa hyökkäystä. Ongelmia voi tulla myös vuorovaikutuksista muiden algoritmien kuten hash-funktioiden ja salausmoodien kanssa. Yleisemmin tietysti implementaation todellisuus voi olla varsin toisenlainen kuin abstraktisti on näytetty toteen.

  6. Koostettavuus (composability): on vaikea ratkaista, onko turvallisista osaprotokollista koostettu kokonaisuus myös turvallinen. Monet käytännön protokollat tarjoavat erilaisia optioita, esim. SSL mahdollisuuden myös asiakkaan autentikointiin. Tällaisissa tilanteissa kokonaisuus ei muodostukaan enää suoraviivaisesti peräkkäin suoritettavista askelista ja tulee hankalammin analysoitavaksi. Olisi paljon helpompaa analysoida suoraviivaiset osat erikseen, jos vain yhdistämisen turvallisuus kyettäisiin ratkaisemaan tehokkaasti. Tästä on todistettu monenlaisia teoreemoja. Keskeistä olisi, etteivät osaprotokollat pääsisi vaikuttamaan toisiinsa siten, että ne hyväksyisivät viestejä toisiltaan. Varsinkaan ei pitäisi protokollakokoelman eri osaprotokollien viestejä voida sekoittaa toisikseen. Ongelma voi jäädä huomaamatta jos liikutaan liian korkealla abstraktiotasolla (vrt. yksityiskohtaisuus edellä).

  7. Mutkikkaat tietorakenteet: sen lisäksi mitä kohdassa 1 sanottiin tietokenttien määrän epämääräisyydestä, jo se että niitä voi olla useita, mutkistaa analyysia.

  8. Menetelmien käyttöönotto ei ole edennyt, vaikka tietyn abstraktiotason mallintamiseen on automatisoituja työkaluja. Menetelmiä pitäisi ottaa käyttöön jo standardointivaiheessa.
Näiden ongelmien tai trendien lisäksi Meadowsin artikkeli sisältää hyvän katsauksen formaalien menetelmien historiaan. Artikkelissa mainitaan myös yksi menetelmä, jota ei sivuta luennoissa (tämän enempää). Se on tyypintarkistus: Viestit ja kanavat tarkistetaan niissä sallittujen tyyppien osalta ja väärän tyypin löytyminen tarkoittaa tietoturvaongelmaa.

Samoihin aikoihin vuonna 2003 Meadowsin kanssa kirjoittaneet Yasinsac ja Childs vahvistavat hänen näkemystään kryptoprotokollien kehittymisestä vaikeammin analysoitaviksi. He tiivistävät modernien protokollien hankaliksi piirteiksi monimutkaiset tietorakenteet sekä haarautumiset. Jälkimmäisestä on esimerkkinä kryptoalgoritmien (cipher suite) valinta, jota varten on aliprotokollansa. Tällaiset valinnaisuudet tuovat lisää toiminnallisuutta ja joustavuutta mutta hankaloittavat analyysia ja tarjoavat useampia tilaisuuksia hyökkääjälle löytää haavoittuvuuksia. (Artikkeli on Formal analysis of modern security protocols, Information Sciences 2005, ja siinä ruoditaan esimerkkinä TLS-protokolla käyttäen CPAL-kieltä.)

Vedonlyöntiä piilossa

Päivän artikkeli raportoi TTY:llä tehtyä tutkimusta ja se on osa ensimmäisen kirjoittajansa väitöskirjaa joulukuulta 2006:
Panu Hämäläinen, Marko Hännikäinen, Timo D. Hämäläinen, Riku Soininen, Risto Rautee, Design and Implementation of Real-time Betting System with Offline Terminals, Electronic Commerce Research and Applications, March 20, 2006, Vol.5, Issue 2, pp. 170-188, Elsevier.
Vedonlyönnin protokollia voisi ajatella erikoistapauksena maksamisesta: vedonlyöjä maksaa vedon ja saa mahdollisesti voiton tietyn kertoimen mukaan. Tietysti voidaan ottaa käyttöön tili, jolle suoritetaan etukäteen rahalla jokin talletus ja jolta pelimaksuja veloitetaan ja jolle voittoja maksetaan bitteinä, kunnes mahdollisen ylijäämän voi lunastaa rahana.

Järjestelmä saadaan sitä kiinnostavammaksi vedonlyöjän kannalta mitä lähempänä vedonlyöntikohteen ratkeamista oman panoksen voi vielä asettaa. Täydellisen reaaliaikaisuuden esteenä voivat olla palvelinten rajallinen suorituskyky ja verkon siirtoviiveet. Päivän artikkeli viittaa joihinkin reaaliaikaisiin vedonlyöntiprotokolliin ja toteaa niiden heikon skaalautuvuuden, joka johtuu on-line -toiminnasta. Tästä koituu ongelmia reiluuden kanssa, mikä tässä yhteydessä tarkoittaakin tasapuolisuutta eri käyttäjien kesken -- eli eri asiaa kuin aiempien luentojen yhteydessä.

On-line -ongelmat tarjoavat motivaation kehitellä off-line -protokollaa, josta tässä käytetään nimeä ORTB (artikkelissa off-line RTB). Ideana on, että vedonlyöjän laite saa tietoja vedonlyönnin järjestäjän palvelimelta ja käyttäjä voi tehdä sijoituksia ja saada voittoja, mutta laitteesta ei lähde viestejä palvelimelle ennen kuin istunto on ohi.

On helppo ymmärtää, että ORTB ei voi toimia, ellei käyttäjän laitteessa ole jotain sellaista, johon palvelin voi luottaa. Siinä tarvitaankin TPM-sirun kaltainen luotettu alusta, joskin artikkeli toteaa, että TPM-määritykset eivät suoraan tarjoa kaikkia piirteitä. Erityinen puute TPM:ssä muodostuu siitä, että kellon oikeellisuudesta ei voida vakuuttua.

Kellon luotettava toiminta on keskeinen ORTB:n vaatimus. Sen toteuttamiseksi artikkeli rakentaa monitasoista ajastusprotokollaa, joka ei ole lainkaan kryptografinen vaan laitteistollinen. Siinä otetaan huomioon prosessorikellon erilaiset epätarkkuudet ja niiden maksimikertymä muutaman tunnin mittaisen istunnon aikana. Palvelin yleislähettää ajastuspaketteja (ticks) ja luotetun prosessorin pitää pystyä päättelemään, onko sen seinäkelloaika riittävän lähellä oikeaa. Artikkelin esittämien tarkistusten perusteella prosessori pystyy havaitsemaan poikkeamat, kunhan hyökkääjä pystyy enintään toiseen seuraavista: modifioimaan vapaasti kellolaskurin taajuutta ja myöhästämään yleislähetyksiä.

Uhkamallia ei artikkelissa ollut asetettu täsmällisesti, mutta viimeksi mainitun vahvankin hyökkääjän onnistuminen todetaan mahdottomaksi, jos palvelin aika ajoin mutta satunnaisesti avaa kaksisuuntaisen yhteyden vedonlyöntilaitteeseen. Kaikkien teknisten tarkastusten lisäksi artikkeli suosittelee käyttäjien tarkkailua ja asioihin puuttumista, mikäli joku alkaa voittaa "epäilyttävän usein".

Kellon oikeellisuus on ratkaisevaa sen takia, että ORTB:n luotettu moduuli oleellisesti vain aikaleimaa kaikki käyttäjän valinnat. Käyttäjän hallinnassa oleva moduuli voi toki pitää käyttäjän ajan tasalla vedonlyönnin sujumisesta, mutta vasta palvelimelle toimitettu loki tapahtumista realisoi voitot. Silloin on siis oleellista tarkistaa, että panokset on asetettu ennen määräaikoja. Tietenkään lokia ei ole saanut muuttaa myöskään siten, että siitä olisi poistettu hävinneitä vetoja. Lokin eheys voitaisiin periaatteessa hoitaa tallettamalla loki luotettuun moduuliin, mutta se ei ole tarpeen, sillä eheysmekanismina voidaan soveltaa kryptografiaa.

Lokien eheysmekanismina ORTB:ssä käytetään Schneierin ja Kelseyn esittämää ketjutusta (1998), jota voidaan yksinkertaistaa, sillä ORTB:ssä ei ole tarvetta luottamuksellisuudelle eikä osatietojen todennukselle. Jokaisen datakentän datai perään talletetaan avaimella Ai laskettu MAC-arvo chaini:

chaini = MAC( Ai, chaini-1 | datai)

Ketjutuksena siis otetaan i:nnellä kierroksella edellinen eli chaini-1 laskuun mukaan (ensimmäisellä 0). Avain Ai lasketaan niinikään joka kierrosta varten edellisestä:

Ai = H( "UpdateKey" | Ai-1).

Ensimmäinen avain A0 lasketaan käyttäjän autentikointiin sovelletusta avaimesta Km ja luotetun moduulin palvelimelta saamasta siemenarvosta q:

A0 = H( H( "StorageKey" | Km )| q ).

Käyttäjän moduuli ei pysty väärentämään chain-arvoja, koska se ei tiedä arvoa q, jonka luotettu moduuli kaiken lisäksi tuhoaa heti laskettuaan A0:n. Samoin jokainen Ai tuhotaan käytön jälkeen.