Formalno modeliranje transakcija kriptografskog lanca blokova

undergraduate thesis

• Title (english): Formally modelling blockchain transaction
• Author: Kristijan Rupić
• Mentor: Ante Đerek (mentor)
• Committee member: Ante Đerek (predsjednik povjerenstva)
• Committee member: Martin Tutek (član povjerenstva)
• Committee member: Darijan Marčetić (član povjerenstva)
• Granter: University of Zagreb; Faculty of Electrical Engineering and Computing; Zagreb
• Defense date and country: 2019-07-12, Croatia
• Scientific / art field, discipline and subdiscipline: TECHNICAL SCIENCES; Computing

Abstract

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.

Abstract (english)

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.

• Keywords: mehanizirani dokaz; pomoćnik za dokazivanje; Coq; kriptografskimehanizirani dokaz; pomoćnik za dokazivanje; Coq; kriptografski lanac blokova; Bitcoin lanac blokova; Bitcoin
• Keywords (english): mechanized proof; proof assistant; Coq; blockchain; Bitcoin
• Language: croatian
• URN:NBN: urn:nbn:hr:168:720794
• Study programme: Title: Computing; Study programme type: university; Study level: undergraduate; Academic / professional title: sveučilišni/a prvostupnik/ prvostupnica (baccalaureus/baccalaurea) inženjer/inženjerka računarstva (sveučilišni/a prvostupnik/ prvostupnica (baccalaureus/baccalaurea) inženjer/inženjerka računarstva)
• Type of resource: Text
• File origin: Born digital
• Access conditions: Closed access
• Created on: 2020-01-07 21:54:43