Pohjana on mm. aiempi artikkeli I.Ray, I.Ray: An Anonymous Fair-Exchange E-Commerce Protocol (Proc. 1st Int. Workshop on Internet Computing and E-Commerce, April 2001), johon uudempi artikkeli ei jostain syystä viittaa. Vanhemman artikkelin protokolla on saanut osittaisen formaalin todistuksen: W.Kong, K.Ogata, J.Xiang, K.Futatsugi: Formal analysis of an anonymous fair exchange e-commerce protocol (Proc. 4th Int. Conf. on Computer and Information Technology, 2004, p. 1100-1107). Tämä artikkeli löytyy esim. ieeexplore.ieee.org:sta mutta on vaikeatajuinen eikä kovin vakuuttava. Siinä on käytetty OBJ-perheeseen kuuluvaa CafeOBJ-kieltä. Kirjoittajat Ray & Ray ovat itse tutkineet reilun vaihdon piirteitä CSP-algebralla: Failure Analysis of an E-commerce Protocol using Model Checking (2000). Tämä tarjoaa soveltajan näkökulman CSP:hen, joka myöhemmissä luennoissa tulee esille lähinnä kehittäjien tekstien perusteella.
Uusi artikkeli on melko pitkä mutta asiat on siinä selitetty juurta jaksain. Monin paikoin tarjoutuu kertausta aiemmin opitusta. Otetaan varsinaisesti luettavaksi vain anonyymin reilun vaihdon protokolla analyyseineen ja lopputoteamukset, eli luvut 8-10 (noin 9 sivua). Artikkelin muihin lukuihin voi joutua hieman vilkaisemaan:
Ristiinvalidointi ('cross validation') tarkoittaa kirjoittajien kehittelemää "teoriaa" sille, mitä voi tehdä kahdella RSA-avaimella K1=<e,N1> ja K2=<e,N2>, joilla on eri moduulit N1 ja N2 mutta sama salauseksponentti e. Näistä määritellään tuloavain K1xK2 = <e, N1·N2>, jota voidaan käyttää normaaliin tapaan. Jos jokin viesti m salataan K1xK2:lla, tulee sama tulos modulo Ni kuin jos m salataan Ki:llä. Luvussa 3 esitetyn teorian ydin on siinä, että sama pätee myös toisinpäin, kun m < Ni (Teoreema 3). Toisin sanoen, jos salatekstit ovat samat modulo Ni, viestitkin ovat samat. Kolmansin sanoin, jos (m1e mod N1·N2) = m2e mod Ni, niin m1=m2. Tämä antaa mahdollisuuden verrata "sokkona" kahta salatekstiä ja vakuuttua, että selkotekstit ovat samat, vaikka salausavaimet ovatkin eri.
Asiakas voi ristiinvalidoinnin kautta protokollan sisällä varmistua siitä, että hänen tilaamansa bittituote on sama kuin se, jonka hän aikanaan saa. Tämä ominaisuus esitellään luvussa 3 määritelmässä 13 ja se on nimeltään validated receipt. (Mitä se olisi suomeksi?) Ominaisuutta käytetään luvun 4 epäanonyymissa perusprotokollassa myös siihen, että kauppias voi vastaavaan tapaan ristiinvalidoida maksumääräyksen ennen kuin myöhemmässä viestissä saa siihen purkuavaimen. Toisin kuin luettavana olevassa protokollassa asiakas käyttää tässä maksun kryptaamiseen siis generoimaansa julkista eikä symmetristä avainta. Vastaavasti kuin tuotteen validoinnissa maksun salaukseen käytetyn tuloavaimen toinen moduuli tekijöineen on luotetulla osapuolella, joka tässä tapauksessa on pankki.
Edellä kuvaillun validointiteorian lisäksi on tärkeää huomata, miten tuloavaimella kryptattu viesti voidaan purkaa. Artikkeli on tässä asiassa melko epämääräinen ja avainten indeksoinnissa esiintyvät virheet hankaloittavat ymmärtämistä. Ilmiö on kuitenkin yhtä yksinkertainen kuin eo. validointiyhtälökin. Jos jotain on salattu korottamalla se potenssiin e ja redusoimalla modulo N1·N2;, niin kun se redusoidaan modulo Ni, saadaan sama kuin jos alunperinkin olisi redusoitu modulo Ni. Tällaisen salatekstin purkaminen tapahtuu tavalliseen tapaan korottamalla se potenssiin d modulo Ni, missä d on e:n käänteisluku modulo Phi(Ni). Tärkeä havainto siis on, ettei lisämoduulista, esim. N1:stä, ole tässä mitään "haittaa", kunhan käänteisavain (eli d) tunnetaan toisen moduulin (N2:n) suhteen. Artikkelin termejä käyttäen avaimella K2-1 voidaan purkaa kryptoteksti, joka on salattu avaimella K1xK2.
Artikkelin luvusta 4.1 kannattaa jo aluksi lukea määritelmät käsitteille [optimistic] fair exchange ja money atomicity. Optimistisuus on sitä, että protokolla normaali toiminta sujuu ilman kolmannen osapuolen aktiivista osallistumista. Tämän ominaisuuden lisäksi artikkelin varsinainen reilun vaihdon protokolla on anonyymi siinä mielessä, ettei kukaan muu osallistuja saa selville asiakkaan identiteettiä. (Aiemmassa, vuoden 2001 artikkelin protokollassa toteutui sekä asiakkaan että myyjän anonymiteetti.) Rahan jakamattomuus on ymmärrettävissä normaalien transaktioiden kautta. (Siihen voitaisiin palata vielä erikseen B-osassa todistusten näkökulmasta, pohjana esim. artikkeli Katsaros ym.: Simulation and verification of atomicity properties for an electronic cash system (2005), jossa käytetään väritettyjä Petri-verkkoja).
Anonyymin reilun vaihdon protokolla sisältää 9 viestiä, joiden pääpiirteet on tiivistetty seuraavassa. Osapuolet C, M, T ja B ilmenevät kahdesta ensimmäisestä viestistä. Viestistä 4 alkaen C esiintyy pseudonyyminä C'.
Harjoitus: (1) Mille tasolle protokolla yltää Vogtin ym:n reiluusluokituksessa: Modular Fair Exchange Protocols for Electronic Commerce, 1999 (vrt. samojen tekijöiden tuoreempi artikkeli: Fair Exchange The Computer Journal, 2003; 46:1, 55-75)
(2) Millä tavoin protokollassa voisi hyödyntää reiluun vaihtoon tarkoitettua "todennettavasti sitoutunutta" allekirjoitusta, joka oli esillä luennolla 8? Miten silloin esillä ollut tilanne muuten vertautuu tämänkertaiseen?
(3) Julkisen avaimen salausta ei tunnetusti ole järkevää soveltaa mihinkään kovin laajoihin bittituotteisiin. Miten tämä pitäisi ottaa huomioon edellä olevassa protokollassa? Miten järkevää on yleisesti ottaen se, että luotettu osapuoli on tässä oikeastaan kauppiaan markkinapaikka, eli siellä on ja sieltä haetaan saman verran tuotebittejä kuin kauppiaalta itseltään?
(4) Kertauskysymys: Mikä olikaan tolkku siinä, että M lähettää C':lle jotain eri moduulilla salattua kuin se mitä C sai T:ltä? Ja miksi (siis) ylipäätään M:n tarvitsee lähettää tuote, vaikka C:llä jo tavallaan on se?
(6) Abstrahointia: Reiluuden vaatimus esitetään toisinaan vain suhteessa johonkin protokollaan, jolloin sen olemus saattaa hieman hämärtyä. Näin väittävät O.Markowitch, D.Gollmann, S.Kremer artikkelissaan On Fairness in Exchange Protocols (2002), jossa määritellään abstrakting vaihtoprotokollan turvallisuus ja sille yhdeksi osaksi reiluus.
Kun annetaan joukko tosia lauseita, voidaan päättelysäännöillä johtaa uusia tosia lauseita. Siinä mielessä logiikalla ei saavuteta mitään uutta, vaan kaikki tietämys on jo "koodattuna" lähtökohdissa eli premisseissä.
Jos esim. tiedetään väitteet eli propositiot p ja p-->q tosiksi, niin päättelysäännön Modus Ponens perusteella tiedetään myös q todeksi. Tämä on propositio- eli lauselogiikkaa. Predikaattilogiikka tuo siihen lisää ilmaisuvoimaa muuttujien avulla. Samalla propositiot laajennetaan antamalla niille ikäänkuin parametreja, jollaisina voivat toimia vakiot ja niitä edustavat muuttujat. "Parametrisoituja propositioita" sanotaan predikaateiksi. Niissä olevia muuttujia sidotaan eksistenssikvanttoreilla E ("there Exists") ja universaalikvanttorilla A ("for All"), joiden symbolit oikeasti ovat ylösalaisin kirjoitetut E ja A. Nyt esim. premisseihin A x: P(x)-->Q(x) ja P(u) "sisältyvät" johtopäätöksinä mm. E y:P(y) ja Q(u). (Tässä u on vakio, ei muuttuja.)
Päättelysääntöjen (älykkään tai automatisoidun) soveltamisen lisäksi näiden logiikkojen tapauksessa uusia tosia lauseita voidaan johtaa myös algebrallisten yhtälöiden perusteella, esimerkiksi p Tai (q Ja r) = (p Tai q) Ja (p Tai r). Yhtälöt ovat tietysti samalla uusia päättelysääntöjä. Toisaalta niistä muodostuu propositiologiikan tapauksessa oma algebrallinen struktuurinsa, nimittäin Boolen algebra. Sen pitäisi olla tuttu monestakin tietotekniikan yhteydestä.
Predikaattilogiikkaa sanotaan ensimmäisen kertaluvun teoriaksi. Jos predikaattisymboleistakin tehdään muuttujia (vähän niinkuin funktioparametreja), saadaan korkeamman kertaluvun teorioita. Sellaisia ei tässä yhteydessä tarvita.
Logiikat ovat siis kieliä, jossain määrin samaan tapaan kuin ohjelmointikielet. Niissä on ensinnäkin syntaksi, joka määrää, mitkä symbolijonot (lauseet) kuuluvat kieleen ja mitkä eivät. Tältä osin syntaksi on periaatteessa varsin yksinkertainen asia, vaikka symbolijoukko voikin olla mutkikas. Päättelysäännötkin kuuluvat syntaksiin, mutta palataan niihin jäljempänä.
Toinen osa kielen määrittelyä on semantiikka, jonka tehtävänä on kertoa, mitä kielen lauseet merkitsevät. Ohjelmointikielessä asia voidaan ilmaista viime kädessä näyttämällä, mitä operaatioita lauseen pitää saada aikaan prosessorissa, eli käytännössä antamalla käännös konekielelle. Logiikassa voisi ajatella, että semantiikka on käännös luonnolliselle kielelle, koska logiikan tehtävänä on todellisuuden mallintaminen. Sellaisenaan tämä johtaisi kuitenkin takaisin samoihin ongelmiin, joiden takia mallinnus tehdään; epätäsmällisyyteen, tulkinnanvaraisuuteen, hallitsemattomaan mutkikkuuteen jne.
Tämän välttämiseksi semantiikka esitetään muodollisen tuntuisena tulkintafunktiona, jossa kielen perusosat käännetään "maailmaksi", mutta vain siinä määrin kuin on tarpeellista osista muodostuvien kokonaisuuksien totuuden määrittämiseen. Propositiologiikan tapauksessa riittää kertoa, mitkä atomilauseet ovat tosia ja mitkä eivät eli kuvata p:t ja q:t totuusarvoiksi 0 tai 1. Tämän jälkeen kaikki niistä koostetut lauseet saavat jommankumman totuusarvon. Lähtökohtana tälle on se, että konnektiiveillekin on määritelty semantiikka eli miten niillä yhdistetyn lauseen totuusarvo lasketaan. Tämä semantiikka on aina sama ja se määritellään tunnetusti totuustauluilla.
Predikaattilogiikassa on hieman enemmän osia, joten siellä tulkitseva kuvauskin on mutkikkaampi. Nytkin tosin riittää antaa totuusarvo tietyille peruslauseille, jolloin operaattoreille kiinnitetty semantiikka hoitaa loput. Määrittely tehdään pystyttämällä universumiksi jokin olioiden joukko (esim. kokonaisluvut tai TTY:n opiskelijat), ja kuvaamalla vakiosymbolit tämän maailman alkioiksi ja kukin predikaatti joksikin tämän maailman relaatioksi. Jos predikaatti on n-paikkainen (eli sillä on n parametria), sen tulkintana on siis n-paikkainen relaatio eli joukko n:n alkion vektoreita. Lauselogiikan propositiot ja niiden kuvaus totuusarvoiksi sisältyvät tähän: ne ovat nimittäin 0-paikkaisia predikaatteja ja 0-paikkainen relaatio voidaan ajatella vakioarvoksi, tässä tapauksessa siis 0:ksi tai 1:ksi. Universumia ja tulkintafunktiota yhdessä sanotaan kielen malliksi.
Päättelysääntöjen ideana on tietenkin, että lähtökohtien ollessa tosia samoin on johtopäätös. Totuuden säilyttävää päättelyjärjestelmää sanotaan konsistentiksi. Jos päättelemällä saadaan aikaan kaikki todet lauseet, järjestelmä on täydellinen. Täydellisyys ja varsinkin konsistenssi ovat ymmärrettävästi tärkeitä minkä tahansa logiikaksi tarkoitetun kielen ominaisuuksia. Vaikka logiikkaa voitaisiinkin siis "pyörittää" päättelyjärjestelmänä, tarvitaan myös semantiikka, jotta tiedettäisiin onko tuloksilla mitään merkitystä. Semantiikan pitäisi tietysti myös hyväksyttävällä tavalla vastata mallinnettavaa todellisuutta.
Vaikka päättelysäännöt ovatkin siis kytköksissä semantiikkaan, niiden soveltaminen on vain syntaktista askartelua. Päättelyn oikeellisuus voidaan nimittäin ratkaista mekaanisesti viittaamatta lauseiden totuuteen tai varsinkaan mihinkään arkimerkitykseen. Riittää vain tarkistaa, kuuluuko päättelyksi väitetty symbolijono oikeiden päättelyiden kieleen vai ei. Tämä tarkistus on ratkeava ja voidaan siis vaikkapa automatisoida. Lauselogiikan tapauksessa annettuun tulokseen johtavan päättelyn generointikin voidaan ohjelmoida, mutta predikaattilogiikassa tämä ei ole teoriassakaan mahdollista.
Jos tuntee predikaattilogiikkaa, voi tietyssä pinnallisessa mielessä ajatella, että modaalilogiikka saadaan siitä asettamalla tavallisten kvanttorien "A" ja "E" tilalle operaattorit "välttämättä" ja "mahdollisesti". Nämä ovat kvanttorien tapaan toisilleen duaaleja eli "välttämättä P" on sama kuin "ei mahdollista että ei P". Modaalilogiikka sinänsä on kuitenkin vain lauselogiikkaa eli siihen ei sisälly muuttujia joita uudet operaattorit sitoisivat (kuten kvanttorit tekivät predikaattien välityksellä).
Siinä missä tavallisen lauselogiikan semantiikaksi riittävät (kaikki) sellaiset maailmat, jotka ovat mahdollisia (eli joissa premissit ovat tosia), modaalilogiikassa pitää esittää, millaiset siirtymät ovat mahdollisia tällaisten maailmojen välillä. "Välttämättä P" on tarkalleen silloin tosi, jos P on tosi kaikissa niissä maailmoissa, joihin nykyisestä voidaan siirtyä, "mahdollisesti P" on tosi, jos P on tosi edes yhdessä niistä.
Tavallinen modaalilogiikka muuttuu episteemiseksi, tietoa koskevaksi, kun "välttämättä" korvataan operaattorilla "tiedetään, että". Tarkemmin voidaan eritellä tietenkin myös toimija eli protokollan osapuoli, joka tietää. Mitä sitten on duaali operaattori, eli "ei tiedetä että ei P"? Tällaisen logiikan avulla yleensä tutkitaan, mitä tietoa on, joten duaalia ei tarvitse tulkita, mutta tulkinta voisi olla: "pidetään mahdollisena että P". Toisaalta tämä yhteys otetaan aksioomaksi, joka edustaa tiedon ristiriidattomuutta: jos tiedetään P, niin silloinhan ei tietenkään tiedetä P:n vastakohtaa (mikä voidaan sanoa niinkin, että P:tä pidetään mahdollisena).
Aksioomiksi otetaan logiikan kielissä (jokin) sellainen mahdollisimman pieni joukko premissejä, joista kaikki muut todet lauseet voidaan päätellä (kunhan päättelysäännöt ovat riittävän vahvat). Muita episteemisiä aksioomia:
Ensi kerralla käsiteltävä BAN-logiikka on eräänlainen muunnos episteemisestä logiikasta, koska siinä tietäminen korvataan uskomuksella. Uskomuslogiikkaa sanotaan doxastiseksi.
Toisenlainen modaalilogiikka on temporaalinen eli aikalogiikka, jossa perusoperaattorit ovat "aina" ja "joskus" ja näillä voidaan viitata joko menneisyyteen tai tulevaisuuteen.
Erilaisia logiikoita on selitetty hyvin Wikipedian sivulla ja keskeinen alaluku kurssin kannalta on modaalilogiikan sivu.
Jos halutaan mallintaa kryptoprotokollia ja yleisemmin hajautettuja järjestelmiä algebran keinoin, niin järjestelmistä pitäisi abstrahoida joitakin keskeisiä olioita, määritellä niiden välille luontevia operaatioita, johtaa operaatioille tehokkaita laskusääntöjä, ja laskennan tuloksena olevista olioista pitäisi saada irti ominaisuuksia, joilla on merkitystä kulloisenkin ongelman ratkaisussa.
Hajautetuissa järjestelmissä on toisistaan erillään toimivia prosessoreita, jotka ovat kuitenkin yhteydessä keskenään viestejä vaihtamalla. Kommunikoivia olioita ovat oikeastaan prosessit ja viestien avulla ne voivat synkronoitua eli toteuttaa jonkin tapahtumansa samalla hetkellä kuin toinenkin. (Sama hetki voi toki vaatia odottelua jommaltakummalta osapuolelta.)
Mitään suurempaa kuin prosessi tuskin kannattaa ottaa algebrallisen käsittelyn kohteeksi. Prosesseja käsittelevän algebran perusolioiksi, lukujen ja propositioiden tapaan, asettuvat luontevasti sellaiset tapahtumat, joita ratkaistavan ongelman kannalta voidaan pitää jotenkin jakamattomina. Esimerkiksi DH-prokollan vastinoliot suorittavat prosesseja, joiden tapahtumina varmaankin ovat viestien lähettämiset ja vastaanottamiset ja niiden perusteella tapahtuva siirtyminen käyttämään generoitua avainta.
Perusoperaatiot ovat luontevasti peräkkäisyys ja rinnakkaisuus. Edellisen voisi ajatella vastaavan eräänlaista ei-vaihdannaista kertolaskua ja jälkimmäisen yhteenlaskua. Hieman erilainen yhteenlasku on Boolen algebran +, joka tarkoittaa summaa modulo 2, eli operaatiota XOR, eli "joko-tai". Tätä vastaa prosessien tapauksessa vaihtoehtoisuus: jompikumpi (tai yksi useammasta kuin kahdesta) prosessista lähtee käyntiin. CCS:ssä vaihtoehtoisuus merkitäänkin +:lla, kun taas CSP:ssä on tähän tarkoitukseen kaksikin hieman erilaista operaatiota. (CCS = Calculus of Communicating Systems, CSP=Communicating Sequential Processes).
Siinä missä vaihtoehtoisuus vastaa "joko-tai"-operaatiota, niin rinnakkaisuuden voisi ajatella vastaavan "sekä-että"- eli "ja"-operaatiota. Boolen algebran mallin mukaisesti kyseessä olisi siis kertolasku, jota tosin edellä verrattiin peräkkäisyyteen! Näiden vertailujen opettavaisuus lieneekin nyt jo käytetty lähes loppuun. Erityisesti rinnakkaisten prosessien kohdistaminen vaatii oleellisesti mutkikkaampia toimia kuin tutuissa algebroissa on kohdattu. Kootaan edellä mainitut algebran osat ja yleiset vertailut vielä yhteen ja otetaan taulukkoon mukaan myös semantiikka eli se, miten malli tulkitaan. Prosessialgebrana käytetään tässä kuten jatkossakin CSP:tä.
| Ilmiö | Boole | CSP |
| aakkosto |
muuttujat vakiot | tapahtumat |
| operaatiot |
disjunktio, konjunktio negaatio,... | peräkkäisyys: --> vaihtoehtoisuus: [] (neliö, ulkoisesti valittu) ja [¯] (hakanen, epädeterm.); rinnakkaisuus: |[ tapahtumia ]| , ||| (jos synkronoitavia tapahtumia ei ole), ... |
| laskusäännöt |
kommutatiivisuus distributiivisuus de Morgan, ... |
kommutatiivisuus,
distributiivisuus, ..., rekursiivisten määrittelyjen käsittelyssä kiintopisteen periaate |
| semantiikka, merkitys |
muuttujien ja vakioiden kuvaus totuusarvoiksi; totuusarvoja yleensä ajatellaan myös silloin, kun näennäisesti vain pyöritellään kaavoja. Totuusarvojen joukko voidaan esittää graafisesti Boolen hilana. |
operationaalinen (lähellä implementaatiota):
esitettävissä siirtymäkaavioina (LTS, labelled
transition system) denotationaalinen: vastaa lähinnä kuvausta totuusarvoiksi, joita tässä tapauksessa edustavat jäljet (traces) eli mahdolliset tapahtumien ketjut. Näille tarvitaan usein pareiksi 'failures' eli ne tapahtumat, jotka kulloinkin ovat mahdottomia. Kolmantena komponenttina voivat olla 'divergences' (~ ikisilmukat). algebrallinen: tietyt laskusäännöt otetaan aksioomiksi. Kielen merkitys muodostuu sitten samaan tapaan kuin esim. kokonaislukujen abstrakti merkitys rakentuu niiden aksioomista. |
Kun edellä puhuttiin laskusäännöistä, viitattiin lähinnä sellaisiin, joissa suoraan esiintyy yhtälö, esim. a·(b+c) = a·b+a·c. On muunkintyyppisiä sääntöjä, esimerkiksi epäyhtälöitä, kuten (luvuilla tai vektoreilla): |a+b| =< |a|+|b|. Lisäksi, jos sattuisi olemaan sellaiset positiiviset luvut x ja y, että a = x < y, voisimme kirjoittaa mm. a·(b+c) = x·b+x·c < x·b + y·c, käyttäen operaatioiden + ja · sekä relaatioiden = ja < ominaisuuksia. Näillä laskusäännöillä on nimenä sijoitussääntö ja (positiivisten lukujen kertolaskun) monotonisuus.
Prosessien laskutoimituksia koskevat laskusäännöt noudattelevat samoja periaatteita, mutta niitä ei saa tulkita liian suoraan vanhojen mallien mukaan. Erityisesti yhtäsuuruuden lisäksi on käytössä eri yhteyksissä hieman eri tavalla määriteltyjä ekvivalensseja, joissa prosessit eivät ole tarkkaan ottaen samat, vaan esimerkiksi sellaisia, ettei niiden välillä pysty ulkoapäin huomaamaan eroa. Ekvivalenssi on syytä määritellä siten, että sijoitussääntö on voimassa. Tämä tarkoittaa, että yhtäläisyys säilyy, vaikka jokin osa vaihdetaan sen kanssa yhtäläiseen (kuten edellä a x:ksi).
Pienemmyysrelaation sijasta prosessien välille määritellään esijärjestys, joka ei ole kokonainen järjestys siten, että kaikki olisivat verrattavissa kaikkiin eikä edes osittainen järjestys, koska siinä ei vaadita antisymmetriaa (eli sitä että a<b sulkisi pois mahdollisuuden b<a). Näitä esijärjestyksiä kuten ekvivalenssejakin voidaan määritellä hieman eri tavoin ja niillä on tärkeä merkitys prosessialgebran soveltamisessa käytäntöön, sillä niiden kautta järjestelmälle asetetut vaatimukset hienonnetaan toteutukseksi ("refinement"). Tässä on keskeistä, että järjestys on määritelty siten, että kaikki operaatiot ovat sen suhteen monotonisia. Tämä tarkoittaa, että jos jokin osa vaihdetaan "parempaan", tulos ei "huonone" (vrt. x:n vaihto y:ksi edellä).