Formal verification of cryptographic protocols with automated reasoning

Ben Smyth (2011) Formal verification of cryptographic protocols with automated reasoning. PhD thesis, School of Computer Science, University of Birmingham.

Download

Abstract

Cryptographic protocols form the backbone of our digital society. Unfortunately, the security of numerous critical components has been neglected. As a consequence, attacks have resulted in financial loss, violations of personal privacy, and threats to democracy. This thesis aids the secure design of cryptographic protocols and facilitates the evaluation of existing schemes.

Developing a secure cryptographic protocol is game-like in nature, and a good designer will consider attacks against key components. Unlike games, however, an adversary is not governed by the rules and may deviate from expected behaviours. Secure cryptographic protocols are therefore notoriously difficult to define. Accordingly, cryptographic protocols must be scrutinised by experts using procedures that can evaluate security properties.

This thesis advances verification techniques for cryptographic protocols using formal methods with an emphasis on automation. The key contributions are threefold. Firstly, a definition of election verifiability for electronic voting protocols is presented; secondly, a definition of user-controlled anonymity for Direct Anonymous Attestation is delivered; and, finally, a procedure to automatically evaluate observational equivalence is introduced.

This work enables security properties of cryptographic protocols to be studied. In particular, we evaluate security in electronic voting protocols and Direct Anonymous Attestation schemes; discovering, and fixing, a vulnerability in the RSA-based Direct Anonymous Attestation protocol. Ultimately, this thesis will help avoid the current situation whereby numerous cryptographic protocols are deployed and found to be insecure.

Summary of contents:

Part I Preliminaries

  • Chapter 1 - Introduction
  • Chapter 2 - Background: Applied pi calculus

Part II Formalisation of security properties

  • Chapter 3 - Election verifability in electronic voting
    A definition of election verifiability is presented in terms of boolean tests which can be performed on the data produced by an election. The definition allows the evaluation of election verifiability in electronic voting protocols. It also allows the identification of hardware and software components that must be trusted for the purpose of verifiability, thereby facilitating the comparison of electronic voting protocols on the basis of trust assumptions. Our definition of election verifiability is compatible with a large class of electronic voting schemes -- including those based upon blind signatures, homomorphic encryption and mixnets -- as will be demonstrated by analysing the FOO, Helios 2.0 and JCJ-Civitas electronic voting protocols.
     
  • Chapter 4 - Anonymity in Direct Anonymous Attestation
    A definition of user-controlled anonymity is introduced in the context of Direct Anonymous Attestation schemes. The definition is expressed as an equivalence property suited to automated reasoning using ProVerif. The practicality of the definition is demonstrated by analysing the RSA-based Direct Anonymous Attestation protocol by Brickell, Camenisch & Chen. The analysis discovers a vulnerability which can be exploited by a passive adversary and, under weaker assumptions, corrupt administrators. A security fix is identified and the revised scheme is shown to satisfy our definition of user-controlled anonymity.

Part III Automated reasoning

  • Chapter 5 - Observational equivalence and barriers
    A procedure for the automated analysis of observational equivalence is delivered. In addition, the notion of barrier synchronisation is characterised for processes. The study of barrier synchronisation in relation to equivalence is particularly interesting because certain equivalence properties can only be realised under specific synchronisation assumptions. In particular, privacy preserving protocols -- including electronic voting schemes, vehicular ad-hoc networking protocols, and anonymity networks -- make such assumptions. The results have been implemented in the tool ProSwapper, an extension to ProVerif, and the applicability of this research is demonstrated by analysing vote privacy in electronic voting protocols and privacy in vehicular ad-hoc networks.

Part IV Evaluation

  • Chapter 6 - Further work and conclusion

Bibtex Entry

@PhdThesis{2011-PhD-thesis,
	author = "Ben Smyth",
	title = "{Formal verification of cryptographic protocols with automated reasoning}",
	year = "2011",
	school = "School of Computer Science",
	address = "University of Birmingham",
	url = "http://www.bensmyth.com/files/Smyth11-PhD-Thesis.pdf",
}