Professor Steve Schneider

Professor of Computing

Qualifications: BA MSc DPhil

Email:
Phone: Work: 01483 68 9637
Room no: 08 BB 02

Office hours

Tuesdays 14:00 - 16:00.  Other times by appointment, or drop by if my door is open.

Evoting video:  See my recent video on secure electronic voting.

Article: Digital Voting is a game changer but we have to get it right

Journal of Information Security and Applications:  Guest editor of June 2014 Special Issue on E-Voting.

Vote-ID 2013:   General chair of the 4th International Conference on e-Voting and Identity: Vote-ID 2013, and the associated voting systems workshop, University of Surrey, July 17-19, 2013.

AVOCS 2013:  Co-chair of 13th International Workshop on Automated Verification of Critical Systems, AVOCS 2013, University of Surrey, September 11-13, 2013.

Further information

Biography

I am Head of the Surrey Centre for Cyber Security.  I joined the Department of Computing as Professor of Computing in September 2004, and was Head of Department from 2004-2010.  I was previously at Royal Holloway during the period 1994-2004.   I was awarded my DPhil (PhD) from the University of Oxford in 1990, and continued there as an RA from 1990-1994.   

My primary research interests are in security design and verification, and in formal methods.    

Research Interests

Secure Electronic Voting  I am currently working on secure electronic voting (see video), in particular on the Prêt à Voter secure verifiable electronic voting system.  I lead the Surrey e-voting group, which produced the first prototype implementation of Prêt à Voter, awarded `best design' at the voting systems competition conference VoComp 2007.   I am currently leading an international collaboration to provide secure electronic voting to the State of Victoria, Australia for their November 2014 State election.   I am also an investigator on the 2009-2014 EPSRC grant `Trustworthy Voting Systems'. 

Security  I have been working in Security for nearly 20 years, initially in the area of formal modelling and verification of security protocols, and in non-interference.  In particular I have developed methods for describing protocols between components interacting in an insecure environment, and to proving that they provide key authentication and confidentiality properties.  More recently I have been working on robustness and distributed trust in situations where it is important not to rely on the trustworthiness of any single individual, such as election systems.

Formal Methods  My other current research activity is on the integration of formal methods, specifically CSP and B, which are concerned with complementary aspects of system behaviour.  This combination is appropriate for systems whose formal description involves consideration of both control and state.  The resulting method, CSP||B, is designed to enable maximum use of the mature industrial strength tools for CSP and for B, within a single framework.  We are currently working on applying the approach to the modelling and analysis of safety in railway systems.

My background is in the theory of concurrency and its applications, and I have been working for a number of years on the process algebra CSP (Communicating Sequential Processes) and the development of its timed extension: Timed CSP.  I have also worked on the modelling and verification of security protocols.  

Publications

Google Scholar Citations

Books and chapters

The B-Method: an Introduction (PDF) ,
Steve Schneider, S.A
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.

Publications

2014

A Peered Bulletin Board for Robust Use in Verifiable Voting Systems,
Chris Culnane & Steve Schneider, arXiv:1401.4151, 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 System
Murat 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 Computing, 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 Computing, 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 Computing, 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 Computing 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 Computing 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 Computing 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
 

Teaching

I am teaching two courses in 2013-14:

  • Computer Security (Spring Semester)
  • Data Structures and Algorithms (Spring Semester)

 

Departmental Duties

Director of Research

Research Excellence Framework (REF2014) UoA Lead for Computing (to November 2013)

Page Owner: css1ss
Page Created: Tuesday 2 December 2008 10:10:56 by mf0009
Last Modified: Wednesday 25 June 2014 15:54:21 by css1ss
Assembly date: Wed Jul 30 17:17:10 BST 2014
Content ID: 2143
Revision: 54
Community: 1028