FORMAALIT MENETELMÄT (FOME)

Yleistä

 
Needhamin ja Schroederin avaintenvaihto-
protokolla säieavaruusmallissa,
kun vihollinen E suorittaa välimieshyökkäystä
Tutkimusryhmän tavoitteena on soveltaa formaaleja mallinnus- ja verifiointimenetelmiä hajautettuihin järjestelmiin ja tietoturvaan. Ryhmä on perustettu vuoden 2005 aikana. FOME jatkaa MOCO-ryhmässä aloitettua, traditionaalisiin verifiointimenetelmiin liittyvää tutkimustyötä, mutta painopiste on nykyään siirtynyt tietoturvaprotokollien verifiointiin.

Tutkimusalueet

Tällä hetkellä tutkimus keskittyy kolmeen aiheeseen. Traditionaalisella puolella jatketaan osittain määriteltyjen spesifikaatioiden tutkimusta. Uudempia alueita on piikalkyyli, erityisesti sen sovellukset tietoturvaprotokollien verifiointiin spiikalkyylin avulla. Kolmantena alueena ovat säieavaruudet, jotka on myös kehitetty tietoturvaprotokollien verifiointiin, joko manuaalisesti tai automaattisesti. Tulevaisuudessa tavoitteena on vielä perehtyä automaattiseen tai interaktiiviseen teoreemantodistukseen protokollien verifioinnin yhteydessä.

Henkilöt

Ryhmä koostuu tällä hetkellä seuraavista henkilöistä:
  1. FT Timo Karvi (ryhmän vetäjä)
  2. FM Päivi Kuuppelomäki
  3. FM Janne Rinta-Mänty
  4. FM Harri Forsgren

Opetus

Ryhmä vastaa tällä hetkellä kursseista Spesifioinnin ja verifioinnin perusteet, Tietoturva ja Verkkojen tietoturva. Jatkossa luennoidaan parin vuoden välein jatkokursseja sekä verifioinnista että tietoturvasta. Samoin järjestetään seminaari jommasta kummasta aiheesta joka lukukausi. Sekä verifioinnin että tieturvan formaaleista menetelmistä voi tehdä myös pro graduja.