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