Kryptoprotokollat, luento 11 (B), 30.4.2008

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

• Steve Schneider:
  • Security Properties and CSP (IEEE Symposium on Security and Privacy 1996, 174-189). Tämä on "päivän artikkeli", varmaankin sopivin yleisjohdanto tähän yhteyteen.
  • Verifying authentication protocols with CSP (1997, luentotekstin malli on enimmäkseen tästä artikkelista eikä äskeisestä)
  • Formal analysis of a non-repudiation protocol (1998).
  Näihin on linkit kirjoittajan sivulla.
• Gavin Lowe:
  • Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR (1996),
  • A Hierarchy of Authentication Specifications (1997, tämän artikkelin notaatiota otetaan esille lopussa),
  • Casper: A Compiler for the Analysis of Security Protocols (1997).
  Näihin on linkit kirjoittajan sivulta. Erotuksena Schneiderin artikkeleihin, joissa pyritään todistuksiin, näissä viitataan enemmän automaattiseen verifiointiin FDR:llä, johon Schneiderinkin työt toki antavat mahdollisuuden.

CSP kryptografisten protokollien mallinnuksessa

Johdantoa

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

• peräkkäisyys: nuoli -->. Esim. P = a --> b tarkoittaa että prosessi P osallistuu ensin tapahtumaan a ja sitten tapahtumaan b.

• rinnakkaisuus: kaksi pystyviivaa ||. Osaprosessit toimivat rinnakkain ja synkronoituvat kaikissa tapahtumissa, jotka ovat niiden aakkostoissa yhteisiä. Synkronoituminen tarkoittaa, että molempien osaprosessien on oltava valmis osallistumaan samaan tapahtumaan samalla "hetkellä"; esim. prosessissa a-->b-->a || a-->a-->b tapahtuu ensin a kummassakin osaprosessissa, mutta sen jälkeen ei voida edetä eli syntyy lukkiuma, dead lock.

  Jos synkronoivat tapahtumat halutaan erikseen mainita (ja samalla rajata), merkitään ne kaksoisviivan väliin hakasulkeisiin: |[ tapahtumia ]|. Jos edellä olisi ollut |[a]| niin kumpikin a-tapahtuma olisi voinut toteutua ja osaprosessit olisivat tehneet b:n omia aikojaan, mutta silti oikeassa kohdassa, eli jälkimmäinen olisi odottanut ensimmäisen tehdessä b-tapahtumaansa.

  Jos mitään synkronoitavaa ei ole, merkitään vain |||.

• vaihtoehtoisuus: ulkoinen valinta, neliö []. Esim. a-->P [] b-->Q toteuttaa joko a:n tai b:n sen mukaan, mitä sen ympäristöstä on tarjolla - yleensä rinnakkaisuussynkronoinnin kautta. Jos sattuu a, sen jälkeen jatketaan kuin prosessi P.

  Epädeterministinen (sisäinen) valinta, hakanen [¯]. Prosessi a-->b [¯] b-->a valitsee "itse", kumpaa osaprosessia se lähtee toteuttamaan. Tällä esimerkillä voidaan mallintaa se, että a ja b tapahtuvat, mutta ei ole väliä kummassa järjestyksessä.

• "Toistorakenne" saadaan aikaan rekursiolla, esim. P = 1-->2-->P toistaa tapahtumia 1 ja 2 vuorotellen ikuisesti.
• "Aliohjelma": aiemmin määriteltyä ja nimettyä prosessia voi käyttää toisen määrittelyssä (kuten rekursiossakin tavallaan tapahtuu).
• "Parametrit": Prosessien tapahtuma-aakkosto sisältää tietoa, joka eri prosesseilla on erilainen. Aakkosto voi olla prosessin määrittelyssä parametrina, jolloin samalla kirjoittamisella voidaan "luoda" useita prosesseja, esimerkiksi kullekin osapuolelle oman tunnuksen i mukaisesti (i=1,2,...). Toinen esimerkki on prosessin "hallussa" kulloinkin olevat viestit.
• "Ehdollisuus": Edellämainitun kaltaisten prosesseissa esiintyvien tietojen perusteella voidaan määrittelystä tehdä ehdollinen, esim. P = if 'i>0' then Q else R.
• "Kapselointi" tai "abstrahointi". Aliohjelmien toinen tavoite (sen lisäksi että ne helpottavat kirjoittamista ja parametrisointia) on yksityiskohtien piilottaminen yleisnäkymän tieltä. Prosessialgebrassa tämä tapahtuu operaatiolla, jossa tietyt tapahtumat piilotetaan prosessin sisäisiksi. Tämä merkitään vähennyslaskuna: P \ {a} on kuin P, mutta a-tapahtumat eivät näy eivätkä erityisesti vaadi synkronointia. Merkinnän \ tilalla voi olla tavallinen miinusmerkki -.

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

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 = (User_A ||| User_B) |[ 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.)

User_A = []_{i: USER}
trans.A!i!p_i(n_A.A) -->
rec.A.i?p_A(n_A.x.i) -->
trans.A!i!p_i(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.)

User_B =
rec.B?j?p_B(y.j) -->
trans.B!j!p_j(y.n_B.B) -->
rec.B.j.p_B(n_B) --> 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 (NODE_i) 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

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.p_B(n_B) 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.p_B(n_B), 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

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.

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 User_A. 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.