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 year
See also:
Google Scholar,
DBLP,
AMiner,
Microsoft Academic,
Semantic Scholar,
ORCID
Edited Proceedings
Chapters in Books
- 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.
Journal articles
- Ben Smyth (2020) Surveying global verifiability. Information Processing Letters, vol. 163.
- Ben Smyth & Yoshikazu Hanatani (2019) Non-malleable encryption with proofs of plaintext knowledge and applications to voting. International Journal of Security and Networks, 14(4), pp. 191-204.
- Maxime Meyer & Ben Smyth (2019) Exploiting re-voting in the Helios election system. Information Processing Letters, vol. 143, pp. 14-19.
- 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.
- Elizabeth A. Quaglia & Ben Smyth (2018) Secret, verifiable auctions from elections. Theoretical Computer Science, vol. 730, pp. 44-92.
- Ben Smyth, Mark D. Ryan & Liqun Chen (2015) Formal analysis of privacy in Direct Anonymous Attestation schemes. Science of Computer Programming, 111(2).
- Véronique Cortier & Ben Smyth (2013) Attacking and fixing Helios: An analysis of ballot secrecy. Journal of Computer Security, 21(1), pp. 89-148.
Thesis
Conference Papers
- Ashley Fraser, Elizabeth A. Quaglia & Ben Smyth (2019) A critique of game-based definitions of receipt-freeness for voting. In ProvSec'19: 13th International Conference on Provable and Practical Security, LNCS 11821, Springer, pp. 189-205.
- 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.
- 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.)
- Jérémie Leguay, Georgios S. Paschos, Elizabeth A. Quaglia & Ben Smyth (2017) CryptoCache: Network Caching with Confidentiality. In ICC'17: IEEE International Conference on Communications, IEEE Computer Society.
- Bruno Blanchet & Ben Smyth (2016) Automated reasoning for equivalences in the applied pi calculus with barriers. In CSF'16: 29th Computer Security Foundations Symposium, IEEE Computer Society, pp. 310-324.
- Ben Smyth, Yoshikazu Hanatani & Hirofumi Muratani (2015) NM-CPA secure encryption with proofs of plaintext knowledge. In IWSEC'15: 10th International Workshop on Security, LNCS 9241, Springer.
- Tom Chothia, Ben Smyth & Chris Staite (2015) Automatically Checking Commitment Protocols in ProVerif without False Attacks. In POST'15: 4th Conference on Principles of Security and Trust, LNCS 9036, Springer.
- Adam McCarthy, Ben Smyth & Elizabeth A. Quaglia (2014) Hawk and Aucitas: e-auction schemes from the Helios and Civitas e-voting schemes. In FC'14: 18th International Conference on Financial Cryptography and Data Security, LNCS 8437, Springer, pp. 51-63.
- Ben Smyth & Alfredo Pironti (2013) Truncating TLS Connections to Violate Beliefs in Web Applications. In WOOT'13: 7th USENIX Workshop on Offensive Technologies, USENIX Association. (First appeared at Black Hat USA 2013.)
- Ben Smyth & David Bernhard (2013) Ballot secrecy and ballot independence coincide. In ESORICS'13: 18th European Symposium on Research in Computer Security, LNCS 8134, Springer, pp. 463-480.
- 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.
- 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.
- 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.
- 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.
- 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.
- Steve Kremer, Mark D. Ryan & Ben Smyth (2010) Election verifiability in electronic voting protocols. In ESORICS'10: 15th European Symposium on Research in Computer Security, LNCS 6345, Springer, pp. 389-404.
- Ben Smyth, Mark D. Ryan, Steve Kremer & Mounira Kourjieh (2010) Towards automatic analysis of election verifiability properties. In ARSPA-WITS'10: Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, LNCS 6186, Springer, pp. 165-182.
- Stéphanie Delaune, Mark D. Ryan & Ben Smyth (2008) Automatic verification of privacy properties in the applied pi-calculus. In IFIPTM'08: 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security, International Federation for Information Processing (IFIP) 263, Springer, pp. 263-278.
- Ben Smyth, Mark D. Ryan & Liqun Chen (2007) Direct Anonymous Attestation (DAA): Ensuring privacy with corrupt administrators. In ESAS'07: 4th European Workshop on Security and Privacy in Ad hoc and Sensor Networks, LNCS 4572, Springer, pp. 218-231.
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. no. 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.