Formalno modeliranje transakcija kriptografskog lanca blokova : završni rad - Rupić, Kristijan (K. Rupić, 2019)
Sažetak na hrvatskom: Kriptografski lanac blokova (engl. blockchain) je raspodijeljena baza podataka koja omogućava neizmjenjivu i neporecivu pohranu zapisa bez potrebe za pouzdanim središnjim autoritetom uporabom kriptografije za osiguravanje podataka. Koristi se u implementaciji sustava poput kriptovaluta i pametnih ugovora (engl. smart contract) te stoga postoji potreba za visokom sigurnošću u ispravnost implementacije s ciljem garancije raznih sigurnosnih svojstava. Formalne metode nameću se kao nužan alat u specifikaciji i verifikaciji ovakvih sustava. U sklopu završnog rada izrađen je formalni model sustava transakcija kriptovalute Bitcoin u sustavu za dokazivanje Coq te napisan računalno provjeren dokaz nemogućnosti dvostrukog trošenja novca u sustavu.