Prof Steve Schneider
Head of Department
Qualifications: BA MSc DPhil
Email: s.schneider@surrey.ac.uk
Phone: 01483 68 9637
Room no: 30 BB 02
Office hours
Mondays 15:00-17:00, or by appointment via Judy Lowe
Further information
Research Interests
I am interested in the theory of concurrency and its applications, and 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.
This has led to work 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.
I am also interested in security, and have previously worked on non-interference, and on the analysis and verification of security protocols. More recently I have been working on secure electronic voting. I contributed to the original proposal for the Prêt à Voter secure auditable electronic voting system, and have been involved in work on extensions. 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'.
Publications
Books
Schneider, S.A. (2001). The B-Method: an Introduction, Palgrave Cornerstones in Computer Science (series editors Richard Bird and Tony Hoare).
Ryan, P.Y.A & Schneider, S.A. & Goldsmith, M & Lowe, G. & Roscoe, A.W. (2000) Modelling and Analysis of Security Protocols, Addison Wesley.
Schneider, S.A. (1999). Concurrent and Real Time Systems: the CSP Approach, John Wiley.
Selected Papers
2009
Siraj Shaikh, Vicky Bush & Steve Schneider, Specifying authentication using signal events in CSP. Computers & Security 28(5), 2009
Steve Schneider & Helen Treharne, Changing system interfaces consistently: a new refinement strategy for CSP||B. IFM 2009, LNCS
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. (Technical report)
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
- COM1006: Foundations of Computing
- COM3004: Concurrent Systems
Departmental Duties
Head of Department
Member of Surrey International Institute Executive Group
Member of University Ethics Committee
