Professor Steve Schneider


Director of Computer Science Research Centre
PhD, FBCS, FIET
PA: Denise Myers
+44 (0)1483 686058

About

Areas of specialism

Secure Electronic Voting; Distributed Ledger Technologies; Rail and Automotive Security; Security and Privacy; Formal modeling and verification

University roles and responsibilities

  • Director of the Computer Science Research Centre

    Previous roles

    2004 - 2010
    Head of Department of Computer Science
    University of Surrey
    2015 - 2019
    Associate Dean (Research and Innovation), Faculty of Engineering and Physical Sciences
    University of Surrey

    Research

    Research interests

    Research projects

    Research collaborations

    Indicators of esteem

    • My work on secure electronic voting has led to the development of a verifiable voting system used in the November 2014 State election in the State of Victoria, Australia.

      Teaching

      Publications

      Google Scholar

      Books and chapters

      The B-Method: an Introduction, Steve Schneider, Palgrave Cornerstones in Computer Science. 2001

      Modelling and Analysis of Security Protocols (PDF), Peter Y.A. Ryan, Steve Schneider, Michael Goldsmith, Gavin Lowe & Bill Roscoe,Pearson Education, 2000. The book also has a companion website

      Concurrent and Real Time Systems: the CSP Approach (PDF), Steve Schneider, John Wiley, 1999. The book also has a companion website

      Verifiable Voting Systems (PDF), Thea Peacock, Peter Y. A. Ryan, Steve Schneider & Zhe Xia, Chapter 69 of Computer and Information Security Handbook, 2nd Edition, John R. Vacca (ed), Elsevier 2013.

      Prêt à Voter: the Evolution of the Species, Peter Y.A, Ryan, Steve Schneider & Vanessa Teague, Chapter 12 in Real World Electronic Voting: Design, Analysis and Deployment, Feng Hao & Peter Y.A. Ryan (eds), 2016.

       

      Publications

      2016

      Foundations for using Linear Temporal Logic in Event-B Refinement, Steve Schneider, Helen Treharne, Heike Wehrheim & David Williams, Formal Aspects of Computing, 2016.

      Verifiable Electronic Voting in Practice: the use of vVote in the Victorian State Election , Craig Burton, Chris Culnane & Steve Schneider, IEEE Security & Privacy, 2016.

      2015

      End-to-End Verifiability in Voting Systems, from Theory to Practice (author version) , Peter Y.A. Ryan, Steve Schneider & Vanessa Teague, IEEE Security & Privacy 13(3), 2015.

      A Formal Framework for Security Analysis of NFC Mobile Coupon Protocols , Ali Alshehri & Steve Schneider, Journal of Computer Security 23(6), 2015.

      vVote: a Verifiable Voting System , Chris Culnane, Peter Y.A. Ryan, Steve Schneider & Vanessa Teague, ACM Transactions on Information Systems Security, 18(1), 2015.

      Automated Anonymity Verification of the ThreeBallot and VAV Voting Systems , Murat Moran, James Heather, & Steve Schneider, Software and Systems Modelling, 2015.

      2014

      Decomposing Scheme Plans to Manage Verification Complexity , Phillip James, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider & Helen Treharne, FORMS/FORMAT 10th Symposium on Formal Methods, 2014.

      Managing LTL properties in Event-B refinement , Steve Schneider, Helen Treharne, Heike Wehrheim & David M. Williams, Integrated Formal Methods IFM 2014.

      On Modelling and Verifying Railway Interlockings: Tracking Train Lengths , Phillip James, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider & Helen Treharne, Science of Computer Programming 96, 2014.

      Robustness Modelling and Verification of a Mix Net Protocol , Efstathios Stathakidis, Steve Schneider & James Heather, Security Standardisation Research - First International Conference, SSR 2014.

      A Peered Bulletin Board for Robust Use in Verifiable Voting Systems , Chris Culnane & Steve Schneider, IEEE 27th Computer Security Foundations Symposium, 2014.

      Techniques for Modelling and Verifying Railway Interlockings,Phillip James, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider & Helen Treharne, International Journal of Software Tools for Technology Transfer, March 2014.

      The Behavioural Semantics of Event-B Refinement. (author version)Steve Schneider, Helen Treharne & Heike Wehrheim, Formal Aspects of Computing 26(2), 2014.

      Verifying Anonymity in Voting Systems using CSP,Murat Moran, James Heather & Steve Schneider, Formal Aspects of Computing, 26(1), 2014.

      Cryptographic Protocols with Everyday Objects,James Heather, Steve Schneider & Vanessa Teague, Formal Aspects of Computing, 26(1), 2014.

      Faster Print on Demand for Prêt à Voter ,Chris Culnane, James Heather, Rui Joaquim, Peter Y. A. Ryan, Steve Schneider & Vanessa Teague, USENIX Journal of Election Technology and Systems (JETS) Volume 2 Issue 1, and Electronic Voting Technology Workshop/Workshop on Trustworthy Elections, EVT/WOTE'14.

      2013

      Formal security analysis and improvement of a hash-based NFC M-coupon protocol,Ali Alshehri & Steve Schneider, 12th Smart Card Research and Advanced Application Conference, CARDIS 2013.

      Formally defining NFC M-coupon requirements, with a case study,Ali Alshehri & Steve Schneider, 8th International Conference for Internet Technology and Secured Transactions, ICITST 2013.

      Testing Voters' Understanding of a Security Mechanisms used in Verifiable Voting ,Morgan Llewellyn, Steve Schneider, Zhe Xia, Chris Culnane, James Heather, Peter Y. A. Ryan & Sriramkrishnan Srinivasan, USENIX Journal of Election Technology and Systems (JETS) Volume 1 Issue 1, and Electronic Voting Technology Workshop/Workshop on Trustworthy Elections, EVT/WOTE'13.

      Automated Anonymity Verification of the ThreeBallot Voting SystemMurat Moran, James Heather & Steve Schneider, 10th International Conference on integrated Formal Methods, iFM 2013.

      Solving the discrete logarithm problem for packing candidate preferences,James Heather, Chris Culnane, Steve Schneider, Sriramkrishnan Srinivasan & Zhe Xia, 2nd International Workshop on Modern Cryptography and Security Engineering, MoCrySEn 2013.

      On key sizes for electronic voting,Sriramkrishnan Srinivasan, Chris Culnane, James Heather, Steve Schneider & Zhe Xia, 7th Chinese Conference on Trusted Computing and Information Security, 2013.

      Policy templates for relationship-based access control,,Evangelos Aktoudianakis, Jason Crampton, Steve Schneider, Helen Treharne & Adrian Waller, 11th Annual Conference on Privacy, Security and Trust, PST 2013.

      OnTrack: An Open Tooling Environment for Railway Verification,Phillip James, Matthew Trumble, Helen Treharne, Markus Roggenbach & Steve Schneider, 5th NASA Formal Methods Symposium, NFM 2013.

      On Modelling and Verifying Railway Interlockings: Tracking Train Lengths,Phillip James, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider & Helen Treharne, Technical Report CS-13-03, Department of Computer Science, University of Surrey, 19 May 2013.

      Formal security analysis of NFC coupon protocols using Casper/FDR,Ali Alshehri, Johann A. Briffa, Steve Schneider & Stephan Wesemeyer, 5th International Workshop on Near Field Communication, NFC 2013.

      Software Design for VEC vVote System, Chris Culnane, James Heather, Steve Schneider and Zhe Xia, Technical Report CS-13-01, 26 March 2013, Department of Computer Science, University of Surrey.

      Software Requirements Specification for VEC vVote System,Matthew Casey, Chris Culnane, James Heather and Steve Schneider, Technical Report CS-13-02, 26 March 2013, Department of Computer Science, University of Surrey

      2012

      Using Prêt à Voter in Victoria State Elections,Craig Burton, Chris Culnane, James Heather, Thea Peacock, Peter Y.A. Ryan, Steve Schneider, Sriram Srinivasan, Vanessa Teague, Roland Wen & Zhe Xia, Electronic Voting Technology/Workshop on Trustworthy Elections, EVT/WOTE 2012.

      A supervised verifiable voting protocol for the Victorian Electoral Commission,Craig Burton, Chris Culnane, James Heather, Thea Peacock, Peter Y.A. Ryan, Steve Schneider, Sriram Srinivasan, Vanessa Teague, Roland Wen & Zhe Xia, 5th International Conference on Electronic Voting, EVOTE 2012

      Verifying anonymity in voting systems using CSP,Murat Moran, James Heather, Steve Schneider, Formal Aspects of Computing Journal, December 2012.

      An integrated framework for checking the behaviour of fUML models using CSP,Islam Abdelhalim, Steve Schneider & Helen Treharne, International Journal on Software Tools for Technology Transfer, 2012.

      An optimization approach for effective formalized fUML model checking,Islam Abdelhalim, Steve Schneider & Helen Treharne, 10th International Conference on Software Engineering and Formal Methods, SEFM 2012.

      A formal framework for modelling coercion-resistance and receipt-freeness,James Heather & Steve Schneider, 18th International Symposium on Formal Methods, FM 2012.

      Railway modelling in CSP||B : the Double Junction case study,Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider & Helen Treharne, Proceedings of the 12th International Workshop on Automated Verification of Critical Systems, AVOCS 2012. See also Department of Computing Technical Report CS-12-03

      Defining and model checking abstractions of complex railway models using CSP||B,Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider & Helen Treharne, Haifa Verification Conference HVC 2012.

      Combining event-based and state-based modelling for railway verification,Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider & Helen Treharne, Department of Computer Science Technical Report CS-12-02, 2012.

      2011

      Bounded Retransmission in Event-B||CSP: a Case Study,Steve Schneider, Helen Treharne & Heike Wehrheim, B2011 Workshop, Limerick, 2011. Also: Department of Computer Science Technical Report CS-11-04, University of Surrey 2011

      Cryptographic Protocols with Everyday Objects,James Heather, Steve Schneider & Vanessa Teague, Cryptoforma Workshop on Formal Methods and Cryptography, Limerick, 2011

      Anonymity and CSP for Voting Systems,Murat Moran, James Heather & Steve Schneider, Cryptoforma Workshop on Formal Methods and Cryptography, Limerick,2011

      Authentication Codes,Chris Culnane, David Bismark, James Heather, Steve Schneider, Sriram Srivinasan & Zhe Xia, EVT/WOTE Electronic Voting Technology Workshop/Workshop on Trustworthy Elections, San Francisco, 2011

      Towards a Practical Approach to Check UML/fUML Models Cinsistency Using CSP,Islam AbdelHalim, Steve Schneider & Helen Treharne, ICFEM: 13th International Conference on Formal Engineering Methods, Durham, 2011

      A CSP account of Event-B refinement,Steve Schneider, Helen Treharne & Heike Wehrheim, REFINE'11: Refinement Workshop, Limerick, 2011

      Focus Group Views on Prêt à Voter 1.0,Steve Schneider, Morgan Llewellyn, Chris Culnane, James Heather, Sriramkrishnan Srinivasan & Zhe Xia, RE-Vote: International Workshop on Requirements Engineering for Electronic Voting Systems, Trento, 2011

      Feasibility Analysis of Prêt à Voter for German Federal Elections,Denise Demirel, Maria Henning, Peter Y. A. Ryan, Steve Schneider & Melanie Volkamer, Vote-ID: International Conference on e-Voting and Identity, Tallinn, Estonia, 2011

      Prêt à Voter with write-ins,Steve Schneider, Sriramkrishnan Srivinasan, Chris Culnane, James Heather & Zhe Xia, Vote-ID: International Conference on e-Voting and Identity, Tallinn, Estonia, 2011

      A formal framework for modelling coercion-resistance and receipt-freeness,James Heather & Steve Schneider, 2011

      Stepwise Refinement in Event-B||CSP. Part 1: Safety,Steve Schneider, Helen Treharne & Heike Wehrheim, Department of Computer Science Technical Report CS-11-03, University of Surrey 2011

      2010

      Changing system interfaces consistently: a new refinement strategy for CSP||B,Steve Schneider & Helen Treharne, Science of Computer Programming, 2010

      Versatile Prêt à Voter: Handling Multiple Election Methods with a Unified Interface,Zhe Xia, Chris Culnane, James Heather, Hugo Jonker, Peter Ryan, Steve Schneider, & Sriram Srivinasan, IndoCrypt 2010

      Formal Verification of Tokeneer Behaviours Modelled in fUML using CSP,Islam Abdelhalim, James Sharp, Steve Schneider & Helen Treharne, ICFEM 2010

      A CSP Approach to Control in Event-B,Steve Schneider, Helen Treharne & Heike Wehrheim, IFM 2010

      2009

      The Prêt à Voter Verifiable Election System,Peter Ryan, David Bismark, James Heather, Steve Schneider & Zhe Xia, IEEE Transactions in Information Security and Forensics, 2009

      Specifying authentication using signal events in CSP,Siraj Shaikh, Vicky Bush & Steve Schneider, Computers & Security 28(5), 2009

      Mobile CSP||B,Beeta Vajar, Steve Schneider & Helen Treharne, AVOCS 2009

      Experiences Gained from the first Prêt à Voter Implementation,David Bismark, James Heather, Roger Peel, Steve Schneider, Zhe Xia & Peter Ryan, RE-Vote 2009

      Changing system interfaces consistently: a new refinement strategy for CSP||B,Steve Schneider & Helen Treharne, IFM 2009, LNCS

      A step towards refining and translating B control annotations to Handel-C,Wilson Ifill & Steve Schneider, Concurrency and Computation: Practice and Experience, 2009

      Modelling and analysis of the AMBA bus using CSP and B,Alistair McEwan & Steve Schneider, Concurrency and Computation: Practice and Experience, 2009

      2008

      Experiments in translating CSP || B to Handel-C,Steve Schneider, Helen Treharne, Alistair McEwan & Wilson Ifill, CPA 2008

      Analysis, improvement, and simplification of Prêt à Voter with Paillier encryption,Zhe Xia, Steve A. Schneider, James Heather & Jacques Traoré, EVT 2008

      Automatic generation of CSP || B skeletons from xUML models,Edward Turner, Helen Treharne, Steve Schneider & Neil Evans, ICTAC 2008

      2007

      Introducing mobility into CSP||B,Steve Schneider, Helen Treharne & Beeta Vajar, AVOCS 2007.

      Augmenting B with control annotations,Wilson Ifill, Steve Schneider & Helen Treharne, B 2007, LNCS

      Modeling and analysis of the AMBA bus Using CSP and B,Alistair A. McEwan & Steve Schneider, CPA 2007

      A step towards refining and translating B control annotations to Handel-C,Wilson Ifill & Steve Schneider, CPA 2007

      Threat analysis of a practical voting scheme with receipts,Sébastien Foulle, Steve Schneider, Jacques Traoré & Zhe Xia, VOTE-ID 2007

      Prêt à Voter: All-In-One,Zhe Xia, Steve Schneider, James Heather, Peter Y. A. Ryan, David Lundin, Roger Peel & Phil Howard, WOTE 2007.

      An algebraic approach to the verification of a class of Diffie-Hellman protocols,Rob Delicata & Steve Schneider, International Journal on Information Security, 6(2-3), 2007

      Augmenting B with control annotations,Wilson Ifill, Steve Schneider & Helen Treharne, B 2007, LNCS.

      2006

      Prêt à Voter with re-encryption mixes,Peter Y. A. Ryan & Steve Schneider, ESORICS 2006, LNCS

      A layered behavioural model of platelets,Steve Schneider, Helen Treharne, Ana Cavalcanti & Jim Woodcock, ICECCS 2006

      Tank monitoring: a pAMN case study,,Steve Schneider, Son Hoang, Ken Robinson & Helen Treharne, Formal Aspects of Computing 18(3), 2006.

      A new receipt-free e-voting scheme based on blind signature,Zhe Xia & Steve Schneider, WOTE 2006.

      A verified development of hardware using CSP||B,Alistair McEwan & Steve Schneider, MEMOCODE 2006.

      2005

      CSP theorems for communicating B machines,Steve Schneider & Helen Treharne, Formal Aspects of Computing, 17(4) 2005. also: Technical report, Royal Holloway

      A practical voter verifiable election scheme,David Chaum, Peter Y. A. Ryan & Steve Schneider, European Symposium on Research in Computer Security, 2005, LNCS.

      Chunks: component verification in CSP||B,Steve Schneider, Helen Treharne & Neil Evans, IFM 2005, LNCS

      A formal approach for reasoning about a class of Diffie-Hellman protocols,Roberto Delicata & Steve Schneider, Formal Aspects of Security and Trust 2005, LNCS.

      Temporal rank functions for forward secrecy,Roberto Delicata & Steve Schneider, 18th IEEE Computer Security Foundations Workshop.

      A decision procedure for the existence of a rank function,James Heather & Steve Schneider, Journal of Computer Security, 13 (2).

      Timed CSP: a retrospective,Joel Ouaknine and Steve Schneider, APC 2005

      Formal verification of fault-tolerant software design: the CSP approach,W Lok Yeung and Steve Schneider, Microprocessors and Microsystems, 29(5), 2005

      2004

      Verifying security protocols: an application of CSP,Steve Schneider & Roberto Delicata, Communicating Sequential Processes, the first 25 years, 2004, LNCS 3525

      Verifying controlled components,Steve Schneider & Helen Treharne, Integrating Formal Methods 2004. Winner of the conference best paper award.

      2003

      Investigating a file transmission protocol using CSP and B,Neil Evans, Steve Schneider & Helen Treharne, (extended abstract), State-oriented cs Event-oriented thinking, ST.EVE 2003.

      How to prevent type flaw attacks on security protocols,James Heather, Gavin Lowe & Steve Schneider, Journal of Computer Security, 2003, 11 (2).

      Design and verification of distributed recovery blocks with CSP,W Lok Yeung & Steve Schneider, Formal Methods in Systems Design, 2003, 22.

      Composing specifications using communication,Helen Treharne, Steve Schneider & Marchia Bramble, ZB 2003.

      pre 2003

      Verifying authentication protocol implementations,Steve Schneider, FMOODS 2002.

      Communicating B machines,Helen Treharne & Steve Schneider, ZB2002: International Conference of Z and B Users, LNCS.

      Process algebra and non-interference,Peter Y. A. Ryan & Steve Schneider, Journal of Computer Security, (9) 1-2, 2001

      May testing, non-interference, and compositionality,Steve Schneider, Electronic Notes in Computer Science 40, 2001.

      How to drive a B machine,Helen Treharne & Steve Schneider, 2nd International conference of Z and B Users, LNCS, 2000. Winner of the conference best paper award.

      Analysing time dependent security properties in CSP with PVS,Neil Evans & Steve Schneider, ESORICS 2000.

      Process algebra and non-interference,Peter Y. A. Ryan & Steve Schneider. CSFW 1999

      Formal analysis of a non-repudiation protocol,Steve Schneider, CSFW 1998

      Test case preparation using a prototype,Helen Treharne, Jon Draper & Steve Schneider, B 1998:

      CSP, PVS and a recursive authentication protocol,Jeremy Bryans & Steve Schneider, DIMACS 1997.

      Verifying authentication protocols with CSP,Steve Schneider, CSFW 1997

      Using a PVS embedding of CSP to verify authentication protocols,Bruno Dutertre & Steve Schneider, TPHOLs 1997

      CSP and anonymity,Steve Schneider & Abraham Sidiropoulos, ESORICS 1996, LNCS

      Security properties and CSP,Steve Schneider, IEEE Symposium on Security and Privacy 1996, (technical report)

      Using CSP for protocol analysis: the Needham-Schroeder Public-Key Protocol,Steve Schneider, Royal Holloway Technical Report 1996.

      Timewise refinement for communicating processes,Steve Schneider, MFPS 1993