Amphiteatre Maison Jean Kuntzmann
25 November 2013 - 14h00
PhD Defense: Formal Verification of Voting and Auction Protocols: From Privacy to Fairness and Verifiability
by Jannik Dreier from VERIMAG
Abstract: In this thesis, we formally analyze security in electronic voting and electronic auctions. On-line voting over is now available in several countries, for example in Estonia or parts of Switzerland. Similarly, electronic auctions are increasingly used: eBay had over 112 million active users and over 350 million listings in 2012, and achieved a revenue of more than 14 billion US Dollars. In both applications, security is a main concern, as fairness is important and money is at stake.
In the case of voting protocols, privacy is crucial to ensure free elections. We propose a hierarchy of privacy notions in the Applied Pi-Calculus, including different levels of coercion, special attacks such as forced-abstention attacks, and inside attackers. We also provide generalized notions for situations where votes are weighted (e.g. according to the number of shares in a company), and show that for many protocols the case with multiple coerced voters can be reduced to the case with one coerced voter. This result is made possible by a unique decomposition result in the Applied Pi-Calculus showing that any finite process has a unique normal form with respect to labeled bisimilarity. Moreover we provide multiple case studies illustrating how our taxonomy allows to assess the level of privacy ensured by a voting protocol.
In the case of auction protocols we also consider a hierarchy of privacy notions, and several fairness and authentication properties such as Non-Interference, Non-Cancellation and Non-Repudiation. We analyze all these properties automatically using ProVerif on three case studies, and identify several flaws. Moreover we give an abstract definition of verifiability in auctions and provide case studies in the symbolic and computational model using ProVerif and CryptoVerif respectively. Again, we identify several shortcomings, but also give a computational proof for one protocol.
Finally we explore the idea of ``true bidder-verifiable auctions'', i.e. auctions that can be verified by a non-expert, as the property is ensured through physical properties instead of complex cryptography. We propose two such protocols, discuss how to model the underlying physical properties, and provide a formal analysis of both protocols using ProVerif.
