Research

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 voting selling and coercion. I surveyed existing frameworks for proving whether a voting system prevents voting 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 HP, IBM, and Intel's RSA-based Direct Anonymous Attestation system (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 year
See also: Google Scholar, DBLP, AMiner, Microsoft Academic, Semantic Scholar, ORCID

Edited Proceedings

Chapters in Books

Journal articles

Thesis

Conference Papers

Miscellaneous