arvutiteaduse instituudi lõputööderegister


EasyCrypti rõõmud
Nimi Tejas Anil Shah
Kokkuvõte Arvutipõhiste tõestuste ja formaalse verifitseerimise ideed on juba pikka aega olnud olemas, kuid selles valdkonnas on sisenemisbarjäär kõrge. Kui tegemist on formaalselt verifitseeritud krüptograafiaga, on see barjäär veelgi kõrgem. Krüptograafias nõuab see rohkemate teemade tundmist, mis toob valdkonna pedagoogikas esile huvitavaid väljakutseid. Algajad, kes õpivad krüptograafia formaalse verifitseerimise vahenditega töötama, seisavad õppematerjalide puudumise tõttu silmitsi märkimisväärsete raskustega.

Krüptograafiliste tõestuste tööriistakomplekti EasyCrypti puhul takistab õppimistempot puudulik ja mõnikord vananenud kasutusjuhend, algajatele mõeldud õppematerjalide puudumine ning kõrge sisenemisbarjäär. Käesolevas töös lahendati seda probleemi, luues formaalse verifitseerimise avatud lähtekoodiga õpiku "The Joy of EasyCrypt".

Esitleme töös valminud õpiku esimesi peatükke, milles luuakse formaalse verifitseerimise kontekst ning arendatakse EasyCrypti õppimiseks ja sellega töötamiseks vajalikku teooriat ja praktilisi harjutusi. Sellega muudame EasyCrypti formaalse verifitseerimise metodoloogiad kättesaadavamaks ja kergemini õpitavaks.
Lõputöö keel inglise
Lõputöö tüüp Magister - Informaatika
Juhendaja(d) Dominique Unruh
Kaitsmise aasta 2022
PDF lisad