Professor Steve Schneider

Professor of Computing

Qualifications: BA MSc DPhil

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

Office hours

By appointment, or drop in if my door is open.   

Vote-ID 2013

I am general chair of Vote-ID 2013, and the associated voting systems workshop, taking place at University of Surrey on July 17-19, 2013.

See my recent video on secure electronic voting.

AVOCS 2013

I am co-chair of AVOCS 2013, taking place at University of Surrey on September 11-13, 2013.

Further information

Research Interests

My main research activity is in the area of security and formal verification, and I have worked on non-interference, and on the analysis and verification of security protocols.  I am currently working on secure electronic voting (see video), in particular on the Prêt à Voter secure verifiable electronic voting system.  I am in 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 also an investigator on the 2009-2013 EPSRC grant `Trustworthy Voting Systems'.  

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.

Publications

Google Scholar Citations

Books and chapters

Schneider, S.A. (2001). The B-Method: an Introduction, Palgrave Cornerstones in Computer Science.

Ryan, P.Y.A, Schneider, S.A., Goldsmith, M., Lowe, G. & Roscoe, A.W. (2000.) Modelling and Analysis of Security Protocols, Pearson Education. The book also has a companion website 

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

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

 

Papers

2013

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

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

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

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

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

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

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

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

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

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

2012

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

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

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

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

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

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

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

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

Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider & Helen Treharne, CSP||B modelling for railway verification: the Double Junction case study,  Department of Computing Technical Report CS-12-03, 2012.

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

2011

Steve Schneider, Helen Treharne & Heike Wehrheim Bounded Retransmission in Event-B||CSP: a Case Study, B2011 Workshop, Limerick, 2011

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

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

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

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

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

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

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

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

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

Steve Schneider, Helen Treharne & Heike Wehrheim, Bounded retransmission in Event-B||CSP: a Case Study.  Department of Computing Technical Report CS-11-04, University of Surrey 2011

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

2010

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

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

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

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

2009

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

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

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

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

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

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

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

2008

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

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

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

2007

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

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

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

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

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

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

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

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

2006

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

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

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

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

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

2005

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

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

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

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

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

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

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

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

2004

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

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

2003

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

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

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

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

pre 2003

Steve Schneider, Verifying authentication protocol implementations, FMOODS 2002.

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

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

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

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

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

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

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

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

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

Steve Schneider: Verifying authentication protocols with CSP. CSFW 1997

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

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

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

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

Steve Schneider, Timewise refinement for communicating processes, MFPS 1993
 

Teaching

I am teaching two courses in 2012-13:

  • COM3009: Computer Security (Autumn Semester)
  • COM1029: Data Structures and Algorithms (Spring Semester)

 

Departmental Duties

My main administrative duty for 2012-13 is: Research Excellence Framework (REF2014) UoA Lead for Computing

Page Owner: css1ss
Page Created: Tuesday 2 December 2008 10:10:56 by mf0009
Last Modified: Wednesday 31 July 2013 16:11:29 by css1ss
Assembly date: Tue Oct 01 18:46:54 BST 2013
Content ID: 2143
Revision: 37
Community: 1028