BANlogiikka

BANlogiikka, eli Burrows–Abadi–Needhamin logiikka, on muodollinen menetelmä hajautetuissa järjestelmissä tapahtuvan todennuksen ja luottamuksen analysointiin. Se julkaistiin vuonna 1989 kolmikolta Burrows, Abadi ja Needham. Logiikan tarkoitus on mallintaa, mitä eri osapuolet uskovat toisistaan, sekä siitä, milloin jokin väite tai avaimen hallinnassa oleva tieto voidaan katsoa luotettavasti todistetuksi.

Keskeiset käsitteet ja notaatio. BANlogiikassa käytetään modal hokareita, jotka ilmaisevat osapuolten uskomuksia. Tavallisimmat ovat esimerkiksi “bp φ”, jolla merkitään, että osapuoli p uskoo väitteeseen φ, sekä “p sanoi φ”, mikä viittaa siihen, että p on kertonut tai esittänyt väitteen. Tuoreus (freshness) tarkoittaa, että viesti tai tapahtuma on uutta eikä sitä voida toistaa hyökkääjän toimesta. Salakirjoitus ja avaimet vaikuttavat, miten uskomuksia voidaan siirtää: jos osapuoli A uskoo, että avain K on ollut vain hänen ja B:n käytössä, ja hän näkee {X}K, voidaan päätellä X tai että B on once said X, riippuen kontekstista. BANlogiikassa on myös sääntöjä, joiden perusteella uskomuksia voidaan johtaa viestien rakennelmasta.

Käyttö ja rajoitukset. Logiikkaa käytetään pääasiassa autentikointiprotokollien ominaisuuksien, kuten todenmukaisuuden ja avaintenvaihdon oikeellisuuden, todistamiseen. Sen suurin hyöty on selkeys ja järjestelmällinen lähestymistapa. Rajoituksina se perustuu ideaalistuksiin kryptografiasta: se mallintaa salakirjoituksen ja avainten turvallisuutta usein yksinkertaistetusti, eikä se käsittele kaikkia aktiivisia hyökkäystapoja tai avaimien kompromissia yhtä kattavasti kuin myöhemmät muodolliset menetelmät. BANlogiikka on vaikuttanut laajemmin kehittyneisiin formaaleihin kieliin, kuten AB(L)P-logiikkaan, ja se on herättänyt huomion erityisesti tunnetuissa protokollatesteissä, kuten Needham–Schroederin protokollin analyysissä.