I no longer pursue academic research. Works already in the publication pipeline may emerge.
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 patched systems secure (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 patched Helios 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 baseline privacy; stronger privacy notions are necessary 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 my patch sufficient to secure the 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 ProVerif (2011), a software tool for automatic analysis of systems modelled in a variant of that calculus.
Publications
Sort by publication type
See also:
Google Scholar,
DBLP,
AMiner,
Microsoft Academic,
Semantic Scholar,
ORCID
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
- Ben Smyth (2020) Mind the Gap: Individual- and universal-verifiability plus cast-as-intended don't yield verifiable voting systems. Cryptology ePrint Archive Technical Report 2020/1054.
- Thomas Haines & Ben Smyth (2020) Surveying definitions of coercion resistance. Cryptology ePrint Archive Technical Report 2019/822.
- Ben Smyth (2020) TLS 1.3 for engineers: An exploration of the TLS 1.3 specification and OpenJDK's Java implementation. arXiv Technical Report 1904.02148.
- Ben Smyth (2019) Athena: A verifiable, coercion-resistant voting system with linear complexity. Cryptology ePrint Archive Technical Report 2019/761.
- Maxime Meyer, Elizabeth A. Quaglia & Ben Smyth (2019) An Overview of GSMA's M2M Remote Provisioning Specification. arXiv Technical Report 1906.02254.
- Ben Smyth (2019) Ballot secrecy: Security definition, sufficient conditions, and analysis of Helios. Cryptology ePrint Archive Technical Report 2015/942.
- Ben Smyth, Steven Frink & Michael R. Clarkson (2019) Election Verifiability: Cryptographic Definitions and an Analysis of Helios, Helios-C, and JCJ. Cryptology ePrint Archive Technical Report 2015/233.
- Ben Smyth (2018) A foundation for secret, verifiable elections. Cryptology ePrint Archive Technical Report 2018/225.
- Elizabeth A. Quaglia & Ben Smyth (2018) A short introduction to secrecy and verifiability for elections. arXiv Technical Report 1702.03168.
- Ben Smyth (2018) First-past-the-post suffices for ranked voting.
- Bruno Blanchet, Ben Smyth, Vincent Cheval & Marc Sylvestre (2018) ProVerif 2.00: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial. Originally appeared as Bruno Blanchet and Ben Smyth (2011) ProVerif 1.85: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial.
- Ben Smyth & Alfredo Pironti (2015) Truncating TLS Connections to Violate Beliefs in Web Applications. INRIA Technical Report hal-01102013.
- Ben Smyth (2014) Forget Me Do: Empowering user privacy on social network sites. Forget Me Do Limited Technical Report 2014/10.
- David Bernhard & Ben Smyth (2014) Ballot secrecy with malicious bulletin boards. Cryptology ePrint Archive Technical Report 2014/822.
- Ben Smyth & David Bernhard (2014) Ballot secrecy and ballot independence: definitions and relations. Cryptology ePrint Archive Technical Report 2013/235.
- Ben Smyth (2012) Replay attacks that violate ballot secrecy in Helios. Cryptology ePrint Archive Technical Report 2012/185.
- Ben Smyth & Véronique Cortier (2011) A note on replay attacks that violate privacy in electronic voting schemes. INRIA Technical Report RR-7643.
- Bruno Blanchet & Ben Smyth (2011) ProVerif 1.85: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial.