
Professor Steve Schneider
Academic and research departments
Surrey Centre for Cyber Security, Department of Computer Science, Faculty of Engineering and Physical Sciences.About
Biography
I am Director of the Surrey Centre for Cyber Security, recognised by NCSC as one of the UK's Academic Centres of Excellence in Cyber Security Research. I joined the Department of Computer Science in September 2004 and was Head of Department 2004-2010. I was Associate Dean Research and Innovation in the Faculty of Engineering and Physical Sciences from 2015-2019.
I was previously in the Department of Computer Science at Royal Holloway, University of London over the period 1994-2004. I gained my doctorate from the University of Oxford, and held post-doctoral positions there prior to joining Royal Holloway.
Areas of specialism
University roles and responsibilities
- Director of the Surrey Centre for Cyber Security
Previous roles
Affiliations and memberships
News
In the media
ResearchResearch interests
I have been working in the area of Secure Electronic Voting since 2004. Since then I have been involved in the design and development of the Prêt à Voter verifiable voting system including its implementation for use in the vVote system used in the 2014 State Election in the State of Victoria, Australia. I am interested in more general approaches to secure electronic voting, and the use of Distributed Ledger Technologies in this domain, and more generally.
I am also researching in security and privacy in the transportation domain. In Rail, we are focusing on the challenges around customer data privacy in the context of increased use of customer information to support journeys. Other work in rail has focused on the application of formal modelling approaches to establishing safety requirements within rail networks.
In the Automotive domain we are focusing on security within vehicle-to-vehicle communications,
These interests are grounded in earlier work in formal methods and in security around modelling and verification of security protocols, and in non-interference. In particular this has focused on methods for analysis of protocols between agents interacting in an insecure environment, and proving that they provide critical authentication and confidentiality properties.
My formal methods work originated in concurrency theory, specifically the process algebra Communicating Sequential Processes (CSP), and its timed version Timed CSP. I also work with the B-Method and with Event-B, their relationship to CSP, and their application to safety and security verification.
Research projects
A collaboration between the University of Surrey and King's College London, together with industrial partners Monax Industries, Crowdcube Limited, and Electoral Reform Services.
The project aims to explore applications of distributed ledger technologies (DLT) in domains involving voting and collective decision making. There are many domains in which some form of balloting is required, such as voting on proposals or electing in charities, professional organisations, clubs, trades unions, political parties, and private companies. It is important to run such ballots in a way to ensure that the result is trusted. The project also focuses on management of more complex voting rights, for example in the context of company shareholdings, and the role that can be played by smart contracts.
Secure Electronic VotingI 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 led an international collaboration to provide secure electronic voting to the State of Victoria, Australia for their November 2014 State election. I was also an investigator on the 2009-2014 EPSRC grant `Trustworthy Voting Systems'.
Research collaborations
I work with Helen Treharne and collaborators in Swansea on developing new methods and tools for formally verifying safety for railway track plans. I am interested in scalability of the methods, enabling them to manage the complexity of real track plans.
I have a longstanding collaboration with Peter Ryan of the University of Luxembourg and Vanessa Teague of the University of Melbourne in the area of Secure Electronic Voting.
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.
Research interests
I have been working in the area of Secure Electronic Voting since 2004. Since then I have been involved in the design and development of the Prêt à Voter verifiable voting system including its implementation for use in the vVote system used in the 2014 State Election in the State of Victoria, Australia. I am interested in more general approaches to secure electronic voting, and the use of Distributed Ledger Technologies in this domain, and more generally.
I am also researching in security and privacy in the transportation domain. In Rail, we are focusing on the challenges around customer data privacy in the context of increased use of customer information to support journeys. Other work in rail has focused on the application of formal modelling approaches to establishing safety requirements within rail networks.
In the Automotive domain we are focusing on security within vehicle-to-vehicle communications,
These interests are grounded in earlier work in formal methods and in security around modelling and verification of security protocols, and in non-interference. In particular this has focused on methods for analysis of protocols between agents interacting in an insecure environment, and proving that they provide critical authentication and confidentiality properties.
My formal methods work originated in concurrency theory, specifically the process algebra Communicating Sequential Processes (CSP), and its timed version Timed CSP. I also work with the B-Method and with Event-B, their relationship to CSP, and their application to safety and security verification.
Research projects
A collaboration between the University of Surrey and King's College London, together with industrial partners Monax Industries, Crowdcube Limited, and Electoral Reform Services.
The project aims to explore applications of distributed ledger technologies (DLT) in domains involving voting and collective decision making. There are many domains in which some form of balloting is required, such as voting on proposals or electing in charities, professional organisations, clubs, trades unions, political parties, and private companies. It is important to run such ballots in a way to ensure that the result is trusted. The project also focuses on management of more complex voting rights, for example in the context of company shareholdings, and the role that can be played by smart contracts.
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 led an international collaboration to provide secure electronic voting to the State of Victoria, Australia for their November 2014 State election. I was also an investigator on the 2009-2014 EPSRC grant `Trustworthy Voting Systems'.
Research collaborations
I work with Helen Treharne and collaborators in Swansea on developing new methods and tools for formally verifying safety for railway track plans. I am interested in scalability of the methods, enabling them to manage the complexity of real track plans.
I have a longstanding collaboration with Peter Ryan of the University of Luxembourg and Vanessa Teague of the University of Melbourne in the area of Secure Electronic Voting.
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
I am currently teaching the module COM2031 Advanced Algorithms to our undergraduate level 5 students. In 2020 this was delivered in hybrid form.
I also supervise undergraduate and MSc projects.
In previous years i have taught
- Computer Security
- Algorithms and Data Structures
- Foundations of Computing
Publications
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