Formal Proofs of Security for Privacy-Preserving Blockchains and other Cryptographic Protocols

Abstract

Cryptography is used to protect data and communications.
\nThe basic tools are cryptographic primitives, whose security and efficiency are widely studied.
\nBut in real-life applications these primitives are not used individually, but combined inside complex protocols.
\nThe aim of this thesis is to analyse various cryptographic protocols and assess their security in a formal way.
\nIn chapter 1 the concept of formal proofs of security is introduced and the main categorisation of attack scenarios and types of adversary are presented, and the protocols analysed in the thesis are briefly introduced with some motivation. 
\nIn chapter 2 are presented the security assumptions used in the proofs of the following chapters, distinguishing between the hardness of algebraic problems and the strength of cryptographic primitives.
\nOnce that the bases are given, the first protocols are analysed in chapter 3, where two Attribute Based Encryption schemes are proven secure.
\nFirst context and motivation are introduced, presenting settings of cloud encryption, alongside the tools used to build ABE schemes.
\nThen the first scheme, that introduces multiple authorities in order to improve privacy, is explained in detail and proven secure.
\nFinally the second scheme is presented as a variation of the first one, with the aim of improving the efficiency performing a round of collaboration between the authorities.
\n
\nThe next protocol analysed is a tokenization algorithm for the protection of credit cards.
\nIn chapter 4 the advantages of tokenization and the regulations required by the banking industry are presented, and a practical algorithm is proposed, and proven secure and compliant with the standard. 
\nIn chapter 5 the focus is on the BIX Protocol, that builds a chain of certificates in order to decentralize the role of certificate authorities.
\nFirst the protocol and the structure of the certificates are introduced, then two attack scenarios are presented and the protocol is proven secure in these settings.
\nFinally a viable attack vector is analysed, and a mitigation approach is discussed.
\nIn chapter 6 is presented an original approach on building a public ledger with end-to-end encryption and a one-time-access property, that make it suitable to store sensitive data. 
\nIts security is studied in a variety of attack scenarios, giving proofs based on standard algebraic assumptions. 
\nThe last protocol presented in chapter 7 uses a proof-of-stake system to maintain the consistency of subchains built on top of the Bitcoin blockchain, using only standard Bitcoin transactions.
\nParticular emphasis is given to the analysis of the refund policies employed, proving that the naive approach is always ineffective whereas the chosen policy discourages attackers whose stake falls below a threshold, that may be adjusted varying the protocol parameters.