Boolean satisfiability problem and cryptography

No Thumbnail Available
Journal Title
Journal ISSN
Volume Title
Helsinki University of Technology | Diplomityö
Checking the digitized thesis and permission for publishing
Instructions for the author
Date
2008
Major/Subject
Tietojenkäsittelyteoria
Mcode
T-79
Degree programme
Language
en
Pages
viii + 60
Series
Abstract
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.
Description
Supervisor
Nyberg, Kaisa
Thesis advisor
Nyberg, Kaisa
Keywords
trivium, kryptologia, cryptography, lauselogiikan toteutuvuusongelma, boolean satisfiability (SAT) problem, SAT -ratkaisija, SAT solver, epälineaariset binäärilukuyhtälöt, nonlinear binary equations, Gaussin eliminaatio, Gaussian elimination
Other note
Citation