Tööriist sümmeetriliste primitiivide formaalseks analüüsiks

Nimi
Kristjan Krips
Kokkuvõte
Tänapäeva maailmas on krüpograafia laialt kasutusel, et turvata elektroonilist sidet. Seega on oluline, et vastavad krüptograafilised algoritmid oleksid tõestatavalt turvalised. Krüptograafiliste protokollide ehitamiseks kasutatakse krüptograafilisi primitiive ja terve protokolli turvalisus tõestatakse vastavate primitiivide turvalisusle tuginedes. Sümmeetrilised primitiivid kasutavad ühte salajast võtit nii krüpteerimiseks kui ka dekrüpteermiseks ja on kiiremad kui asümmeetrilised primitiivid. Seetõttu kasutatakse sümmeetrilisi primitiive paljudes protokollides ja seega on vaja leida vastavatele primitiividele turvatõestused. Üks võimalus turvatõestuste kirjutamiseks on kasutada krüptograafiliste mängude põhist tõestamist. Krüptograafilised mängud modelleerivad primitiive kindlas keskkonnas, kus leidub vastane. Mängude põhise tõestamise abil kirjutatakse esialgne mäng ümber nii, et primitiivi turvalisust oleks lihtsam tõestada. Selline tõestamise meetod on keeruline, kuna see nõuab palju ümberkirjutamist. Lisaks sellele võib mängude ümberkirjutamisel tekkida tõestusse vigu. Antud olukorra lahendamiseks kasutatakse tööriistu, mis abistavad tõestuse läbiviimist. Antud magistritöö teemaks on tööriista arendamine, mis aitab mängude põhiseid tõestusi läbi viia sümmeetriliste primitiivide jaoks. Vastava tööriista nimi on ProveIt ja see lubab modifitseerida krüptograafilisi mänge, kasutades kindlaid tõestuse skeeme. Vastava tõestusskeemi rakendamist nimetatakse transformatsiooniks. Minu eesmärgiks oli lisada antud programmis kasutatavale keelele semantika ja kasutada seda semantikat erinevate transformatsioonide lisamiseks programmi ProveIt. Magistritöö käigus implementeerisin ProveIt jaoks järgnevad transformatisoonid: Dead Code Elimination, Statement Switching, Remove Condition, Replace Function Call, Wrap ja Random Function Simulation. Surnud koodi eemaldamiseks oli vaja implementeerida elusate muutujate analüüs. Enne transformatsiooni implementeerimist tuleb tõestada vastav turvalisuse garantii ning seetõttu tõestasin magistritöös käsitletud trasformatsioonidele vastavad turvalisuse teoreemid. Edasise tööna tuleb ProveIt lisada keerukamaid transformatisoone, et võimaldada keerukamate turvatõestuste läbiviimist.
Lõputöö keel
inglise
Lõputöö tüüp
Magister - Informaatika
Juhendaja(d)
Sven Laur
Kaitsmise aasta
2012
 
PDF