haku: @keyword formaalit menetelmät / yhteensä: 8
hakutulos-lista
viite: 5 / 8
« edellinen | seuraava »
Tekijä:Huima, Antti
Työn nimi:Analysis of cryptographic protocols via symbolic state space enumeration
Kryptografisten protokollien analysointi symbolisella tilahaulla
Julkaisutyyppi:Diplomityö
Julkaisuvuosi:1999
Sivut:xiii + 142      Kieli:   eng
Koulu/Laitos/Osasto:Tietotekniikan osasto
Oppiaine:Digitaalitekniikka   (Tik-79)
Valvoja:Ojala, Leo
Ohjaaja:Ylönen, Tatu
OEVS:
Sähköinen arkistokappale on luettavissa Aalto Thesis Databasen kautta.
Ohje
sulje

Digitaalisten opinnäytteiden lukeminen Aalto-yliopiston Harald Herlin -oppimiskeskuksen suljetussa verkossa

Oppimiskeskuksen suljetussa verkossa voi lukea sellaisia digitaalisia ja digitoituja opinnäytteitä, joille ei ole saatu julkaisulupaa avoimessa verkossa.

Oppimiskeskuksen yhteystiedot ja aukioloajat: https://learningcentre.aalto.fi/fi/harald-herlin-oppimiskeskus/

Opinnäytteitä voi lukea Oppimiskeskuksen asiakaskoneilla, joita löytyy kaikista kerroksista.

Kirjautuminen asiakaskoneille

  • Aalto-yliopistolaiset kirjautuvat asiakaskoneille Aalto-tunnuksella ja salasanalla.
  • Muut asiakkaat kirjautuvat asiakaskoneille yhteistunnuksilla.

Opinnäytteen avaaminen

  • Asiakaskoneiden työpöydältä löytyy kuvake:

    Aalto Thesis Database

  • Kuvaketta klikkaamalla pääset hakemaan ja avaamaan etsimäsi opinnäytteen Aaltodoc-tietokannasta. Opinnäytetiedosto löytyy klikkaamalla viitetietojen OEV- tai OEVS-kentän linkkiä.

Opinnäytteen lukeminen

  • Opinnäytettä voi lukea asiakaskoneen ruudulta tai sen voi tulostaa paperille.
  • Opinnäytetiedostoa ei voi tallentaa muistitikulle tai lähettää sähköpostilla.
  • Opinnäytetiedoston sisältöä ei voi kopioida.
  • Opinnäytetiedostoa ei voi muokata.

Opinnäytteen tulostus

  • Opinnäytteen voi tulostaa itselleen henkilökohtaiseen opiskelu- ja tutkimuskäyttöön.
  • Aalto-yliopiston opiskelijat ja henkilökunta voivat tulostaa mustavalkotulosteita Oppimiskeskuksen SecurePrint-laitteille, kun tietokoneelle kirjaudutaan omilla Aalto-tunnuksilla. Väritulostus on mahdollista asiakaspalvelupisteen tulostimelle u90203-psc3. Väritulostaminen on maksullista Aalto-yliopiston opiskelijoille ja henkilökunnalle.
  • Ulkopuoliset asiakkaat voivat tulostaa mustavalko- ja väritulosteita Oppimiskeskuksen asiakaspalvelupisteen tulostimelle u90203-psc3. Tulostaminen on maksullista.
Sijainti:P1 Ark T80     | Arkisto
Avainsanat:cryptographic protocols
formal methods
state space enumeration
symbolic methods
kryptografiset protokollat
formaalit menetelmät
tilahaku
symboliset menetelmät
Tiivistelmä (fin):Kryptografiset protokollat ovat keskeisessä asemassa tietoturvaratkaisuja kehitettäessä.
Monet suunnitelluista turvallisuusprotokollista on havaittu myöhemmin rakenteeltaan virheellisiksi.
Virheet protokollan loogisessa rakenteessa voivat mahdollistaa erilaisia hyökkäyksiä protokollaa vastaan.
Pahimmassa tapauksessa tuloksena ovat suuret taloudelliset ja muunlaiset menetykset.
Tästä syystä tieteellisessä kirjallisuudessa onkin esitetty useita menetelmiä kryptografisten protokollien formaalia verifiointia varten.

Tässä työssä esitetään uusi formaali menetelmä tietoturvaprotokollien analysoimiseksi.
Analyysimenetelmä perustuu symbolisen tilahakuun.
Symbolinen tilahaku itsessään on yleiskäsite joka viittaa luokkaan rinnakkaisten järjestelmien käyttäytymistä tutkittaessa käytettäviä menetelmiä.

Symbolinen tilahaku mahdollistaa äärettömän tila-avaruuden läpikäymisen äärellisessä ajassa.

Kryptografisia operaatioita mallinnetaan työssä algebrojen ja uudelleenkirjoitusjärjestelmien avulla.
Yleensä mallit jotka käyttävät uudelleenkirjoitusjärjestelmiä toteutetaan narrowing-algoritmin muunnelmilla.
Tässä työssä narrowing-algoritmia ei tarvita uuden, vaihtoehtoisen lähestymistavan vuoksi joka on sidottu kiinteästi koko hakuprosessiin.

Rinnakkaisten järjestelmien formaalissa analyysissa voidaan tyypillisesti suurin osa datasta abstrahoida pois.
Tietoturvaprotokollien kohdalla tilanne on toinen, koska nimenomaan siirretyt viestit ovat kiinnostavia.
Suurin osa esitellyn symbolisen menetelmän monimutkaisuudesta johtuukin tarpeesta käsitellä äärettömiä termijoukkoja ja niiden välisiä suhteita uudelleenkirjoitusjärjestelmien alaisuudessa.

Perusmenetelmän lisäksi työssä esitellään symmetriamenetelmä symbolisille tiloille ja menetelmä joidenkin symbolisten tilojen alisteisuussuhteiden havaitsemiseksi.

Analysointimenetelmän lisäksi myös menetelmästä tehty loppukäyttäjätoteutus esitellään.
Ohjelmisto on toteutettu Scheme-ohjelmointikielellä.

Työ jakautuu kahteen osaan.
Ensimmäinen osa esittää teoreettisen menetelmän.
Toinen osa keskittyy toteutukseen ja sisältää esimerkin.
ED:1999-07-20
INSSI tietueen numero: 14609
+ lisää koriin
« edellinen | seuraava »
INSSI