Research

I'm no longer pursuing academic research actively. Works already in the publication pipeline may emerge. (Perhaps the occasional piece of weekend writing too.)

Prior to startup life, I conducted research on electronic voting systems designed to provide strong notions of secrecy and to provide verifiable proof of correct operation:

I developed a framework for proving verifiability of voting systems, applied that framework to analyse Helios, Helios-C, helios-server-mixnet, JCJ, and Zeus, found vulnerabilities in each, introduced patches, and proved my patches restore security (IACR'19, Voting'18, AFRICACRYPT'18, ESORICS'10, ARSPA-WITS'10). I also surveyed existing frameworks for proving verifiability, finding each to be inadequate (IPL'20).

I developed a compatible framework for ballot secrecy, analysed Helios, helios-server-mixnet, and Zeus, found vulnerabilities in Helios, introduced patches, and proved my patches secure (IACR'19, IJSN'19, IWSEC'15, JCS'12, ESORICS'13, CSF'11). I also extended the ProVerif software tool to enable automated analysis of ballot secrecy (JCS'18, CSF'16, IFIPTM'08).

Ballot secrecy offers minimal privacy; stronger secrecy notions are needed to prevent vote selling and coercion. I surveyed existing frameworks for proving whether a voting system prevents vote selling (ProvSec'19) and coercion (IACR'19), largely finding frameworks inadequate. Additionally, I built Athena, a verifiable, coercion-resistant voting system with linear complexity (IACR'19).

I identified a relationship between voting and auction systems, exploited that relation to build auction systems Hawk and Aucitas from the Helios and Civitas voting systems (FC'14), and generalised results to derive a construction for secure, verifiable auction systems from voting systems (TCS'18).

Beyond voting systems, I discovered attacks against GSMA's next generation eSIM architecture (FC'18). Discovered TLS truncation attacks against Microsoft Live, Google, and Helios (Black Hat'13,WOOT'13). And discovered an attack against the RSA-based Direct Anonymous Attestation system by HP, IBM, and Intel (ESAS'07), developed a framework for proving security of such systems, and proved that my patch suffices to secure the aforementioned RSA-based system (SCP'15,FAST'11).

I've written introductory texts on: TLS 1.3 and OpenJDK's implementation (arXiv'20), GSMA's next generation eSIM architecture (arXiv'19), secret, verifiable elections (IACR'18,arXiv'18), the Applied Pi calculus (IOS Press'11), and the ProVerif software tool that can be used to automatically analyse systems modelled in a variant of that calculus (2011).

Publications

Sort by publication type
See also: Google Scholar, DBLP, AMiner, Microsoft Academic, Semantic Scholar, ORCID

Drafts

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2008

2007

Miscellaneous