haku: @supervisor Nyberg, Kaisa / yhteensä: 11
viite: 7 / 11
Tekijä:Hänninen, Aleksi
Työn nimi:Boolean satisfiability problem and cryptography
Lauselogiikan toteutuvuusongelma kryptologiassa
Julkaisutyyppi:Diplomityö
Julkaisuvuosi:2008
Sivut:viii + 60      Kieli:   eng
Koulu/Laitos/Osasto:Informaatio- ja luonnontieteiden tiedekunta
Oppiaine:Tietojenkäsittelyteoria   (T-79)
Valvoja:Nyberg, Kaisa
Ohjaaja:Nyberg, Kaisa
OEVS:
Sähköinen arkistokappale on luettavissa Aalto Thesis Databasen kautta.
Ohje

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 Aalto  8652   | Arkisto
Avainsanat:trivium
cryptography
boolean satisfiability (SAT) problem
SAT solver
nonlinear binary equations
Gaussian elimination
kryptologia
lauselogiikan toteutuvuusongelma
SAT -ratkaisija
epälineaariset binäärilukuyhtälöt
Gaussin eliminaatio
Tiivistelmä (fin): Tässä diplomityössä tutkitaan lauselogiikan toteutuvuusongelman (SAT -ongelman) ja sen ratkaisijoiden soveltamista kryptologiaan.
Ensin aiempia SAT -ongelman sovelluksia kryptologiaan esitetään lyhyesti.
Ne voidaan luokitella seuraaviin kategorioihin: SAT - pohjainen salaus, SAT -pohjainen suora hyökkäys, SAT - ratkaisijoihin perustuva sivukanavahyökkäys, SAT -ratkaisijoita apunaan käyttävä hyökkäys ja looginen kryptosysteemien varmennus.

Jonosalain Trivium, yksi ECRYPT:in eStream cipher -projektin kandidaatti, esitetään, joitain sen suunnitteluperusteita mainitaan ja sen muutamia ominaisuuksia lasketaan.
SAT - ratkaisijoiden toimintaperiaatteita kuvataan, samoin kuin keino muuntaa hyökkäys Triviumia vastaan SAT -ongelmaksi.
Tavoitteenamme on analysoida teoreettisesti kuinka SAT -ratkaisija ratkaisee samankaltaisia ongelmia ja kuinka hyökkäyksessä olevat parametrit tulee asettaa.

Erilaisten Triviumia vastaan tehtyjen suorien hyökkäysten tulokset esitetään ja tutkitaan.
Pienin löytämämme kompleksisuus on luokkaa 263 sekuntia, mikä saadaan tavallisella (ei sisäisen tilan) suoralla hyökkäyksellä.
Kompleksisuus avaimen etsimiselle brute force -menetelmällä on 280.
Syyksi huonoon menestykseen esitämme Triviumin loogisen piirin rakennetta.
Siinä ominaista on suhteellisen pientä tuloporttien määrää, kompleksista rakennetta, jota ei voi tehdä yksinkertaisemmaksi tai jakaa pienemmiksi ongelmiksi.
Nämä ominaisuudet ovat läsnä ongelmassa, ja osoitamme, että SAT -ratkaisijat etsivät tällöin ratkaisua tekemällä enimmäkseen päätöksiä tuloporteilla, mikä vastaa likimäärin brute force -hyökkäystä.

Lopuksi ehdotamme uutta SAT -pohjaista algoritmia, joka yhdistää Gaussin eliminaation SAT -ratkaisijaan.
Algoritmin pääajatus on lineaarisesti approksimoida epälineaarisia termejä.
Tämän jälkeen joukko lineaarisia yhtälöitä saadaan aikaiseksi approksimaatioita käyttämällä, joista voimme saada joukon rajoituksia käytettäville approksimaatioille.
Lopuksi voimme antaa uudet rajoitukset SAT -ratkaisijalle, joka etsii uudet approksimaatiot, jotka toteuttavat kaikki edelliset rajoitteet.
Tätä jatketaan, kunnes joko löydetään oikeat approksimaatiot, jolloin myös ratkaisu voidaan saada, tai sitten rajoitukset, ja siten koko ongelma, löydetään toteutumattomaksi.
ED:2008-05-19
INSSI tietueen numero: 35607
+ lisää koriin
INSSI