*12:06*[PhD][New] Flavio D. Garcia: Formal and Computational Cryptography: Protocols, Hashes and Commitments

Name: Flavio D. Garcia

Topic: Formal and Computational Cryptography: Protocols, Hashes and Commitments

Category: cryptographic protocols

Description: In modern society we are surrounded by distributed systems. Most electronic devices that are currently on the market have some networking capability or are able to communicate with each other. Communication\r\nover shared media is inherently insecure. Therefore, proper design of security protocols is of primary concern. The design and analysis of security protocols is a challenging task. Several protocols have been proposed in the\r\nliterature which later were found to be flawed. This is a consequence of the intrinsic complexity associated with the presence of a malicious adversary. The traditional complexity-theoretical adversarial model is realistic but complex. As a consequence of this, designing and analyzing protocols in\r\nthis model is error prone. The Dolev-Yao model refers to the attacker model in which an adversary has complete control over the communication media. In this model, the adversary is not bounded in running time but\r\nis completely unable to break any cryptographic primitive. This model is satisfactory as it provides a good level of abstraction. Proofs are simpler than the complexity-theoretical ones, and therefore less error prone, still capturing most common mistakes in the design of security protocols. This thesis addresses the problem of secure protocol design from both formal and computational perspectives and also studies the relation among them. We present four original contributions:\r\n• We present a decentralized digital currency for peer-to-peer and grid applications that is able to detect double-spending of the coins and\r\nother types of fraud.\r\n• We develop a formal framework for the analysis of anonymizing protocols in terms of epistemic logic. We illustrate our approach by proving sender anonymity and unlinkability of some well-known anonymizing protocols.\r\n• We relate the Dolev-Yao model, extended with hash functions, with a realistic computational model. We use a special randomized construction to interpret hashes.[...]