BANlogiikassa

BAN-logiikka (Burrows-Abadi-Needham logiikka) on formaali menetelmä autentikointiprotokollien arviointiin. Sen kehittäjät ovat Burrows, Abadi ja Needham, ja se julkaistiin vuonna 1989. Logiikan tavoitteena on mallintaa, mitä uskovat eri osallistujat protokollan aikana ja millaisia luottamussuhteita syntyy vastaanotettujen viestien perusteella. BAN-logiikka kiinnittää erityistä huomiota siihen, missä määrin viestien alkuperä ja aitous voidaan todentaa, sekä siihen, millaisia luottamusväitteitä voidaan johtaa saatujen viestien perusteella.

Keskeiset käsitteet ovat osanottajat (protokollan osapuolet), uskomukset (believes), näkeminen (sees) ja tuoreus (fresh). Logiikassa käytetään modaalisia lausekkeita ilmaisemaan, että esimerkiksi tietty osapuoli uskoo jonkin väitteen olevan tosi, tai että hän pitää jonkin avaimen hallinnassaan. Lisäksi BAN-logiikassa korostetaan viestin tuoreutta sekä avainten valvontaa (control), jotka vaikuttavat siihen, millaisia johtopäätöksiä voidaan tehdä. Näiden avulla voidaan päätellä, onko protokolla todentanut viestin alkuperän ja eheyden.

Soveltamisena BAN-logiikkaa käytetään erilaisten autentikointiprotokollien analysointiin sekä ymmärtämään, millaiset oletukset ja rajoitteet johtavat oikeisiin tai harhaanjohtaviin uskomuksiin. Logiikan oletukset ovat ideaalitynyys kryptografiassa: avaimet ovat oikein jakautuneet, viestit eivät ole muokattavissa, ja uudet viestit ovat todellisia. BAN-logiikka on historiallisesti vaikuttanut protokollien turvatarkasteluun, mutta sitä on kritisoitu sen rajoitusten vuoksi sekä siitä, että se ei yksin ratkaise kaikkia protokollien turvallisuushaasteita.