83593: Oppikerta 7, 23.2.1999

Oppikerta 7, 23.2.1999

Koko oppikerta käytetään tämän kerran artikkelin käsittelyyn. Erityisesti käydään läpi joitakin sen esimerkkejä - jossain määrin harjoituksenomaisesti.

Protokollien analysointi BAN-logiikalla

Burrowsin, Abadin ja Needhamin "A logic of authentication" on oikeastaan uskomusten logiikkaa (eräänlaista modaalilogiikkaa siis). Sitä käytetään autentisointiprotokollien analysointiin. Tälläkin kurssilla protokollien saavutetuksia on perusteltu juuri uskomusten avulla. Jos esimerkiksi uskot, että K on Ainon julkinen avain, niin saatuasi viestin, jonka salauksen voit purkaa K:n avulla, voit uskoa, että viesti on alunperin Ainolta. Yleisenä taustaoletuksena BAN-logiikassa on, että viesteissä on aina riittävästi redundanssia sen havaitsemiseksi, oliko purkuavain oikea. Toinen yleinen taustaoletus on että käytettyyn kryptosysteemiin voi luottaa eikä esim. salaisia avaimia ole vuotanut julkisuuteen.

Logiikan keskeisenä rakenteena on kaava "P believes X". Jos tämä kaava on tosi - eli se voidaan analyysin kuluessa johtaa tehdyista oletuksista - se merkitsee, että osapuoli P voi toimia ikäänkuin X olisi tosi (vrt. Abadi-Needhamin periaate 2 "toimintaehdot").

Protokollan analyysissa on seuraavat vaiheet:

Alkuperäinen protokolla idealisoidaan/abstrahoidaan sellaiseksi, että sen viestit ovat jäljempänä olevan notaation mukaisia logiikan kaavoja. Erityisesti jätetään pois sellaiset viestin osat, joita ei ole salattu. Vaikka ne ovat tärkeitä vihjeitä osapuolten tehokkaan toiminnan kannalta, niillä ei kuitenkaan voi ole merkitystä autenttisuuden kannalta, koska ne voivat olla väärennettyjä. Pois jätetään myös muu sellainen aines, joka ei voi vaikuttaa osapuolten uskomuksiin.
Lähtötilannetta koskevat oletukset kirjataan, ts. loogisilla kaavoilla ilmaistaan, mitä uskomuksia milläkin osapuolella on. Nämä koskevat tyypillisesti osapuolten yhteisiä avaimia ja aikaleimojen tai nonce-arvojen tuoreutta.
Protokollan vaiheet varustetaan niiden jälkeen vallitsevaa tilaa koskevilla loogisilla kaavoilla ("annotaatiot"). Viestin lähettäminen merkitsee tyypillisesti sitä, että tarkoitetun vastaanottajan oletetaan sen jälkeen "näkevän" jotain uutta (kaavoja). Tässäkin on siis idealisointia sikäli, ettei viestien estämistä oteta huomioon.
Päättelysääntöjä sovelletaan kohtien 2 ja 3 kaavoihin. Tuloksena saadaan tietoa siitä, mitä uskomuksia osapuolilla on protokollan suorituksen jälkeen (oikeastaan jo jokaisen vaiheenkin jälkeen).

Autentisointiprotokollan päämäärä voi eri yhteyksissä olla hieman erilainen. Yksi luonnollinen tavoite on tilanne, jossa A ja B autentikoivat toisensa ja tuloksena on vain heidän tiedossaan oleva symmetrinen avain K eli "A <-K-> B". Tämä tilanne voidaan formalisoida seuraavasti:
A believes A <-K-> B , B believes A <-K-> B
Enemmänkin voidaan saavuttaa, esimerkiksi se, että B uskoo ensimmäisen ylläolevista väitteistä ja A jälkimmäisen.

Notaatio (syntaksi, jolla semanttinen selitys)

Seuraavassa P ja Q ovat osapuolia, X ja Y ovat väitteitä ja K on salausavain.

"P believes X", ks. edellä.
"P sees X": P on saanut viestin josta hän voi (mahd. dekryptauksen jälkeen) lukea X:n ja jatkossa siis myös kirjoittaa (lähettää) sen.
"P said X": P on joskus lähettänyt viestin johon sisältyi X. Erityisesti tiedetään, että tuolloin oli voimassa "P believes X".
"P controls X": P:llä on valta X:n suhteen ja P:hen voi siis luottaa X:n suhteen.
"fresh(X)": tietoa X ei ole lähetetty missään viestissä aikaisemmin. Nonce-luvulle N pätee määritelmänsö nojalla fresh(N).
" P <-K-> Q " : P:llä ja Q:lla on yhteinen symmetrinen avain K.
" -K-> P " : P:llä on julkinen avain K, jota vastaava salaisen avaimen K^-1 oletetaan olevan vain P:n tiedossa.
" P <=X=> Q " : X on salaisuus, jonka vain P ja Q tuntevat
" {X}_K " : X on salattu avaimella K; implisiittisesti kyseessä on aina viesti joltakulta.
" <X>_Y " : X on yhdistetty Y:n kanssa; käytännössä X ja Y on vain katenoitu, mutta salausta muistuttavalla merkinnällä korostetaan Y:n erikoisasemaa: sen on tyypillisesti tarkoitus olla salasana, joka todentaa X:n lähettäneen osapuolen.

Viimeksi mainittu yhdistelmä on erikoistapaus. Yleinen tapa ilmaista, että viesti tai väite koostuu osista, on merkitä osat sulkuihin pilkuilla eroteltuina, esim. (X,Y) koostuu osista X ja Y. Varsinaisesti tässä on kyseessä looginen konjunktio: Pilkku edustaa siis operaatiota AND.

Varsinaisesti syntaksi muodostuu pelkästään em. kaavoista ja niiden yhdistelemisen säännöistä, jotka ovat varsin yksinkertaiset: AND on ainoa konnektiivi ja "kontrolloituihin" avaimiin liittyy implisiittisesti kaikki-kvantifiointi: ts. jos palvelimen uskotaan hallitsevan avaimia, niin silloin uskotaan kaikkiin sen tuottamiin avaimiin. Merkitysten selitykset puolestaan ovat semantiikkaa, jonka tehtävänä on sitoa syntaksin mukainen formaali kieli todellisuuteen, joskin idealisoituun sellaiseen. Artikkelin laajempi versio luonnostelee logiikalle myös formaalista semantiikkaa.

Tässä logiikassa ei oteta huomioon aikaa eikä tapahtumien rinnakkaisuutta saman protokollan sisällä. Ainoa erottelu on aikaisempien protokollien ja viestien mennyt aika ja nykyhetki, jota meneillään olevan protokolla kaikkineen edustaa.

Alustava esimerkki ja harjoitus. Wide-mouthed frog-protokolla:
Viesti 1 A--> S: A, { T_A, B, K_AB } _{K_AS}
Viesti 2 S--> B: A, { T_S, A, K_AB } _{K_BS}

Mitä tässä tapahtuu ja mitä oletuksia siihen liittyy?

Oletukset ovat:

A believes A <-K_AS-> S
B believes B <-K_BS-> S
S believes A <-K_AS-> S
S believes B <-K_BS-> S
A believes A <-K_AB-> B
B believes A controls A <-K-> B
B believes S controls A believes A <-K-> B
S believes fresh(T_A)
B believes fresh(T_S)

Viestit näyttävät idealisoituina seuraavilta:
Viesti 1 A--> S: { T_A, A <-K_AB-> B } _{K_AS}
Viesti 2 S--> B: { T_S, A believes A <-K_AB-> B } _{K_BS}

Seuraavaksi esiteltäviä päättelysääntöjä käyttäen voidaan johtaa uskomukset:

B believes A <-K_AB-> B
B believes A <-K_AB-> B

Päättelysääntöjä

Seuraavilla säännöillä voidaan aiemmista väitteistä johtaa uusia.

Viestin tulkintaa koskevat säännöt: Voidaan päätellä "P believes Q said X", jos premisseinä on jokin seuraavista

P believes Q <-K-> P , P sees {X}_K
P believes -K-> Q , P sees {X}_K^-1
P believes P <=Y=> Q , P sees <X>_Y

Viestin tuoreus johtaa uskomaan enempäänkin seuraavasti (tämä on ainoa sääntö, jolla jokin sanottu ylennetään uskottuun asemaan):
Jos "P believes fresh(X) , P believes Q said X", niin
"P believes Q believes X"

Osapuolen luottamusta "controls"-auktoriteettiin kuvaa sääntö:
Jos "P believes Q controls X" ja "P believes Q believes X", niin
"P believes X".

Viestin osien näkemistä koskevat säännöt: Päätelmä "P sees X" voidaan tehdä, jos premisseinä on jokin seuraavista:

P sees (X,Y)
P sees <X>_Y
P believes Q <-K-> P , P sees {X}_K
P believes -K-> P , P sees {X}_K
P believes -K-> P , P sees {X}_K^-1

Osan tuoreus takaa kokonaisuuden tuoreuden eli:
Jos "P believes fresh(X)" niin "P believes fresh(X,Y)".

Edellä mainitut säännöt löytyvät tämän kerran artikkelin suppeasta versiosta. Laajemmassa versiossa on lisäksi sääntöjä, jotka koskevat viestin osia ja avainten tai salaisuuksien symmetriaa. Ensin mainittuihin liittyy havainnollisia huomautuksia, siitä millaiset säännöt eivät ole voimassa:

Jos "P believes X" ja "P believes Y", niin "P believes (X,Y)".
Jos "P believes (X,Y)", niin "P believes X".
Jos "P believes Q believes (X,Y)", niin "P believes Q believes X".
Jos "P believes Q said (X,Y)", niin "P believes Q said X".

Harjoitus: Mitä luonnolliselta tuntuvaa ei saa päätellä seuraavissa tilanteissa ja miksei?

"P believes Q said X" ja "P believes Q said X"
"P sees X" ja "P sees Y"

Symmetriasäännöt ovat ilmeisiä ja ne jätetään kirjaamatta tähän.

Esimerkit

Artikkeleissa käsitellään kahdeksaa protokollaa. Noin kuudessa tapauksessa niiden tarkoituksena sopia istuntoavaimesta siten, että sopijapuolet päätyvät jonkinlaiseen varmuuteen siitä, kenen kanssa sopimus tehtiin - lyhyesti sanoen kyse on siis autentisoidusta avaimenvaihdosta.

Suppeammassa artikkelissa analysoidaan neljä protokollaa mutta esitetään taulukkona tiivistelmä kaikista kahdeksasta. Mainitut neljä ovat:

Kerberos. Kellojen synkronoinnin tarve todetaan.
Andrew'n RPC-turvakättely (varhainen versio). Päättelysääntöjä soveltamalla ei päästä halutunlaiseen tulokseen ja syykin on selvä: Vika ilmenee tilanteessa, jossa vanha istuntoavain on paljastunut. (vrt. Andersson-Needamin periaate 5. Päätelmä: )
Needham-Schroederin julkisen avaimen protokolla. Yhdessä vastaavan symmetristä avainta käyttävän protokollan kanssa tämä on yksi vanhimmista (1978) ja lähtökohta monille variaatioille, mm. Kerberokselle. Tästä löytyy sama vika kuin em. Andrew'n protokollassa. Artikkeli myöntää siis sen, mutta analyysissa asia ilmenee siten, että on tehty "haavoittuva" lisäoletus. Tämä analyysi on ainoa esimerkki, jossa käytetään keskinäistä salaisuutta "P<=N=>Q" ja sen avulla allekirjoitettua yhdistelmää <X>_N.
CCITT X.509, kolmen viestin protokolla, jonka tarkoituksena on allekirjoitettu yksityisyyden säilyttävä viestintä. Tässä esiintyy sama vika, joka todettiin viime kerralla yhden viestin protokollassa (= sama kuin tämän ensimmäinen viesti). Syynä on ennen allekirjoitusta tapahtuva salaus.

Laajemmassa versiossa on lisäksi seuraavat neljä protokollaa ja näistäkin kaikista löytyy huomautettavaa. Kaikki neljä käyttävät symmetristä salausta ja autentisointipalvelinta.

Otway-Rees-protokolla. Saa "moitteita" redundanteista viestien osista ja salauksista.
Needham-Schroederin symmetrisen avaimen protokolla. Tästä siis löytyy sama vika kuin em. Andrew'n protokollassa. Otway-Rees on lähes samanlainen kuin korjattu versio tästä.
Wide-Mouthed Frog. Burrowsin yksinkertainen protokolla, jossa toinen osapuoli generoi yhteisen avaimen.
Yahalom. Tässä sovelletaan yhteistä salaisuutta (P<=X=>Q), jollaisen kirjoittajat toteavat kuuluvan jo lähtöoletuksiin.

Esimerkit/harjoitukset

Kerberos, suoraan artikkelin mukaisesti (tarkoitus oli jatkaa päättely loppuun asti, mutta siihen ei aika riittänyt).
Otway-Rees, laajemmasta versiosta. Tätä ei ehditty käsitellä. Analyysi löytyy yksityiskohtaisesti auki kirjoitettuna (mutta vähin selityksin) New Yorkista: 10 PS-sivua.
Tämän protokollan idealisointi on erikoinen. Protokollalla saavutetaan implisiittinen avaimen autentisointi ja vakuututaan avaimen tuoreudesta, mutta ei molemminpuolista olion autentisointia eikä eksplisiittistä avaimen autentisointia (näiden käsitteiden määrittelyä oli oppikerran 5 tekstissä)

BAN-logiikan kritiikkiä ja myöhempiä kehittelyjä

BAN on yksinkertainen ja intuitiivinen ja sen seurauksena tietenkin monin tavoin rajoittunut:

Logiikka antaa saman tuloksen riippumatta viestien järjestyksestä!
Protokollan formalisointi menee helposti harhaan. Myös alkuoletusten määrittäminen vaatii suurta huolellisuutta.
Mitä järkeä on uskoa nonce-luku (vrt. "nonce-verification-sääntö", jonka tulos on oli "P believes Q believes X".)?
Vaikka protokolla (oikein formalisoitunakin) olisi BAN:n perusteella oikein, se ei välttämättä ole sitä. Esimerkkinä on laajemmassa versiossa analysoitu Otway-Rees-protokolla.

Yksi syy viimeksi mainittuun on se, ettei BAN ole täydellinen (complete) eli on olemassa tosia kaavoja, joita ei voi johtaa päättelysäännöillä. Yksi esimerkki tästä epätäydellisyyden ongelmasta on se, ettei havaita, että jollekulle muullekin kuin A:lle ja B:lle (ja palvelimelle) saattaa muodostua uskomuksia avaimesta K_AB. BAN on kuitenkin konsistentti eli terve (sound), eli vain tosia kaavoja voidaan johtaa.

BAN-logiikasta on useita modifikaatioita, mm.:

GNY (Gong-Needham-Yahalom), monimutkainen rakennelma: ei oleta salatekstien redundanssia; osapuolen uskomien kaavojen lisäksi mallinnetaan hänen hallussaan olevien kaavojen joukko; mahdollistaa luottamuksen tason erittelyn.

AT (Abadi-Tuttle) muunnelma joka sisältää myös semantiikan

SvO (Syverson-van Oorschot), joka on yhdistelmä edellisistä ja BAN:sta itsestään. Tätäkin on jo kehitelty eteenpäin (tuoreimman version esittelyä PS:nä) Kaikissa näissä on sama idealisointiongelma. Siihen on tarjonnut lääkettä mm. Wenbo Mao artikkelissaan "An Augmentation of BAN-Like Logics" ( 8th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, June 1995, sivut 44-56 [PS]). Hän ehdottaa sääntöpohjaista tekniikka, jolla protokollan idealisoinnista tulee protokollan syntaksin symbolista manipulointia. Perusajatus on BAN-tyyppisten logiikkojen vaatiman yhden ison idealisointiaskeleen sijasta tehdä useita pieniä, jotka on helpompi ymmärtää ja saada oikein.

Luettavaksi: Steve Schneider: Security Properties and CSP, IEEE Symposium on Security and Privacy 1996, 174-189. Tässä artikkelissa on liikaa uutta asiaa, jotta sitä voisi käsitellä vastaavalla tarkkuudella kuin tämänkertaista. Ensi kerralla on sitä paitsi hieman yleistäkin asiaa. Siispä artikkeliin tosiaan kannattaa tutustua etukäteen. Jos CSP:stä haluaa pikalisätietoa voi selata johdannoksi (sivulta 6 alkaen) myös Carl Gunterin esitelmän kalvot, jotka löytyvät pakattuna PS:nä.