|
|
|
|
| LEADER |
02646na a2200229 4500 |
| 003 |
HR-ZaFER |
| 008 |
160221s2019 ci ||||| m||| 00| 0 hr d |
| 035 |
|
|
|a (HR-ZaFER)ferid7085
|
| 040 |
|
|
|a HR-ZaFER
|b hrv
|c HR-ZaFER
|e ppiak
|
| 100 |
1 |
|
|a Rupić, Kristijan
|9 40851
|
| 245 |
1 |
0 |
|a Formalno modeliranje transakcija kriptografskog lanca blokova :
|b završni rad /
|c Kristijan Rupić ; [mentor Ante Đerek].
|
| 246 |
1 |
|
|a Formally modelling blockchain transaction
|i Naslov na engleskom:
|
| 260 |
|
|
|a Zagreb,
|b K. Rupić,
|c 2019.
|
| 300 |
|
|
|a 40 str. ;
|c 30 cm +
|e CD-ROM
|
| 502 |
|
|
|b preddiplomski studij
|c Fakultet elektrotehnike i računarstva u Zagrebu
|g smjer: Računarska znanost, šifra smjera: 41, datum predaje: 2019-06-14, datum završetka: 2019-07-12
|
| 520 |
3 |
|
|a 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.
|
| 520 |
3 |
|
|a Sažetak na engleskom: 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.
|
| 653 |
|
1 |
|a mehanizirani dokaz, pomoćnik za dokazivanje, Coq, kriptografskimehanizirani dokaz, pomoćnik za dokazivanje, Coq, kriptografski lanac blokova, Bitcoin lanac blokova, Bitcoin
|
| 653 |
|
1 |
|a mechanized proof, proof assistant, Coq, blockchain, Bitcoin
|
| 700 |
1 |
|
|a Đerek, Ante
|4 ths
|9 35048
|
| 942 |
|
|
|c Z
|
| 999 |
|
|
|c 51559
|d 51559
|