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
Käyttö ja rajoitukset. Logiikkaa käytetään pääasiassa autentikointiprotokollien ominaisuuksien, kuten todenmukaisuuden ja avaintenvaihdon oikeellisuuden, todistamiseen. Sen suurin