Väitös tietotekniikan alalta, DI Aleksi Peltonen

Väitöskirjan nimi: Formal Verification and Standardization of Security Protocols

Tohtoriopiskelija: Aleksi Peltonen
Vastaväittäjä: Prof. Kristian Gjøsteen, Norwegian University of Science and Technology (NTNU), Norja
Kustos: Prof. Tuomas Aura, Aalto-yliopiston perustieteiden korkeakoulu, tietotekniikan laitos

Linkki väitöskirjan sähköiseen esittelykappaleeseen (esillä 10 päivää ennen väitöstä): https://aaltodoc.aalto.fi/doc_public/eonly/riiputus/

Kryptografisten protokollien tietoturvan verifiointi

Suojattu viestintä avoimissa verkoissa on tärkeä osa monia nykyaikaisia tietojärjestelmiä. Aiemmin keskitetyt arkkitehtuurit ovat entistä riippuvaisempia hajautetuista järjestelmistä ja niiden välisestä tiedonsiirrosta internetin välityksellä. Tämän seurauksena turvallisten, luotettavien ja tehokkaiden salausprotokollien tarve on kasvanut merkittävästi. Kysyntää lisää entisestään uusien teknologioiden, kuten esineiden internetin, ilmaantuminen. Aiemmin itsenäisten laitteiden vaaditaan nyt toimivan vuorovaikutuksessa keskenään tai muodostavan yhteyden etäpalvelimiin. Lukuisat tietoturvahyökkäykset ovat osoittaneet, että yhä monimutkaisempien järjestelmien tietoturvariskien havaitseminen on vaikeaa ja ne voivat jäädä huomaamatta jopa vuosien ajan. Formaalit verifiointimenetelmät mahdollistavat protokollien tietoturvan analysoinnin jo ennen niiden käyttöönottoa. 

Tämä väitöskirja osoittaa, kuinka formaalia verifiointia voidaan käyttää kryptografisten protokollien kehitys- ja standardointiprosessin aikana kriittisten haavoittuvuuksien välttämiseen ja ongelmien havaitsemiseen. Sen lisäksi, että analysoimme protokollastandardeja tunnettujen haavoittuvuuksien varalta, pyrimme myös tunnistamaan uusia heikkouksia ja hyökkäyksiä. Työn tutkimustavoitteita on kaksi: (1) tunnettujen ja laajalti käytössä olevia suojausprotokollien analysointi haavoittuvuuksien havaitsemiesi ja (2) havaittujen heikkouksien perusteella opittujen kokemusten hyödyntäminen tietoturvaprotokollan standardoinnissa. Työ voidaan näin ollen nähdä osana aloitetta, jonka tarkoituksena on vahvistaa salausprotokollien turvallisuutta, ja osoituksena formaalien verifiointimenetelmien hyödyllisyydestä standardointiprosessissa.

Yhteystiedot:

Perustieteiden korkeakoulun väitöskirjat: https://aaltodoc.aalto.fi/handle/123456789/52