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

Cryptography is used to protect data and communications. The basic tools are cryptographic primitives, whose security and efficiency are widely studied. But in real-life applications these primitives are not used individually, but combined inside complex protocols. The aim of this thesis is to analyse various cryptographic protocols and assess their security in a formal way. In 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. In 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. Once that the bases are given, the first protocols are analysed in chapter 3, where two Attribute Based Encryption schemes are proven secure. First context and motivation are introduced, presenting settings of cloud encryption, alongside the tools used to build ABE schemes. Then the first scheme, that introduces multiple authorities in order to improve privacy, is explained in detail and proven secure. Finally 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. The next protocol analysed is a tokenization algorithm for the protection of credit cards. In 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. In chapter 5 the focus is on the BIX Protocol, that builds a chain of certificates in order to decentralize the role of certificate authorities. First 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. Finally a viable attack vector is analysed, and a mitigation approach is discussed. In 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. Its security is studied in a variety of attack scenarios, giving proofs based on standard algebraic assumptions. The 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. Particular 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.