key: 2011-PhD-thesis
type: phdthesis
title: Formal verification of cryptographic protocols with automated reasoning
authors:
  - Ben Smyth
year: 2011
month: 3
school: School of Computer Science
address: University of Birmingham
description: >-
  This page contains Ben Smyth's PhD thesis entitled 'Formal verification of cryptographic protocols
  with automated reasoning.'
keywords: >-
  cryptographic protocols, verification, formal methods, observational equivalence, applied pi
  calculus, ProSwapper, ProVerif, election verifability, electronic voting, privacy, anonymity,
  user-controlled anonymity, Direct Anonymous Attestation, trusted computing, attack, vulnerability,
  analyzing, security protocols, protocols, formal models
abstract: >-
  <p>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.</p>
  <p>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
  <i>the rules</i> and may deviate from <i>expected behaviours</i>. Secure cryptographic protocols
  are therefore notoriously difficult to define. Accordingly, cryptographic protocols must be
  scrutinised by experts using procedures that can evaluate security properties.</p> <p>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. </p> <p>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.</p>
extra: >
  <h2>Summary of contents:</h2>

  <p>Part I Preliminaries</p>

  <ul>

  <li>Chapter 1 - Introduction</li>

  <li>Chapter 2 - Background: Applied pi calculus</li>

  </ul>


  <p>Part II Formalisation of security properties</p>

  <ul>

  <li>Chapter 3 - Election verifability in electronic voting<br/>

  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.<br/>&nbsp;

  </li>

  <li>Chapter 4 - Anonymity in Direct Anonymous Attestation<br/>

  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 &amp; 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.

  </li>

  </ul>


  <p>Part III Automated reasoning</p>

  <ul>

  <li>Chapter 5 - Observational equivalence and barriers<br/>

  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 <i>ProSwapper</i>,

  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.</li>

  </ul>


  <p>Part IV Evaluation</p>

  <ul>

  <li>Chapter 6 - Further work and conclusion</li>

  </ul>
links:
  - file: Smyth11-PhD-Thesis.pdf
    text: Thesis
    alt:
      url: http://etheses.bham.ac.uk/1604/
      text: Birmingham eTheses version