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 publication type
See also:
Google Scholar,
DBLP,
AMiner,
Microsoft Academic,
Semantic Scholar,
ORCID
Drafts
2020
2019
2018
- Elizabeth A. Quaglia & Ben Smyth (2018) Secret, verifiable auctions from elections. Theoretical Computer Science, vol. 730, pp. 44-92.
- Elizabeth A. Quaglia & Ben Smyth (2018) Authentication with weaker trust assumptions for voting systems. In AFRICACRYPT'18: 10th International Conference on Cryptology in Africa, LNCS 10831, Springer, pp. 322-343.
- Tom Chothia, Joeri de Ruiter & Ben Smyth (2018) Modelling and Analysis of a Hierarchy of Distance Bounding Attacks. In USENIX Security'18: 27th USENIX Security Symposium, USENIX Association.
- Bruno Blanchet & Ben Smyth (2018) Automated reasoning for equivalences in the applied pi calculus with barriers. Journal of Computer Security, 26(3), pp. 367-422.
- Ben Smyth (2018) Verifiability of Helios Mixnet. In Voting'18: 3rd Workshop on Advances in Secure Electronic Voting, LNCS 10958, Springer, pp. 247-261.
- Maxime Meyer, Elizabeth A. Quaglia & Ben Smyth (2018) Attacks against GSMA's M2M Remote Provisioning. In FC'18: 22nd International Conference on Financial Cryptography and Data Security, LNCS 10957, Springer, pp. 243-252. (First appeared at Black Hat Europe 2017.)
2017
2016
2015
2014
2013
2012
- Dalia Khader, Ben Smyth, Peter Y. A. Ryan & Feng Hao (2012) A Fair and Robust Voting System by Broadcast. In EVOTE'12: 5th International Conference on Electronic Voting, Lecture Notes in Informatics 205, Gesellschaft für Informatik, pp. 285-299.
- Mark D. Ryan, Ben Smyth & Guilin Wang, editors (2012) Proceedings of the 8th International Conference on Information Security Practice and Experience (ISPEC'12). LNCS 7232, Springer.
- Fangming Zhao, Yoshikazu Hanatani, Yuichi Komano, Ben Smyth, Satoshi Ito & Toru Kambayashi (2012) Secure Authenticated Key Exchange with Revocation for Smart Grid. In ISGT'12: 3rd IEEE Power & Energy Society Conference on Innovative Smart Grid Technologies, IEEE Computer Society.
2011
- David Bernhard, Véronique Cortier, Olivier Pereira, Ben Smyth & Bogdan Warinschi (2011) Adapting Helios for provable ballot privacy. In ESORICS'11: 16th European Symposium on Research in Computer Security, LNCS 6879, Springer, pp. 335-354.
- Ben Smyth, Mark D. Ryan & Liqun Chen (2011) Formal analysis of anonymity in ECC-based Direct Anonymous Attestation schemes. In FAST'11: 8th International Workshop on Formal Aspects of Security and Trust, LNCS 7140, Springer, pp. 245-262.
- Véronique Cortier & Ben Smyth (2011) Attacking and fixing Helios: An analysis of ballot secrecy. In CSF'11: 24th Computer Security Foundations Symposium, IEEE Computer Society, pp. 297-311.
- Mark D. Ryan & Ben Smyth (2011) Applied pi calculus. Chapter in Véronique Cortier & Steve Kremer (editors) Formal Models and Techniques for Analyzing Security Protocols, IOS Press.
- Ben Smyth (2011) Formal verification of cryptographic protocols with automated reasoning. PhD thesis, School of Computer Science, University of Birmingham.
2010
2008
2007
Miscellaneous