Autentikaatiotestien merkitys suunnittelun kannalta on suurinpiirtein, että tietynlaisia viestejä on syytä esiintyä, jotta voidaan olla varmoja, että laillinen eli autenttinen osapuoli on muokannut niiden tietoja, kun ne myöhemmin esiintyvät jossain viestissä tietyllä tavalla muuntuneina. Testit ovat oikeastaan vain haaste-vaste -menettelyn ranta-avaruudellisia formalisointeja: "lähtevä" testi sisältää salauksen purun ja "tuleva" testi allekirjoituksen ('outgoing' ja "incoming test'). Hyötynä on nimenomaan testien formaalisuus, jonka kautta niitä voi helposti käyttää todistuksissa. Lisäksi testit ovat sillä tavoin yleisiä, ettei niissä vaadita, että vastapuoli heti seuraavassa viestissään palauttaa vasteen.
Artikkelissa esitetään ranta-avaruuksien piirteitä tiiviisti, ja tässä tekstissä esitellään vain keskeiset käsitteet johdannoksi. Alkuperäinen strand space -artikkeli on
Termit ovat siis viestejä, joita osapuolet voivat vaihtaa keskenään tarkasteltavana olevassa protokollassa. Niiden rakentuminen osatermeistä määritellään mallissa tuttuun tapaan mutta tarkasti (Liite A.3) ja se on keskeistä krypto-operaatioiden kannalta. Artikkelissa mainittu 'transformation edge' on siirtymä, jossa jokin krypto-operaatio tapahtuu. Sitä ei piirretä graafeihin millään erityisellä tavalla mutta tekstissä siitä käytetään aaltonuolta. Yksi tapa rakentaa termejä on tietenkin avainten käyttö. Avaimet eivät kuitenkaan ole osatermejä, ellei niitä itseään siirretä salattuna jollain toisella avaimella (tai salaamatta, mitä tuskin on tarkoitus tehdä).
Ranta ('strand') on graafissa sellainen solmujen kautta kaarien välityksellä kuljettu polku, joka kuvaa yhden protokollaan osallistuvan osapuolen suorittamaa täydellistä lähetys- ja vastaanottotapahtumien sarjaa. Ranta muodostuu siis kaksinkertaisten viivojen yhdistämistä solmuista. Hyökkääjää varten on omat termien muodostamisen sääntönsä normaaliin Dolev-Yao -tyyliin. Näin muodostuu hyökkääjän rantoja ('penetrator strands'). Laillisten osapuolten rantojen sanotaan olevan säännöllisiä ('regular').
Ranta-avaruus on kaikista mahdollisista rannoista muodostuva graafi. Verifioinnin tarkastelut koskevat koko graafin sopivasti valittuja osia, joista käytetään nimeä kimppu ('bundle'). Sellainen on periaatteessa mikä tahansa äärellinen aligraafi, jossa jokainen mukana oleva ranta on mukana ensimmäisestä ("ylimmästä") solmustaan asti, ei silti välttämättä loppuun asti. Kimppu edustaa siis protokollan kokonaista ajoa, mahdollisesti hyökkääjän kanssa. Jälki ('trace') on jonkin protokollan "kulkema polku" graafissa johonkin tiettyyn solmuun asti. Varsinaisesti jälki muodostuu tällä polulla esiintyvistä termeistä etumerkkeineen (Liite A.1).
Solmujen välinen edeltämisrelaatio ('precedence') on ilmeinen. Se ei erottele nuolien laatua. Erikoisempi solmujen suhde on taannoisuus ('recency'). Artikkelissa määritellään induktiivisesti, milloin jokin solmu on toiselle n-taannoinen (n=1,2,...). Intuitiivisesti, säännölliselle solmulle x ovat n-taannoisia solmuja sellaiset, joista on x:ään n:n tai useamman askelen mittainen tietynlainen polku. Ehtona polulle tai oikeastaan siinä taaksepäin laskettaville askelille on, että kukin niistä sisältää siirtymän samassa rannassa -- siis yhden ==>-nuolen. Vaikka välillä olisi viestisiirtymiä rantojen välillä, ensimmäinen taannoisuusaskel otetaan samassa rannassa kuin x itse on. Toinen taannoisuusaskel voi tapahtua ("olla tapahtunut") jossain muussa rannassa kahden solmun välillä. Koko ajan siis seurataan tavallista siirtymäpolkua (nuolia) taaksepäin.
Taannoisuus sisältyy autentikaatiotesteihin, vaikka sitä ei niissä mainita. Käsite tarvitaan artikkelin esittämään mutkikkaampaan tietoturvatavoitteeseen, jolla on nimenä "Authentication II". Siinä edellytetään vakuuttumista saadun viestin tuoreudesta. Taannoisuuslaskelmat ovat kätevä tapa todeta, että protokolla toteuttaa tällaisen vaatimuksen. Tässä tapauksessa löytyy 2-taannoinen solmu, jossa viestin ainekset on pantu alulle (kuvassa Fig.4).
Ranta-avaruus -menetelmän tutkimuksesta ja sovelluksista, mm. automatisointiyrityksistä, saa käsityksen menetelmän kotisivulta. "Perinteinen" automaattinen työkalu ranta-avaruuksien "kartoittamiseen" on nimeltään Athena (D.Song 1999). Se yhdistää mallintarkastusta ja logiikkaa. Rantojen tiettyjen ominaisuuksen ansiosta se säästyy osalta tilaräjähdystä. Athenan tekee mielenkiintoiseksi myös sen yhteyteen rakennettu automaattinen protokollageneraattori (APG; Perrig & Song 2000).
Yksi tuoreimmista rantahankkeista näyttää olevan jälleen uuden protokollaohjelmointikielen laatiminen: cryptographic protocol programming language, cppl, artikkelissa
Trust Engineering. A domain specific language for cryptographic protocols raises the question, however, why programmers need to create new protocols. Although there could be several answers to this, one specific answer motivated our work on cppl. When a programmer must implement a transaction in a distributed application, cppl allows him to engineer a protocol to achieve the specific authentication and confidentiality goals needed by this transaction. This process--the process of shaping a transaction so that it can reflect the trust goals of its participants--we call trust engineering.
Muut päivän artikkelin yhdistelyt saadaan aikaan "automaattisesti" sen ansiosta että protokollat ovatkin oikeastaan toisistaan riippumattomia, nimittäin siinä mielessä, että niissä toteutuu vahvasti erillinen salaus ('strongly disjoint encryption', luku 4.2). Se tarkoittaa, että vaikka avain olisi sama, kahta samanlaista kryptotekstiä ei voi esiintyä kahdessa eri protokollassa. Tämä saavutetaan yksinkertaisesti sillä, että jokaisessa selkotekstissä on protokollan tunniste mukana.
Tutkijat toteavat pyrkivänsä yhdistämään parhaat palat tähänastisista kahdesta kryptoprotokollien todistamisen tavasta, jotka ovat yhtäältä kryptografiset reduktiot ja toisaalta formaalit menetelmät. Edelliset pitää tehdä ihmisvoimin ja toisissa voidaan käyttää koneita kuten mallintarkistajia ja teoreemantodistajia.
Artikkelin raportoimassa työssä on pystytty todistamaan, että tekijöiden laatima (mallintama) todellinen kryptografinen kirjasto on yhtä turvallinen kuin ideaalinen kryptografinen kirjasto. Tulos ilmaistaan seuraavassa muodossa: kun asetetaan reaalisessa kirjastossa hyökkääjän paikalle polynomiaikainen simulaattori ja ideaalisessa kirjastossa polynomiaikainen simulaattori, tarkkailijan on laskennallisesti mahdotonta erottaa tapauksia toisistaan. Käytännön merkitys on, että protokolla, joka on todistettu turvalliseksi ideaalisen kirjaston pohjalta, voidaan turvallisesti toteuttaa todellisen kryptografisen kirjaston avulla.
Vaikka todistus vaatikin suurimman työn, varsinaisia aikaansaannoksia ovat ideaalinen ja reaalinen kryptokirjasto, joita teoreema koskee. Ideaalista kirjastoa voidaan käyttää mallintamaan kryptoprotokollan ympäristöä, kun tarvitsee todistaa kyseisen protokollan turvallisuus. Uutta tässä on Dolev-Yao -malliin verrattuna se, että hyökkääjällä on käytössään aktiivisia hyökkäyksiä ja että operaatiot tukevat sisäkkäisiä operaatiokutsuja, siis esim. salatun tekstin allekirjoittamista. Reaalista mallia voidaan käyttää kryptoprotokollan toteutusvaiheessa, kun on ensin todistettu protokolla ideaalisen mallin pohjalta ja halutaan varmistaa, että myös toteutus on turvallinen.
Ideaalinen kirjasto tarjoaa tavallisille käyttäjille ja hyökkääjälle hieman erilaisia operaatiota. Edellisille on tarjolla salaus, salauksen purku, allekirjoitus, sellaisen tarkistus ja satunnaisluvun (noncen) luonti. Hyökkääjällä on käytössään operaatiot virheellisen merkinnän lisäämiseen, virheellisen salatekstin luomiseen, allekirjoituksen muuttamiseen, ei-salaisen tiedon keräämiseen ja datan lähettämiseen. Lisäksi malli sallii, että hyökkääjällä on käytössään aktiivisia hyökkäykeinoja kuten man-in-the-middle ja lähetetyn viestin uudelleenkäyttö protokollan myöhemmässä vaiheessa.