International Association for Cryptologic Research

Ph.D. Database

The aim of the IACR Ph.D. database is twofold. On the first hand, we want to offer an overview of Ph.D. already completed in the domain of cryptology. Where possible, this should also include a subject classification, an abstract, and access to the full text. On the second hand, it deals with Ph.D. subjects currently under investigation. This way, we provide a timely map of contemporary research in cryptology. All entries or changes need to be approved by an editor. You can contact them via phds (at)


Ben Smyth (#694)
Name Ben Smyth
Personal Homepage
Topic of his/her doctorate. Formal verification of cryptographic protocols with automated reasoning
Category cryptographic protocols
Keywords anonymity, attack, cryptographic protocols, Direct Anonymous Attestation, election schemes, election verifability, electronic voting, privacy, trusted computing, user-controlled anonymity, verification
Ph.D. Supervisor(s) Mark D. Ryan
Year of completion 2011

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.

Your Ph.D. thesis as fulltext 87_BenSmyth_Formalverificationcryptographi.pdf
Last Change 2011-09-27 23:57:21
To provide an update on this entry, please click .

Contact: phds (at)

[ IACR home page ] [ IACR PhDs page ] © IACR