Formalno modeliranje transakcija kriptografskog lanca blokova

završni rad

• Naslov (engleski): Formally modelling blockchain transaction
• Autor: Kristijan Rupić
• Mentor: Ante Đerek (mentor)
• Član povjerenstva: Ante Đerek (predsjednik povjerenstva)
• Član povjerenstva: Martin Tutek (član povjerenstva)
• Član povjerenstva: Darijan Marčetić (član povjerenstva)
• Ustanova koja je dodijelila akademski / stručni stupanj: Sveučilište u Zagrebu; Fakultet elektrotehnike i računarstva; Zagreb
• Datum i država obrane: 2019-07-12, Hrvatska
• Znanstveno / umjetničko područje, polje i grana: TEHNIČKE ZNANOSTI; Računarstvo

Sažetak

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.

Sažetak (engleski)

Blockchain is a distributed database that allows for immutable and non-repudiable storage of records without need for a trusted central authority using
cryptography for securing the stored data. It is used in implementations of systems such as cryptocurrencies and smart contracts and therefore requires high certainty in the correctness of implementation in order to guarantee various security-related properties. Formal methods arise as a crucial tool in the specification and
verification of such systems. In this thesis a formal model of the cryptocurrency Bitcoin’s transaction system is developed in the Coq proof assistant and a
machine-checked proof of the impossibility of double spending of money in the
system is written.

• Ključne riječi: mehanizirani dokaz; pomoćnik za dokazivanje; Coq; kriptografskimehanizirani dokaz; pomoćnik za dokazivanje; Coq; kriptografski lanac blokova; Bitcoin lanac blokova; Bitcoin
• Ključne riječi (engleski): mechanized proof; proof assistant; Coq; blockchain; Bitcoin
• Jezik: hrvatski
• URN:NBN: urn:nbn:hr:168:720794
• Studijski program: Naziv: Računarstvo; Vrsta studija: sveučilišni; Stupanj studija: preddiplomski; Akademski / stručni naziv: sveučilišni/a prvostupnik/ prvostupnica (baccalaureus/baccalaurea) inženjer/inženjerka računarstva (univ.bacc.ing.comp.)
• Vrsta resursa: Tekst
• Način izrade datoteke: Izvorno digitalna
• Prava pristupa: Zatvoreni pristup
• Datum i vrijeme pohrane: 2020-01-07 21:54:43