Kryptoprotokollat, luento 11 (B), 30.4.2008

Prosessien algebraan johdateltiin jo luennolla 9B.

Tämän jakson taustalla on useita artikkeleita, jotka valottavat samaa asiaa hieman eri näkökulmista:

Pikajohdanto CSP:hen löytyy Wikipediastakin. Keskeisiä CSP-lähteitä ja työkalujakin on mainittu sivulla CSP-archive. Tuoreehko yleisesitys on Schneiderin ja Delicatan artikkeli Verifying Security Protocols: an Application of CSP (CSP, the first 25 years, LNCS 3525, 2004). Hyvin kattavan näkemyksen saa Peter Ryanin ja Schneiderin kirjasta Modelling and analysis of security protocols (Addison-Wesley, 2001).

CSP kryptografisten protokollien mallinnuksessa

Johdantoa

Viime kerralla esitetyssä BAN-logiikassa analyysin vaiheet olivat: protokollan idealisaatio uskomuksia käsitteleviksi (ajattomiksi) kaavoiksi, alkuoletusten kirjaaminen, tavoitelauseiden johtaminen päättelysäännöillä. Prosessialgebrassa ei esiinny uskomuksia vaan tapahtumia ja niiden ketjuja. Protokolla mallinnetaan nyt määrittämällä osapuolet, hyökkääjä ja verkko (media) prosesseiksi, joissa tapahtumina ovat tietynmuotoiset viestit, jotka "lähetetään" kanavia pitkin. Mitään lähetyksiä ei tietenkään tapahdu ja puhe kanavista on vain havainnollistus.

CSP (communicating sequential processes) on abstrakti kieli, jolla kuvataan rinnakkain toimivia ja viestien vaihdon avulla kommunikoivia järjestelmiä. Ne koostuvat prosesseista, jotka "elävät" tapahtumien (events) kautta. Prosessit ilmaisevat, millaisia tapahtumia voi sattua ja miten ne asettuvat toistensa perään tai rinnalle. Osa tapahtumista on sellaisia, jotka synkronoivat eri prosesseja. Tällaiset on luontevaa tulkita viestien lähettämiseksi ja vastaanottamiseksi, mutta se ei ole ainoa mahdollisuus.

Tietoturvatavoitteet mallinnetaan asettamalla vaatimuksia sille, millaisia tapahtumaketjuja eli jälkiä ('traces') tällaisessa systeemissä voi esiintyä. Siis kaikkien mahdollisten tapahtumaketjujen pitää toteuttaa joitakin ominaisuuksia. Tämä riittää luottamuksellisuuden ja autenttisuuden mallintamiseen. Jos halutaan tutkia kiistämättömyyttä tai saatavuutta, joudutaan vaatimaan myös sitä, että tietynlaiset tapahtumaketjut ovat mahdollisia, tai siis että jotkin tapahtumat tosiaan toteutuvat. Tätä varten pitää ottaa huomioon, millaisia estymiä ('failures') prosesseissa voi esiintyä. Tällä luennolla tyydymme 'traces'-tyyppiseen semantiikkaan.

Prosessin (jälki-)semantiikalla tarkoitetaan siis kaikkia mahdollisia tapahtumaketjuja, jotka se voi suorittaa. Jälkiä koskevat vaatimukset voi tarkistaa todistamalla ne muodollisesti tai käyttämällä automaattista mallintarkistajaa (model checker) FDR. Se ei oikeastaan tarkista yhtä mallia, vaan vertailee kahta prosessia P ja Q. Vertailussa selviää, onko P hienonnus (refinement) Q:sta eli sisältyykö P:n semantiikka Q:n semantiikkaan. Lähtökohta Q mainitaan usein spesifikaatioksi, jota implementaatio P sitten hienontaa. Kun nyt puhumme vain jäljistä, P on hienonnus Q:sta, jos jokainen P:lle mahdollinen tapahtumaketju on mahdollinen myös Q:lle -- eli implementaatiossa ei tapahdu mitään sellaista mitä ei ole spesifioitu.

Nimi FDR tulee sanoista Failures Divergences Refinement. Failures mainittiin edellä ja divergence eli pillastuma tarkoittaa ikisilmukkaa; yleisessä semantiikassa pitää nekin ottaa huomioon. FDR toimii siten, että se käy läpi tietyn tila-avaruuden kaikki tilat ("jälkiä seuraten"). Näin ollen se voi käsitellä vain äärellistilaisia systeemejä (muutamaan miljoonaan tilaan asti). Siispä menetelmää voidaan käyttää vain sellaisen systeemin tutkimiseen, jossa on rajattu määrä osapuolia, käytännössä vain muutama. Protokollan sinänsä pitää toimia käytännössä rajattoman toimijajoukon puitteissa. Oxfordin yliopistossa kehitetty FDR on nykyään kaupallinen tuote: FDR2-sivulta voi koodia ladata myös kokeiltavaksi.

Kieli

CSP:n kieli pohjautuu siis tapahtumiin. Niistä muodostuvat prosessien aakkostot. Prosesseja (aluksi siis yksittäisiä tapahtumia) yhdistellään seuraavilla operaattoreilla: Prosessien määrittelyssä voidaan käyttää myös seuraavia jossain määrin ohjelmointia muistuttavia rakenteita: Koska tapahtumat ovat protokollissa kommunikaatiota, niihin täytyy saada mahtumaan myös dataa. Tätä varten tapahtuma-aakkostolle kehitellään rakennetta kirjoittamalla tapahtuman komponentit peräkkäin välimerkein eroteltuina, esim. c.d.e. Yleensä ensimmäinen komponentti (c) nimeää kanavan ja viimeinen komponentti (e) siinä kulkevan viestin. Sen mukaan onko kulloisenkin prosessin kannalta kyseessä vastaanottaminen vai lähettäminen, välimerkkinä on '?' tai '!'.

Esimerkiksi COPY = in?x --> out!x --> COPY on prosessi, joka saatuaan kanavasta 'in' viestin x lähettää saman x:n kanavaan 'out', minkä jälkeen se palaa odottamaan uutta viestiä. Algebran kannalta voisi tietysti kirjoittaa in.x ja out.x tai vain a.x ja b.x, jolloin COPYn kanssa synkronoituvassa prosessissa olisi myös a.jotakin ja b.jotakin. Oleellista on kuitenkin, että x edustaa muuttujaa, jolle on alussa määritelty tyyppi eli mahdollisten arvojen joukko. Siksi COPY voi saada jonkin tähän kuuluvan arvon x:ksi tapahtumassa in.x ja osallistuu seuraavaksi tapahtumaan out.x, missä x on sama.

Kanavien nimeämisen tarkoituksena on havainnollisuus, mutta sellaisten kuin in ja out (tai rec ja trans) tapauksessa tarvitaan joustavaa mielikuvitusta. Niiden avulla synkronoivissa prosesseissa ne ovat sama tapahtuma, joten jommassakummassa ne menevät "väärinpäin". Kryptoprotokollien tapauksessa tapahtumien komponentteina esiintyvät yleensä myös (väitetty) lähettäjä ja (tarkoitettu) vastaanottaja. Esimerkiksi protokollan askel A --> B: m mallinnettaisiin artikkelin mukaisesti kahdella tapahtumalla, trans.A.B.m ja rec.B.A.m. Prosessit A ja B eivät ole tekemisissä toistensa kanssa näillä tapahtumilla, vaan edellinen on A:n tapahtuma, jolla se synkronoituu välitysprosessin (mediumin) kanssa ja jälkimmäinen on vastaavasti B:n tapahtuma. Kumpikin tapahtuma kuuluu siis tietysti myös välitysprosessin aakkostoon.

Tapahtuman kukin komponentti voi saada arvonsa tietotyyppinsä mukaisesta joukosta. Tällainen joukko voidaan myös merkitä tapahtuman komponentin tilalle, jolloin tuloksena on lyhennysmerkintä usean tapahtuman joukolle. Jos esim. i on tyyppiä U={0,1,2}, niin merkintä c.U.m tarkoittaa joukkoa {c.0.m, c.1.m, c.2.m} ja c.i.m on jokin tämän joukon alkio.

Keskeinen asema mallinnuksessa on tapahtuman sillä komponentilla, joka edustaa viestin sisältöä. Esimerkiksi artikkelissa parametrisoidaan osapuolten välinen prosessi MEDIUM sen mukaan, mikä joukko viestejä siinä kulloinkin on sisällä. Tämä joukko kasvaa, vähenee tai pysyy ennallaan tapahtumien edetessä. Hyökkääjäprosessilla on parametrinaan sen haltuun päätyneiden viestin joukko. Tämän joukon käsittelyssä otetaan huomioon myös se, että hyökkääjä pystyy johtamaan uusia viestejä aiemmin kuulemistaan, ja sitten myös lähettämään näitä. Jos jokin tieto m on johdettavissa aiempien tietojen joukosta S, merkitään S |- m. Relaation |- perusominaisuudet ovat varsin ilmeiset, mutta eri tilanteita (esim. erityisiä kryptosysteemejä) varten voidaan sen noudattamia sääntöjä täydentää.

Mallinnusta lähemmin

Seuraavassa tutkitaan CSP-koodia, jolla Schneider (97) mallintaa Needham-Schroederin julkisen avaimen protokollan alkaen siitä kohdasta, jossa A ja B ovat hankkineet toistensa julkiset avaimet (pA ja pB). Tässä piste "." toimii erottimena tietokenttien välillä ja toisen viestin lopussa oleva B on korjaus protokollan alkuperäiseen versioon. Protokolla on:
A --> B : pB(nA.A)
B --> A : pA(nA.nB.B)
A --> B : pB(nB)

Tässä mallissa oletetaan yksinkertaisuuden vuoksi, että osapuolia A ja B vastaavat prosessit "tietävät" kumpikin roolinsa eli sen että A on aloittava ja B vastaava osapuoli. Ne toimivat mallissa rinnakkain kommunikoimatta keskenään suoraan. Kanavat trans ja rec yhdistävät ne "väliaineen" kautta (kukaties) toisiinsa. Päivän artikkelissa hyökkääjä on mallinnettu omana prosessinaan, mutta tässä mallissa hän hoitaa samalla väliaineen virkaa. Tämä tuntuu dramaattiselta, mutta kuvaa varsin hyvin sitä, mistä tietoverkon paljon puhutussa turvattomuudessa on kyse.

NET = (UserA ||| UserB) |[ trans, rec ]| ENEMY

Ennen osapuolen A prosessin alkua A valitsee joukosta USER alkion i ja aloittaa sitten lähettämällä sille tarkoitetun viestin. (Tässä on siis useita muuttujan i avulla parametrisoituja prosesseja liitetty toisiinsa valinta-operaattorilla.)

UserA = []i: USER
trans.A!i!pi(nA.A) -->
rec.A.i?pA(nA.x.i) -->
trans.A!i!pi(x) --> Stop.

Osapuoli B aloittaa, kun sen vastaanottokanavassa esiintyy tapahtuma. B saa siitä tietoonsa, että se näyttäisi tulevan j:ltä. Viestin sisällöstä opitaan muuttujan y arvo, mutta vain jos se purkautuu B:n yksityisellä avaimella yhdessä äskeisen j:n kanssa. (Muunlainen tapahtuma ei oikeastaan edes pääsisikään vastaanottokanavaan, sillä se ei kuuluisi B:n aakkostoon.)

UserB =
rec.B?j?pB(y.j) -->
trans.B!j!pj(y.nB.B) -->
rec.B.j.pB(nB) --> Stop.

Vihollisprosessi lukee kaikkien käyttäjien trans-kanavia ja oppii niiden viestit: Prosessi on parametrisoitu sen tietämien viestien eli joukon S mukaan. Vihollisen alkutiedoiksi eli joukon S alustavaksi sisällöksi otetaan mm. muiden osapuolten nimet, näiden julkiset avaimet sekä joitakin omia satunnaislukuja (nonce-käyttöä varten).

Toimiessaan vihollinen vaihtoehtoisesti valitsee käyttäjäparin i,j ja lähettää jonkin tietämänsä tai tiedoistaan (relaatiolla |-) johtamansa viestin j:n nimissä i:n vastaanottokanavaan. Tietenkin näiden viestintöjen joukossa voi olla myös se liikenne, mitä protokollan mukaan pitäisi tapahtua A:n ja B:n välillä.

ENEMY(S) =
trans?i?j?m --> ENEMY( S U {m} )
  []
[]i,j:USER , S |- m rec.i!j!m --> ENEMY(S)

Päivän artikkelissa on tähän verrattuna toinenkin ero, jonka merkitys on vähäisempi. Mallissa on ylimääräinen kerros: kukin solmu i (NODEi) on yhteydessä "loppukäyttäjään" i, kanavien in.i ja out.i kautta.

CSP-kuvauksen laatimista varten on olemassa myös kääntäjä, Casper (vrt. Lowe'97 ja Casperin kotisivu). Sen syötteenä on tekstitiedosto, jossa kuvataan protokolla melko tavalliseen tyyliin ja myös tutkittava systeemi osapuolineen, avaimineen yms. Tuloksena on vastaava CSP-kuvaus.

Tietoturvatavoitteiden mallinnus

Luottamuksellisuuden vaatimus tapahtumaketjuille on yksinkertaisesti se, että salaiseksi tarkoitettu viesti (eli tapahtuman viimeinen komponentti tietystä joukosta M) ei koskaan esiinny hyökkääjän vastaanottamia viestejä kuvaavissa tapahtumissa. Tämän kerran artikkeli kehittelee tälle vaatimukselle useita vaihtoehtoisia mutta yhtäpitäviä formalisointeja. Vaikka kyse on luontevimmin jälkiä koskevasta vaatimuksesta, sen algebrallinen ilmaisu on sopivin FDR-työkalun tutkittavaksi. Tämän ilmaisun ydin on, että kokonaisprosessi NET ei muutu, jos se asetetaan rinnakkain Stop-prosessin kanssa siten, että ne synkronoidaan kiellettyjen tapahtumien K kautta: NET |[K]| Stop = NET.

Stop on prosessi joka pysähtyy (lukkiutuu) heti, joten jos NET:ssä voisi sattua jokin K:n tapahtuma, se johtaisi lukkiutumiseen synkronointivaatimuksen takia. Prosessi NET |[K]| Stop ei siis olisi enää alkuperäinen NET. Koska FDR tarkastaa hienonnusrelaation, ja NET |[K]| Stop joka tapauksessa hienontaa NET:n, riittää tarkastaa vain, että NET hienontaa prosessin NET |[K]| Stop.

Harjoitus: Kaikesta siitä huolimatta, mitä olet autentikoinnista tähän mennessä oppinut, seuraavassa esitettävä autenttisuuden määrittely voi tuntua omituiselta tai ainakin hankalalta. Ennenkuin paneudut siihen, pohdi mitä oikeastaan edellyttää, että voit jostain viestistä tai muusta tapahtumasta sanoa, että se on aito. Eikö edellytykseksi osoittaudukin jokin aiempi tapahtuma ... ?

Autenttisuus edellyttää sitä, että jälki ei sisällä tiettyä tapahtumaa T, ellei jokin muu tapahtuma R esiinny ennen sitä. Jos tämä toteutuu, niin sanotaan, että T autentikoi R:n. Tässä R ja T voivat olla myös tapahtumajoukkoja, jolloin minkä tahansa T-alkion esiintyminen vaatii jonkin R-alkion esiintymisen.

Prosessialgebrallinen formalisointi on nyt   P |[ R,T ]| Stop = P |[ R ]| Stop.   Perusteluna ajatellaan jotain P:n tapahtumaketjua, jossa ei ole esiintynyt vielä mitään R:n tapahtumaa. Jos P seuraavaksi voisi toteuttaa jonkin T-tapahtuman, niin yhtälön vasemman puolen prosessi lukkiutuisi siihen paikkaan, kun taas oikea puoli pääsisi eteenpäin. Yhtälö ei siis olisi voimassa - yhtälön merkityshän on tapahtumaketjujen samuus molemmilla puolilla. Jos siis yhtälö pätee, mikään P:n tapahtumaketju ei voi sisältää mitään T-tapahtumaa ennen kuin jokin R-tapahtuma on esiintynyt siinä.

Kuten luottamuksellisuudenkin kohdalla yhtälön todistamiseksi riittää tässä tarkistaa vain, että jälkimmäinen prosessi on hienonnus edelliselle, koska toisinpäin hienonnus pätee P:stä riippumatta. (Mitä enemmän Stopin kanssa "kommunikoidaan", sitä vähemmän voi tapahtua).

Harjoitus: Edellä olevassa koodissa: mitä tapahtumia autentikoi tapahtuma rec.B.A.pB(nB) ja mitä ne merkitsevät?

Vastauksen etsiminen tähän on samaa toimintaa, jota pitää tehdä, kun protokollaa verifioidaan. Erityisesti voidaan todistaa, että autentikoiduksi tulee tapahtuma trans.A.B.pB(nB), mikä merkitsee, että A on vastannut B:n nonce-haasteeseen. Toisin (ja tarkemmin) sanoen, protokollan lopussa B tietää, että myös A on päässyt loppuun ja että A uskoi kommunikoineensa B:n kanssa. Ellei toisen viestin loppuun olisi (korjauksena) liitetty B:n nimeä, tätä tavoitetta ei saavutettaisi.

Lowen artikkelissa (96) yritetään verifioida alkuperäistä protokollaa, josta em. nimeäminen puuttuu. FDR osoittaa, ettei kysytty hienonnusrelaatio ole voimassa löytämällä sille vastaesimerkin eli tapahtumaketjun, jonka spesifikaatio (siis protokollan malli) sallii, mutta implementaatio (autentikointivaatimus) ei. Tästä jäljestä on helppo kaivaa esiin itse hyökkäys eli se, miten voi naamioitua protokollan aloittavaksi osapuoleksi. Artikkeli jatkaa sitten osoittamalla, että korjatussa versiossa autentikointi toteutuu.

Autentikointitavoitteita tarkemmin

Lowe esittää hierarkian, jossa erottuu autentikointia neljällä eri tasolla. Jos lisäksi otetaan huomioon aika - se että vastapuolesta tiedetään jotain tuoretta - saadaan neljä tasoa lisää. Katsotaan tässä vain ajastamattomia vaatimuksia ja ilmaistaan ne yksisuuntaisina niinpäin, että olio A autentikoi oliota B. Spesifikaation lähtökohtana on oletus, että A on suorittanut protokollan loppuun ilmeisesti B:n kanssa. Seuraavanlaisia olion B autentikoinnin tasoja voidaan saavuttaa:
  1. Elossaolo ('aliveness'): vaatimus on, että myös B on joskus aiemmin suorittanut protokollaa.
  2. Heikko sopiminen: äskeisen lisäksi vaaditaan, että B on protokollaa suorittaessaan luullut tekevänsä niin juuri A:n kanssa.
  3. Epäinjektiivinen sopiminen: Oletetaan, että protokollassa esiintyy joitakin tietoalkioita (kuten avaimia tai eo. esimerkissä nonce-lukuja). Vaatimus äskeisen lisäksi on, että B on protokollaa suorittaessaan tehnyt niin vastakkaisessa roolissa kuin A ja oliot ovat yhtä mieltä kaikista protokollan myötä vaihdetuista tiedoista.
  4. Sopiminen: Äskeisen lisäksi vaaditaan, että jokaista A:n suorittamaa protokollan ajokertaa ("ilmentymää") vastaa B:n puolella yksikäsitteinen eri ajokerta. Tällaisella injektiivisyydellä voi olla tärkeä merkitys vaikkapa transaktioiden oikeuttamiseen liittyvässä autentikoinnissa.
Autentikoinnin tiukimman tason vaatimus, eli (injektiivinen) sopiminen, mallinnetaan Lowen mukaan seuraavana prosessina (jos tietoalkiota sattuisi olemaan kaksi):

Agreement(B-role, A-role, {d1,d2}) (B) =
signal.Running.B-role.B?A?e1?e2 -->
signal.Commit.A-role.A.B.e1.e2 --> Stop.

Ajatus on, että kun tutkittavasta prosessista kätketään muut kuin tässä näkyvät tapahtumat, siitä pitäisi tulla tämän Agreement-prosessin hienonnus. Tapahtumien koostumus on aiempaan verrattuna monimutkaisempi. Erityisesti tässä erotellaan, missä rooleissa osapuolet osallistuvat protokollaan. Kanavan signal viestit ovat protokollan mallinnuksessa esiintyviä aputapahtumia, joilla osapuolet ikäänkuin välittävät uskomuksiaan tarkkailijalle. Uskomuksiin siis palattiin kuitenkin. Nyt ne vastaavat suoraan olion tilaa suhteessa protokollan vaiheisiin.

Tapahtumalla signal.Commit.A-role.A.B.e1.e2 osapuoli A ilmaisee, että hän on suorittanut loppuun protokollan kommunikoiden A-roolissa B:n kanssa käyttäen tietoalkioita e1 ja e2. Tämä tapahtuma sijoitetaan protokollan mallissa A:n viimeisen viestin perään (kuten kohta nähdään). Tapahtuma, joka tämän pitäisi autentikoida, on signal.Running.B-role.B?A?e1?e2. Sen toteutuminen ilmaisee, että B on ajanut protokollaa kommunikoiden B-roolissa A:n kanssa samoja tietoalkoita käyttäen. (Agreement-prosessin kannalta tiedot saavat arvonsa tässä prosessissa ja eo. Commit-tapahtumassa sitten ovat samat).

Olkoon mallinnettu jokin protokolla prosessina SYSTEM (kuten "NET" yo. esimerkissä) siten, että signal-kanavaa käytetään asianmukaisissa paikoissa. Toteuttaako protokolla "sopimis"-tasoisen autenttisuuden, testataan kysymällä FDR:ltä, onko prosessi   SYSTEM \ (S \ X)   hienonnus prosessille   Agreement(B-role, A-role, {d1,d2}) (B).   Tässä X on Agreement-prosessin aakkosto ja S on kaikkien tapahtumien joukko. SYSTEM \(S\X) tarkoittaa siis sellaista prosessia, josta on piilotettu sisäisiksi kaikki muut tapahtumat paitsi ne, jotka kuuluvat X:ään. (Operaation \(S\X) eli -(S-X) voi tavallaan ajatella myös muodossa -S+X. Mutkikas vähennys johtuu siitä, että kerran piilotettua ei "saada takaisin".)

Harjoitus. Seuraavassa on Needham-Schroederin protokollan aloittajaprosessin malli Lowen notaatiolla, jossa viestien rakenne on kryptauksen osalta hieman aiemmasta poikkeava, joskin ilmeinen. Isolla kirjoitetut tietoalkiot edustavat vakioarvoja ja pienellä kirjoitetut muuttujia. Vertaa tätä aiemman esimerkin prosessiin UserA. Kiinnitä huomiosi siihen, miten signaalit Running ja Commit sijoittuvat.

INITIATOR(A,na,pka) =
[]B:Agent   env.A.(Env0.B) -->
comm.A.B.(Msg1,Encrypt.(PK(B), <na,nb>)) -->
[]nb:Nonce   comm.B.A.(Msg2,Encrypt.(pka,<na,nb,B>)) -->
signal.Running.INIT-role.A.B.na.nb -->
comm.A.B.(Msg3,Encrypt.(PK(B),<nb>)) -->
signal.Commit.INIT-role.A.B.na.nb -->
SKIP

Toisenlainen esimerkki signal-kanavien tapaisista protokollan ulkopuolisista tapahtumista on evidence-kanava, jollaista voidaan käyttää kiistämättömyysvaatimuksen mallintamisessa. Tällaisessa tapauksessa ei riitä, että tarkoitetut toimijat noudattavat protokollaa. Semantiikkaan puolestaan pitää ottaa mukaan failures ja divergences (eli "estymät" ja "pillastumat"), mutta kuten sanottu, nämä jätetään tällä kurssilla syrjään.

Formalisoidaan nyt Lowen autentikointivaatimukset esittämällä, mitkä tapahtumat tai joukot T ja R niiden mukaan pitää sijoittaa Schneiderin yhtälöön SYSTEM |[ R,T ]| Stop = SYSTEM |[ R ]| Stop, joka tarkoitti siis, että T autentikoi R:n.

  1. Elossaolo, Aliveness(A-role)(B):
    T = signal.Commit.A-role.AGENT.B.DATA
    R = signal.Running.ROLE.B.AGENT.DATA
    Tässä AGENT, DATA ja ROLE ovat joukkoja, joten samoin ovat T ja R.

  2. Heikko sopiminen: WeakAgreement(A-role)(B):
    T = signal.Commit.A-role.A.B.DATA
    R = signal.Running.ROLE.B.A.DATA
    Kuten näkyy, edelliseen verrattuna tässä olio A kiinnittyy molemmissa samaksi. Ehdon pitää silti päteä kaikille A:n arvoille toimijoiden joukosta AGENT.

  3. Epäinjektiivinen sopiminen, NonInjectiveAgreement(B-role, A-role, d)(B):
    T = signal.Commit.A-role.A.B.e
    R = signal.Running.B-role.B.A.e
    Nyt B-role on kiinnitetty. Ehdon pitää päteä kaikille toimijoille A ja data-arvoille e, ja nyt myös jälkimmäinen on molemmissa joukoissa sama.

    Nämä joukot näyttävät juuri sellaisilta kuin edellä oli injektiivisen sopimisen spesifikaatiossa Agreement(B-role, A-role, {d1,d2}) (B). Prosessialgebrallinen yhtälö ei tuota injektiivisyyttä vaan sallii useita tapahtumia T, kunhan niitä edeltää edes yksi R-tapahtuma.

  4. Sopiminen: Schneider (1997) toteaa, että injektiivisyysvaatimuksen ilmaiseminen autentikointiyhtälöllä on työn alla. Ilmeisesti se on myös jäänyt sinne. Suoraan jälkien avulla asia voidaan kuitenkin ilmaista helposti vaatimalla, että missä tahansa jäljessä R:n esiintymien määrä on vähintään T:n esiintymien määrä. Muuten R ja T ovat kuten 3:ssa.
Autentikointikäsitteiden Lowen mukaista hierarkiaa on "havainnollistanut" F. Schuetz opetuskalvoillaan (2006) osoittamalla animaatiolla miten vaatimukset muuttuvat. Ne on kaikki esitetty prosesseina samaan tapaan kuin Agreement(..) edellä. Lopussa on käsitelty hieman myös aikariippuvaa autentikointia, edelleen Lowen mukaan.