Kryptoprotokollat, luento 10 (B), 23.4.2008

Päivän artikkeli on: M. Burrows, M. Abadi, R.M. Needham: A logic of authentication. ACM Transactions on Computer Systems, 8(1), Feb 1990, 18-36. Tämä on 19-sivuinen julkaisu. Täysi 50-sivuinen raportti (1989) löytyy verkosta eri muodoissa. Luettavana olevaan versioon viitataan jatkossa "suppeampana".

Protokollien analysointi BAN-logiikalla

Burrowsin, Abadin ja Needhamin "A logic of authentication" on oikeastaan uskomusten logiikkaa, siis yhdenlaista modaalilogiikkaa. Sitä käytetään autentikointiprotokollien analysointiin. Tälläkin kurssilla protokollien saavutuksia on perusteltu juuri uskomusten avulla. Jos esimerkiksi uskot, että K on Ainon julkinen avain, niin saatuasi viestin, jonka salauksen voit purkaa K:n avulla, voit uskoa, että viesti on alunperin Ainolta. Yleisenä taustaoletuksena BAN-logiikassakin on, että viesteissä on aina riittävästi redundanssia sen havaitsemiseksi, oliko purkuavain oikea. Toinen yleinen taustaoletus on, että käytettyyn kryptosysteemiin voi luottaa eikä esim. salaisia avaimia ole vuotanut julkisuuteen.

Logiikan keskeisenä rakenteena on kaava "P believes X". Jos tämä kaava on tosi - eli se voidaan analyysin kuluessa johtaa tehdyistä oletuksista - se merkitsee, että osapuoli P voi toimia ikäänkuin X olisi tosi (vrt. Abadi-Needhamin periaate 2 "toimintaehdot").

Protokollan analyysissa on seuraavat vaiheet:

  1. Alkuperäinen protokolla idealisoidaan/abstrahoidaan sellaiseksi, että sen viestit ovat jäljempänä olevan notaation mukaisia logiikan kaavoja. Erityisesti jätetään pois sellaiset viestin osat, joita ei ole salattu. Vaikka ne ovat tärkeitä vihjeitä osapuolten tehokkaan toiminnan kannalta, niillä ei kuitenkaan voi olla merkitystä autenttisuuden kannalta, koska ne voivat olla väärennettyjä. Pois jätetään myös muu sellainen aines, joka ei voi vaikuttaa osapuolten uskomuksiin.
  2. Lähtötilannetta koskevat oletukset kirjataan, ts. loogisilla kaavoilla ilmaistaan, mitä uskomuksia milläkin osapuolella on. Nämä koskevat tyypillisesti osapuolten yhteisiä avaimia ja aikaleimojen tai nonce-arvojen tuoreutta.
  3. Protokollan vaiheet varustetaan niiden jälkeen vallitsevaa tilaa koskevilla loogisilla kaavoilla ("annotaatiot"). Viestin lähettäminen merkitsee tyypillisesti sitä, että tarkoitettu vastaanottaja sen jälkeen "näkee" joitain uusia kaavoja. Tässäkin on siis idealisointia sikäli, ettei viestien estämistä oteta huomioon.
  4. Päättelysääntöjä sovelletaan kohtien 2 ja 3 kaavoihin. Tuloksena saadaan tietoa siitä, mitä uskomuksia osapuolilla on protokollan suorituksen jälkeen (oikeastaan jo jokaisen vaiheenkin jälkeen).
Autentikointiprotokollan päämäärä voi eri yhteyksissä olla hieman erilainen. Yksi luonnollinen tavoite on tilanne, jossa A ja B autentikoivat toisensa ja tuloksena on vain heidän tiedossaan oleva symmetrinen avain K eli "A <-K-> B". Tämä tilanne voidaan formalisoida seuraavasti: A believes A <-K-> B ,   B believes A <-K-> B. Enemmänkin voidaan saavuttaa, esimerkiksi se, että B uskoo ensimmäisen näistä väitteistä ja A jälkimmäisen.

Johdatteleva esimerkki

Tarkastellaan pientä "protokollaa", jossa on vain yksi viesti:

A --> B:   {A, B, {TA, NAB}KA-1 }KB

Viestin tavoitteena on saada tiedosta NAB osapuolten A ja B välinen salaisuus siten, että (erityisesti) vastaanottaja B uskoo siihen. Idealisaatio näyttää seuraavalta:

A --> B:   {TA, "NAB on A:n ja B:n välinen salaisuus"}KA-1,

ja välitön käännös logiikan kielelle (suomeksi murtaen) on:

B näkee viestin, jossa A on kryptannut avaimella KA-1 kaavan ( TA, NAB on A:n ja B:n välinen salaisuus ).

Näissä julkisella avaimella KB kryptattu osuus on pelkistetty korvaamalla se sillä, mitä se tarkoittaa. Oleellisesti viestinä on siis A:n allekirjoittamana aikaleima ja jotain A:n tuntemaa ja sillä tavoin salaamaa, ettei se pääse kenenkään muun kuin B:n tietoon. Tämä pelkistys tarvitaan, koska uskomuksia koskeva päättely ei voi tuottaa tuloksena, että jokin on salaista. Luottamuksellisuushan on sitä, että kukaan ulkopuolinen ei tiedä eikä saakaan tietää. Miten tällaista voisi mallintaa sen perusteella että katsotaan, mitä jotkut tietävät - ellei sitten jo lähtökohtana ole, etteivät muut vielä tiedä jotain? Uskomusten käsittely tiedon sijasta ei muuta tätä asiaa.

Lähtötilanteena tälle protokollalle ja sen idealisaatiolle ovat seuraavat oletukset, joista muodostuvat samalla premissit loogiselle käsittelylle:

Ensi vaiheessa B varmaankin purkaa (sisemmän ja idealisaatiossa ainoan) kryptauksen. Tällöin hänen A:n avainta koskevan uskomuksensa seurauksena on tietenkin:

B uskoo, että A "sanoi" kaavan ( TA, NAB on A:n ja B:n välinen salaisuus).

Kyseessä on tavanomainen allekirjoituksen todentamistilanne, mutta logiikassa sitä varten tarvitaan erillinen päättelysääntö (joka kohta nähdään). Se, että joku sanoo jotain, pitää sisällään myös sen, että hän itse uskoo sanomansa. Kyseessä ei ole tämän protokollan idealisaatiota vaan varsin luonnollinen perusoletus itse logiikassa. Tässä kohden pitää sitten olla varuillaan, ettei pääse syntymään tilannetta jossa Abadi-Needhamin "prudent"-periaatteen 5 vastaisesti luultaisiin A:n uskoneen jotain sellaista, jonka hän on allekirjoittanut sen jälkeen, kun hän (tai joku!) on sen salannut.

Nyt siis B uskoo myös sen, että A sanoessaan uskoi kaavansa, mutta kuten on varoittavista esimerkeistä (toistohyökkäyksistä) opittu, B:n pitää varmistua A:n uskomuksen tuoreudesta eli siitä että A:n uskomus on edelleen voimassa. Tähän päästään välivaiheen kautta. Ensin B:n "alku-uskomus" aikaleiman tuoreuteen yhdistetään siihen, että aikaleima esiintyy osana pitempää kaavaa. Tällöin koko kaava uskotaan tuoreeksi:

B uskoo tuoreeksi kaavan ( TA, NAB on A:n ja B:n välinen salaisuus).

Kun tämä sitten yhdistetään siihen, että B uskoo A:n (joskus) sanoneen tällaisen kaavan, niin tietenkin nyt B uskoo, että A uskoo kyseisen kaavan. Luonnollisesti B uskoo A:n uskovan myös osakaavan eli sen, että NAB on A:n ja B:n välinen salaisuus.

Jotta B voisi nyt ryhtyä jatkotoimiin siinä uskossa, ettei kukaan muu tiedä NAB:tä, hänen pitää selvästikin luottaa A:n kykyyn hallita tällaisia salaisuuksia. Juuri tämä oletus tehtiin viimeisessä premississä.

Notaatio

Seuraavassa luetellaan rakenteet, joilla BAN-logiikan kieli eli kaavat muodostetaan. Kaikki merkinnät voisi esittää käyttäen pelkkiä symboleita tai pelkkiä sanoja, esim. #(X) = fresh(X). Tässä (ja suppeammassa artikkelissa) käytetään välimuotoa, jolla kaavat pysynevät paremmin luettavina (ja HTML-kirjoitettavina). Kielen vakio- ja muuttujasymbolit ovat kirjaimia, jotka on mahdollisesti varustettu tarkoituksesta vihjaavilla alaindekseillä. Ne jakautuvat luokkiin: osapuolet (P ja Q), avaimet (K) sekä viittaukset toisiin kaavoihin (X ja Y). Viimeksi mainittu yhdistelmä on erikoistapaus. Yleinen tapa ilmaista, että viesti tai väite koostuu osista, on merkitä osat sulkuihin pilkuilla eroteltuina, esim. (X,Y) koostuu osista X ja Y. Varsinaisesti tässä on kyseessä looginen konjunktio: Pilkku edustaa siis operaatiota AND.

Varsinaisesti syntaksi muodostuu pelkästään em. kaavoista ja niiden yhdistelemisen säännöistä, jotka ovat varsin yksinkertaiset: AND on ainoa konnektiivi ja "kontrolloituihin" avaimiin liittyy implisiittisesti kaikki-kvantifiointi: ts. jos palvelimen uskotaan hallitsevan avaimia, niin silloin uskotaan kaikkiin sen tuottamiin avaimiin. Merkintöjen selitykset puolestaan ovat semantiikkaa, jonka tehtävänä on sitoa syntaksin mukainen formaali kieli todellisuuteen, joskin idealisoituun sellaiseen. Artikkelin laajempi versio luonnostelee logiikalle myös formaalista semantiikkaa. Yleisesti kuitenkin BAN-logiikan semantiikka jää vain intuitiiviselle tasolle: Vaikka kaavat olisivat kuinka ymmärrettäviä, niiden "totuudelle" ei ole muita perusteita kuin ne itse - erityisesti ei siis mitään kuvausta sellaiseen mahdolliseen maailmaan, jonka olioiden välisiä relaatioita tutkimalla kaavan totuuden voisi määrittää. Jatkossa esiteltävät päättelysäännöt eivät edusta tällaista kuvausta, vaan ne ovat vain lisää intuitiivista syntaksia.

Tässä logiikassa ei oteta huomioon aikaa eikä tapahtumien rinnakkaisuutta saman protokollan sisällä. Ainoa erottelu on aikaisempien protokollien ja viestien mennyt aika ja nykyhetki, jota meneillään olevan protokolla kaikkineen edustaa.

Alustava esimerkki ja harjoitus. Wide-mouthed frog-protokolla:
Viesti 1   A--> S:   A, { TA, B, KAB } KAS
Viesti 2   S--> B:   { TS, A, KAB } KBS

Mitä tässä tapahtuu ja mitä oletuksia siihen liittyy?

Oletukset ovat uskomuksia, jollaisia useissa aiemmissakin protokollissa on tuotu esille, vaikka silloin tyydyttiin vain sanomaan esim. että A:lla ja S:llä on yhteinen symmetrinen avain KAS. Oletukset ovat nyt

Viestit näyttävät idealisoituina seuraavilta:
Viesti 1   A--> S:   { TA, A <-KAB-> B } KAS
Viesti 2   S--> B:   { TS, A believes A <-KAB-> B } KBS

Avaimen KAB erilainen ilmeneminen näissä viesteissä osoittaa, että idealisaatio ei ole kovin yksioikoista. Sitä olisi ilmeisen hankala automatisoida ainakaan suoraan. Tässä tapauksessa toisen viestin idealisaatio muodostuu luontevammin sen perusteella, millaisia uskomuksia ensimmäinen aiheuttaa S:ssä. Tällä tavoin idealisaatiovaihe ja sen jälkeinen päättely hieman lomittuvat toisiinsa.

Seuraavaksi esiteltäviä päättelysääntöjä käyttäen voidaan varsin suoraan johtaa uskomukset:

Tietenkään A ei voi tietää mitään B:n uskomuksista, koska ei saa häneltä viestejä. Vastaavalla tavalla kuin johdantoesimerkissä edellä, lopputulokseen ei päästä ilman voimakkaalta tuntuvaa oletusta B believes A controls A <-K-> B. Se, että B:n pitää luottaa S:ään, ei ole niinkään outoa, mutta A on tässä vain "tavallinen" osapuoli, ei mikään avainpalvelin. (Vrt. "prudent"-periaate 11.)

Päättelysääntöjä

Seuraavaksi esitellään säännöt, joilla aiemmista kaavoista (väitteistä) voidaan johtaa uusia. Nämä säännöt on luontevaa tosiaan ajatella päättelysäännöiksi. Varsinaisesti ne artikkelin mukaan ovat "postulaatteja" eli aksioomia (logiikkaan "vakiona" kuuluvia oletuksia). Logiikan "todellisia" päättelysääntöjä on vain kaksi: Ensinnäkin viestistä "P --> Q: X" voidaan päätellä että "Q sees X". Toisena on tuttu Modus Ponens (vrt. myös viime kerta), joka sanoo yksinkertaisesti: Jos X pätee ja X:stä voidaan johtaa Y, niin Y pätee. Tässä "voidaan johtaa" tarkoittaa juuri niitä "postulaatti"-päätelmiä, joihin seuraavaksi käydään käsiksi.

Viestin tulkintaa koskevat säännöt (message meaning rules): Voidaan päätellä "P believes Q said X", jos premisseinä on jokin seuraavista (muista, että pilkku tarkoittaa konjunktiota):

Viestin tuoreus johtaa uskomaan enempäänkin. Tämä on ainoa sääntö, jolla jokin sanottu ylennetään uskottuun asemaan (nonce verification rule):
Jos P believes fresh(X) ,   P believes Q said X,   niin   P believes Q believes X

Osapuolen luottamusta "controls"-auktoriteettiin kuvaa sääntö (jurisdiction rule):
Jos P believes Q controls X ja P believes Q believes X,   niin   P believes X.

Viestin osien näkemistä koskevat säännöt: Päätelmä "P sees X" voidaan tehdä, jos premisseinä on jokin seuraavista:

Osan tuoreus takaa kokonaisuuden tuoreuden eli:
Jos P believes fresh(X),   niin   P believes fresh(X,Y).

Edellä mainitut säännöt löytyvät tämän kerran artikkelin suppeasta versiosta. Laajemmassa versiossa on lisäksi sääntöjä, jotka koskevat viestin osia ja avainten tai salaisuuksien symmetriaa. Ensin mainittuihin liittyy havainnollisia huomautuksia siitä, millaiset säännöt eivät ole voimassa. Pätevät säännöt ovat:

Harjoitus: Mitä luonnolliselta tuntuvaa ei saa päätellä seuraavissa tilanteissa ja miksei?
  1. P believes Q said X ja P believes Q said Y
  2. P sees X ja P sees Y
Symmetriasäännöt ovat ilmeisiä ja ne jätetään kirjaamatta tähän.

Esimerkit

Artikkeleissa käsitellään kahdeksaa protokollaa. Noin kuudessa tapauksessa niiden tarkoituksena on sopia istuntoavaimesta siten, että sopijapuolet päätyvät jonkinlaiseen varmuuteen siitä, kenen kanssa sopimus tehtiin -- lyhyesti sanoen kyse on siis autentikoidusta avaimenvaihdosta.

Suppeassa artikkelissa analysoidaan neljä protokollaa mutta esitetään taulukkona tiivistelmä kaikista kahdeksasta. Mainitut neljä ovat:

Laajemmassa versiossa on lisäksi seuraavat neljä protokollaa ja näistäkin kaikista löytyy huomautettavaa. Kaikki neljä käyttävät symmetristä salausta ja autentikointipalvelinta. Käsitellään esimerkkeinä/harjoituksina:

BAN-logiikan kritiikkiä ja myöhempiä kehittelyjä

BAN on yksinkertainen ja intuitiivinen ja sen seurauksena tietenkin monin tavoin rajoittunut: Yksi syy viimeksi mainittuun on se, ettei BAN ole täydellinen (complete) eli on olemassa tosia kaavoja, joita ei voi johtaa päättelysäännöillä. ("Totuus" kuitenkin vain siinä intuitiivisessa mielessä kuin BAN-semantiikka tarjoaa). Yksi esimerkki tästä epätäydellisyyden ongelmasta on se, ettei havaita, että jollekulle muullekin kuin A:lle ja B:lle (ja palvelimelle) saattaa muodostua uskomuksia avaimesta KAB. BAN on kuitenkin konsistentti eli terve (sound), eli vain tosia kaavoja voidaan johtaa.

Kryptoteknik-kurssin (aiemman kuin 2005) tekijät tiivistävät BAN-kritiikkinsä seuraavasti:

BAN-logiikasta on useita modifikaatioita, mm.: Kaikissa näissä on sama idealisointiongelma. Siihen on tarjonnut lääkettä mm. Wenbo Mao artikkelissaan "An Augmentation of BAN-Like Logics" ( 8th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, June 1995, sivut 44-56 [PS]). Hän ehdottaa sääntöpohjaista tekniikka, jolla protokollan idealisoinnista tulee protokollan syntaksin symbolista manipulointia. Perusajatus on BAN-tyyppisten logiikkojen vaatiman yhden ison idealisointiaskeleen sijasta tehdä useita pieniä, jotka on helpompi ymmärtää ja saada oikein.

BAN-logiikka on sen verran yksinkertainen, että päättelyt on voitu rakentaa käsinkin. Työtä automatisoinnin hyväksi on kuitenkin tehty niin BAN:n kuin sen variaatioidenkin puitteissa. (esim. E.A. Campbell and R. Safavi-Naini, "On Automating The BAN Logic of Authentication", in Proc. Fifteenth Australian Computer Science Conference (ACSC '15), 1992.)

Alkuperäiseen BAN-artikkeliin on viitattu Citeseer-palvelun mukaan 292 muussa artikkelissa (tilanne huhtikuussa 2006). Kaikissa niissä ei logiikkaa suinkaan ole käytetty, vaan BAN on esim. mainittu yhtenä verifiointimenetelmänä. Yksi esimerkki BAN:n käytöstä on artikkelissa P.Papadimitratos, Z.Haas: Secure Routing for Mobile Ad Hoc Networks (Proc. of CNDS 2002). Yksi tuoreimmista käyttökohteista on IMKE-protokollan (IM key exchange) verifiointi artikkelissa M.Mannan, P.v.Oorschot: A Protocol for Secure Public Instant Messaging (2006). Kirjoittajat toteavat BAN-tekniikasta seuraavasti:

While BAN analysis is somewhat informal in certain aspects and is well-known to have shortcomings (...), it is nonetheless helpful in explaining the reasonings behind security beliefs of protocol designers, and often leads to security flaws being uncovered. However, a more rigorous security analysis as well as a proof of security of IMKE using alternate (non-BAN) techniques would be preferable to provide supplementary confidence. (Note however, that such a proof does not necessarily guarantee security; see Koblitz and Menezes ["Another look at provable security". J. of Cryptology (to appear, 2006).] for an interesting analysis of provable security.) We thus consider the BAN-like analysis to be a first step.
Artikkelissa ei esitetä todistusta rivi riviltä vaan kuvaillaan päättelyä sanallisesti. Lisäksi, kuten näkyy, kirjoittajat toteavat käyttävänsä BANin kaltaista logiikkaa. Muunnelmia on mahdollista tehdä, kunhan vakuuttaa lukijan päättelysääntöjen oikeutuksesta. Seuraavassa esimerkissäkin viitataan lisäsääntöjen tarpeellisuuteen joissain tilanteissa. Cremersin ym:n BAN-esittelyssä, johon viitattiin luennolla 10, otettiin käyttöön uusi merkintäkin, nimittäin sille että B sanoi X:n tässä protokollan ajossa. Se, että A uskoo tämän, vastaa tosin suoraan sitä, että A uskoo että B uskoo X:n.

Kertaava esimerkki: Anonymiteetti langattomassa viestinnässä

Tässä käsitellään luennolla 9A esillä olleen artikkelin BAN-todisteluja, autentikaatioprotokollan osalta.

Matkapuheluiden anonymisointiprotokollan perusidea kerrattuna: Tilaaja suorittaa ennakkomaksun ja saa sen perusteella sokeasti allekirjoitetun lippu, jolla hän voi myöhemmin autentikoitua viestintäpalveluun ilman, että häntä pystytään tunnistamaan. Laskutus tapahtuu siten, että lippu toimii indeksinä nimettömään tiliin, jolle ensimmäisellä palvelun käyttökerralla talletetaan tunnetun ennakkomaksun verran rahaa, jota sitten vähennetään käytön mukaan.

Merkinnät ja idealisaatio
Oletetaan, että lippu on jo hankittu, eikä puututa sen rakenteeseen, eikä myöskään anonymiteettiin, vaan aloitetaan autentikointiprotokollan idealisaatiosta ja vielä sitäkin ennen protokollan taustalla olevista oletuksista (suluissa on niiden artikkelin mukainen kirjaimointi).

Ensinnäkin osapuolet ovat
S = subscriber, tilaaja
H = HSD, home service domain, palvelu jonne S on rekisteröitynyt
V = VSD, visiting service domain, vieras palvelu, jonka alueella S haluaa käyttää matkaviestintään.

Autentikoinnin tarkoituksena on luoda S:n ja V:n välille istuntoavain Ki (vastaten i:nnettä puhelua), eli formalisoituna tavoite on

S believes S <-Ki-> V ja V believes S <-Ki-> V

Avaimen Ki voi laskea S:n keksimästä satunnaisluvusta ri ja S:n ja H:n yhteisestä salaisuudesta Ksh (jonka S on ostanut H:lta ja joka ei identifioi S:ää. Se on itse asiassa sama kuin lippu H:n allekirjoittamana). Salaisuutta koskevat oletukset ovat (joskaan ei artikkelissa):

(ä) S believes S <=Ksh=> H
(ö) H believes S <=Ksh=> H

Avaimen Ki saattaminen S:n ja V:n väliseen käyttöön on H:n toimintaa, ja siihen liittyvät seuraavat oletukset (joissa avainta ei pitäisi spesifioida alaindeksillä i, toisinkuin artikkelissa):

(a) S believes H controls S <-K-> V
(b) V believes H controls S <-K-> V

Toimen tekee mahdolliseksi yhtäältä se, että H:lla on käytössään Rabinin julkisen avaimen kryptosysteemi eli oleellisesti moduli m, joka on kahden suuren tietynlaisen alkuluvun tulo. Rabin-salaus on neliöön korottamista modulo m ja merkitään jatkossa {..}2m. (Artikkelissa m:n tilalla on er ja sen tekijätkin on mainittu, eli salaiset alkuluvut pr ja qr, mutta niitä ei tarvita tässä). Julkista avainta m koskeva oletus on:

(h) S believes -m-> H

Toisaalta H:lla ja V:llä on yhteinen avain Kvh (kohdassa c artikkelissa lienee virhe):

(c) H believes V <-Kvh-> H
(d) V believes V <-Kvh-> H

Viestit H:lta V:lle salataan tällä avaimella niin tässä kuin muissakin protokollissa. Toisinpäin eli V:ltä H:lle näin ei tehdä, sillä kyseessä on vain S:ltä tulleiden viestin forwardointi, minkä lisäksi V vain liittää mukaansa keksimänsä nonce-luvun. Tässä protokollassa kyseinen luku sattuu olemaan numeroltaan 4. Sitä ja S:n lähettämää satunnaislukua ri koskien tarvitaan tuoreusoletus:

(f) V believes fresh(N4)
(g) S believes fresh(ri)

Autentikointiprotokollan idealisaatio on seuraava

1. S --> V:   { ri , S <=Ksh=> H }2m
2. V --> H:   { ri , S <=Ksh=> H }2m
3. H --> V:   { ri , S <-Ki-> V, N4 }Kvh
4. V --> S:   { ri , S <-Ki-> V }Ki

Ensimmäisellä idealisoidulla viestillä ei ole oikeastaan mitään vaikutusta uskomuksiin, sillä V ei saa sitä auki. Toisen viestin vaikutuksen artikkeli on ottanut mukaan jo oletuksiin siten, että S:n ja H:n uskomus salaisuuteen Ksh (kuten edellä kirjattiin) on samantien korvattu sillä, mihin he päätyvät laskiessaan Ki:n ri:stä ja Ksh:sta:

(e) S believes S <-Ki-> H
(i) H believes S <-Ki-> H

Tämä on sangen uskottavaa, mutta sitä ei voisi päätellä pelkillä BAN-logiikan säännöillä! Sitä varten tarvittaisiin ilmeisesti lisäsääntö, jolla salaisuutta voi käyttää avaimen laskentaan. Siihen varmaankin tarvittaisiin myös lisäoletus, että laskussa on mukana jotain tuoretta. Tässä tapauksessa se on lähinnä ri (sillä Ksh:n elinaika voi olla pitkäkin), mutta sitä ei voi ratkaista yksin tämän protokollan puitteissa: Protokollaa esittäessään artikkeli mainitsee ehdoksi viestin 2 hyväksymiselle, että H ei löydä ri:tä aiemmin Ksh:n kanssa käytettyjen lukujen joukosta.

Kun äskeiset Ki:tä koskevat S:n ja H:n uskomukset on saatu aikaan (eli oletettu), jatko sujuu varsin loogisesti, aiemmin opitun perusteella. (Huomaa, että oletuksia ä, ö, h, c ja i ei käytetä: kolmen ensimmäisen voi ajatella tuottaneen äskeiset e:n ja i:n, minkä jälkeen H:n uskomukset eivät enää vaikuta S:n ja V:n uskomuksiin.)

Viestin 3 ja oletusten (d), (f) ja (b) perusteella voidaan johtaa vaiheittain seuraavat uskomukset V:lle:

V believes H said (ri , S <-Ki-> V, N4)
V believes H believes (ri , S <-Ki-> V, N4)
V believes S <-Ki-> V

Konkreettisen protokollan esittämistä ajatellen tässä kannattaa huomata nonce-luvun N4 rooli: Tuntuu oudolta, että V vastaanottaa sen ja noin vain uskoo sen tuoreuteen. Selvästi jokin tällainen tuoreususkomus tarvitaan, jotta sanomuksen tasolta päästäisin uskomuksen tasolle ja sikäli N4 on aivan oikeassa paikassa. Sen tuoreusoletus on osa protokollan idealisaatiota: V on todellisuudessa itse lähettänyt sen viestissä 2, joten hän pystyy kyllä tarkastamaan, onko viestissä 3 salattuna palautuva N4 sama ja siis tuore.

Vastaavasti viestin 4 ja oletusten (e), (g) ja (a) perusteella artikkeli johtaa seuraavat uskomukset S:lle:

S believes H said (ri , S <-Ki-> V)
S believes H believes (ri , S <-Ki-> V)
S believes S <-Ki-> V

Tässä vastaava tuoreusseikka näkyy idealisoidussakin protokollassa (ri viestissä 1). Onko analyysissa kuitenkin jotain vialla? Saavutetusta uskomuksesta S believes S <-Ki-> V voidaan nimittäin nyt johtaa
S believes V said (ri , S <-Ki-> V),
mikä oikeastaan vastaakin paremmin sitä, mitä viestissä 4 tapahtuu. Onko siis mahdollista, että S uskoo sekä H:n että V:n sanoneen täsmälleen saman asian, vaikka varmaankin vain toinen sen sanoi?

Päättely on kyllä logiikan mukainen, eli kunnossa. Ongelma lieneekin lähinnä BAN-logiikassa itsessään ja nimenomaan sen puutteellisessa semantiikassa. Pitäisi pystyä tarkastamaan semanttisesti eikä vain päättelysäännöistä, tarkoittaako "H said X" tosiaan sitä miltä se englannin kielellä näyttää.

Mikäli tämän kirjoittaja olisi laatinut protokollan, ensimmäisenä epäiltyjen listalla ei toki olisi BAN, vaan protokollan idealisaatio ja seuraavaksi itse protokolla. Edellä sanotusta riippumatta protokollassa voi tietenkin olla jokin sellainen aukko, jota BAN-logiikka ei pysty löytämään.