Integrating and Extending JCSP (2009)
Alistair A. Mcewan, Steve Schneider, Wilson Ifill, Peter Welch, Peter Welch A, Neil Brown A, ...
Abstract. This paper presents the extended and re-integrated JCSP library of CSP packages for Java. It integrates the differing advances made by Quickstone’s JCSP Network Edition and the “core...
Timed CSP: A Retrospective (2008)
Joël Ouaknine, Steve Schneider
We review the development of the process algebra Timed CSP, from its inception nearly twenty years ago to very recent semantical and algorithmic developments.
By relieving the brain of all unnecessary work, a good notation sets it free to concentrate on more advanced problems.
Steve Schneider, Helen Treharne
Abstract. Recent work on combining CSP and B has provided ways of describing systems comprised of components described in both B (to express requirements on state) and CSP (to express interactive and...
PyCSP- Communicating Sequential Processes for Python (2008)
Alistair A. Mcewan, Steve Schneider, Wilson Ifill, Peter Welch, Brian Vinter B, ...
Steve Schneider, Thai Son Hoang, Ken Robinson, Helen Treharne
Abstract. The introduction of probabilistic behaviour into the B-Method is a recent development. In addition to allowing probabilistic behaviour to be modelled, the relationship between expected...
JCSProB: Implementing Integrated Formal Specifications in Concurrent Java (2008)
Alistair A. Mcewan, Steve Schneider, Wilson Ifill, Peter Welch, Letu Yang, Michael R. Poppleton
Augmenting B with Control Annotations (2008)
Wilson Ifill, Steve Schneider, Helen Treharne
Abstract. CSP�B is an integration of the process algebra Communicating Sequential Processes (CSP), and the B-Method, which enables consistent controllers to be written for B machines in a...
A Layered Behavioural Model of Platelets (2008)
Steve Schneider, Helen Treharne
There is great interest in the application of nanotechnology to medicine, but concerns for safety are paramount. We present a modelling technique based on CSP and B as a starting point for simulation...
Augmenting B with Control Annotations (2008)
Wilson Ifill, Steve Schneider, Helen Treharne
Abstract. CSP�B is an integration of the process algebra Communicating Sequential Processes (CSP), and the B-Method, which enables consistent controllers to be written for B machines in a...
May Testing, Non-interference, and (2007)
This paper uses CSP to introduce a characterisation of non-interference in terms of the deductions that may be made about high level processes by low level tests. May testing yields classic...
Design and Verification of Distributed Recovery Blocks with CSP (2007)
W L Yeung, Steve Schneider, Francis Tam, Hants Rg Pd
A case study on the application of Communicating Sequential Processes (CSP) to the design and verification of fault-tolerant real-time systems is presented. The distributed recovery block (DRB)...
From Inaoe Itziar, Itziar Aretxaga, Esperanza Carrasco, Luis Carrasco, Elsa Recillas, Elena Terlevich, ...
MT point to a large population of mm-emitters that are likely at cosmological distances. 3. The excess in the sub-mm background radiation reported by Puget et al. may require high-redshift...
A failures semantics for ET-LOTOS (2007)
Steve Schneider, Royal Holloway, Jeremy Bryans, Jim Davies
A denotational semantics is presented for ET-LOTOS [LeL94] in the style of semantics for timed CSP, in terms of timed failures with additional information about internal events. This semantics is...
Towards the rank function verication of protocols that use temporary secrets (2007)
Abstract. The rank functions approach to protocol analysis is incomplete with respect to condentiality properties. In particular, protocols that use temporary secrets may be un-veriable within the...
Towards the rank function verication of protocols that use temporary secrets (2007)
Abstract. The rank functions approach to protocol analysis is incomplete with respect to condentiality properties. In particular, protocols that use temporary secrets may be un-veriable within the...
Classifying and Capturing Timing Requirements (2007)
Helen Treharne, Steve Schneider
Abstract. This paper classifies the timing requirements that arise in embedded avionics systems. A typical avionics system motivates the work. Its timed specification is presented, from which we...
Alan Jeffrey, Alan Jeffrey, Steve Schneider, Steve Schneider, Frits Vaandrager, Frits Vaandrager
A comparison of additivity axioms
Towards the Verification of Security (2007)
Protocols That Use, Rob Delicata, Steve Schneider
The rank functions approach to protocol analysis is incomplete with respect to secrecy specifications. In particular, security protocols that use temporary secrets may be un-verifiable within the...
A Formal Approach for Reasoning About a Class of Diffie-Hellman Protocols (2006)
Delicata, Robert, Schneider, Steve
We present a framework for reasoning about secrecy in a class of Diffie-Hellman protocols. The technique, which shares a conceptual origin with the idea of a rank function, uses the notion of a...
Microstrip Leaky Wave Antenna Performance on a Curved Surface (Preprint) (2006)
Radcliffe, Joshua, Thiele, Gary, Penno, Robert, Schneider, Steve, Kempel, Leo
Microstrip antennas are popular due to their ease of construction and minimal dimensions; especially in terms of thickness. These antennas typically are resonant structures and hence having a...
Driving Point Impedance for a Linear Array of Half-Width Leaky-Wave Antenna (Preprint) (2006)
Corwin, Michael, Kempel, Leo, Schneider, Steve
Printed leaky-wave antennas offer the potential for a low-profile, wide-bandwidth antenna element that can be arrayed if desired. Microstrip leaky-wave antennas rely on the suppression of the...
Electronic voting has attracted much interest recently and a variety of schemes have been proposed. Generally speaking, all these schemes can be divided into three main approaches: based on blind...
Electronic voting has attracted much interest recently and a variety of schemes have been proposed. Generally speaking, all these schemes can be divided into three main approaches: based on blind...
A Practical, Voter-Verifiable Election Scheme (2005)
Chaum, David, Ryan, Peter Y. A., Schneider, Steve
We present an election scheme designed to allow voters to verify that their vote is accurately included in the count. The scheme provides a high degree of transparency whilst ensuring the secrecy of...
Tank monitoring: a pAMN case study (2005)
Schneider, Steve, Hoang, Thai Son, Robinson, Ken, Treharne, Helen
The introduction of probabilistic behaviour into the B-Method is a recent development. In addition to allowing probabilistic behaviour to be modelled, the relationship between expected values of the...
Formal verification of fault-tolerant software design: the CSP approach (2005)
Yeung, W. L., Schneider, Steve
Software design techniques for tolerating both hardware and software faults have been developed over the past few decades. Paradoxically, it is essential that fault-tolerant software is designed with...
Verifying Security Protocols: An Application of CSP (2005)
Schneider, Steve, Delicata, Robert
The field of protocol analysis is one area in which CSP has proven particularly successful, and several techniques have been proposed that use CSP to reason about security properties such as...
A decision procedure for the existence of a rank function (2005)
Heather, James, Schneider, Steve
Schneider's work on rank functions [IEEE TSE 24(9) (1998)] provides a formal approach to verification of certain properties of a security protocol. However, he illustrates the approach only with a...
A formal approach for reasoning about a class of diffie-hellman protocols (2005)
Abstract. We present a framework for reasoning about secrecy in a class of Diffie-Hellman protocols. The technique, which shares a conceptual origin with the idea of a rank function, uses the notion...
The internet and communication studies (2004)
Jankowski, Nicolas, Jones, Steve, Foot, Kirsten, Howard, Phil, Mansell, Robin, Schneider, Steve, ...
This book explores the impact of the Internet on scholarly research across and beyond the social sciences. The contributors - leading figures in a broad spectrum of disciplines - explain how their...
The internet and communication studies (2004)
Jankowski, Nicolas, Jones, Steve, Foot, Kirsten, Howard, Phil, Mansell, Robin, Schneider, Steve, ...
This book explores the impact of the Internet on scholarly research across and beyond the social sciences. The contributors - leading figures in a broad spectrum of disciplines - explain how their...
Verifying Controlled Components (2004)
Steve Schneider And, Steve Schneider, Helen Treharne
Recent work on combining CSP and B has provided ways of describing systems comprised of components described in both B (to express requirements on state) and CSP (to express interactive and...
Newcastle upon Tyne, NE1 7RU, UK. A Practical, Voter-Verifiable Election Scheme (2004)
David Chaum, Steve A. Schneider, David Chaum, Steve Schneider
Abstract. We present an election scheme designed to allow voters to verify that their vote is accurately included in the tabulation. The scheme provides a high degree of transparency whilst ensuring...
Verifying Controlled Components (2004)
Steve Schneider And, Steve Schneider, Helen Treharne
Recent work on combining CSP and B has provided ways of describing systems comprised of components described in both B (to express requirements on state) and CSP (to express interactive and...
A formal model of Diffie-Hellman using CSP and rank functions (2003)
Formal analysis techniques have proved successful in finding flaws in security protocols. Such techniques typically assume the presence of perfect encryption, an assumption that is clearly not true...
CSP Theorems for Communicating B Machines (2003)
Steve Schneider, Helen Treharne, Surrey Tw Ex
Recent work on combining CSP and B has provided ways of describing systems comprised of components described in both B (to express requirements on state) and CSP (to express interactive and...
Composing Specifications Using Communication (2003)
Helen Treharne, Steve Schneider, Marchia Bramble
This paper develops a case study using the process algebra CSP to enable controlled interaction between B machines. This illustrates how B machines are essential components within a combined...
Heather, James, Schneider, Steve
Many methods of analysing security protocols have been proposed, but most such methods rely on analysing a protocol running only a finite network. Some, however - notably, data independence, the...
James Heather, Steve Schneider
Abstract. Many methods of analysing security protocols have been proposed, but most such methods rely on analysing a protocol running only a finite network. Some, however—notably, data...
Communicating B machines (2002)
Steve Schneider, Helen Treharne
Abstract. This paper describes a way of using the process algebra CSP to enable controlled interaction between concurrent B machines. This approach supports compositional verification: each of the...
CSP theorems for communicating B machines (2002)
Steve Schneider, Helen Treharne, Surrey Tw Ex
Abstract. Recent work on combining CSP and B has provided ways of describing systems comprised of components described in both B (to express requirements on state) and CSP (to express interactive and...
Verifying Authentication Protocol Implementations (2002)
Formal methods for verifying authentication protocols tend to assume an idealised, perfect form of encryption. This approach has been spectacularly successful in finding flaws, but when we aim for...
Analysing Time Dependent Security Properties in CSP Using PVS (2000)
This paper details an approach to verifying time dependent authentication properties of security protocols. We discuss the introduction of time into the Communicating Sequential Processes (CSP)...
How to prevent type flaw attacks on security protocols (2000)
James Heather, Gavin Lowet, Steve Schneider
A type flaw attack on a security protocol is an attack where afield that was originally intended to have one type is subsequently interpreted as having another type. A number of type fiaw attacks...
How to drive a B machine (2000)
Helen Treharne, Steve Schneider
Abstract. The B-Method is a state-based formal method that describes behaviour in terms of MACHINES whose states change under OPERATIONS. The process algebra CSP is an event-based formalism that...
Analysing Time Dependent Security Properties in CSP using PVS (2000)
This paper details an approach to verifying time dependent authentication properties of security protocols. We discuss the introduction of time into the Communicating Sequential Processes (CSP)...
Towards Automatic Verification of Authentication Protocols on an Unbounded Network (2000)
James Heather, Steve Schneider
Schneider's work on rank functions [14] provides a formal approach to verification of certain properties of a security protocol. However, he illustrates the approach only with a protocol running...
Capturing timing requirements formally in AMN (1999)
Helen Treharne, Steve Schneider
This paper classifies the timing requirements that arise in embedded avionics systems. A typical avionics system motivates the work. Its timed specification is presented, from which we extract...
Abstraction and Testing (1999)
ion and testing Steve Schneider Department of Computer Science Royal Holloway, University of London Egham, Surrey, TW20 0EX, UK Abstract Restricted views of process behaviour result in a form of...
Using a Process Algebra to control B OPERATIONS (1999)
Helen Treharne, Steve Schneider
The B-Method is a state-based formal method that describes system behaviour in terms of MACHINES whose state changes under OPERATIONS. The process algebra CSP is an event-based formalism that enables...
Using a Process Algebra to control B OPERATIONS (1999)
Helen Treharne, Steve Schneider
The B-Method is a state-based formal method that describes system behaviour in terms of MACHINES whose state changes under OPERATIONS. The process algebra CSP is an event-based formalism that enables...
FE-BI Analysis of a Leaky-Wave Antenna with Resistive Sheet Termination (1998)
Kempel, Leo, Schneider, Steve, Radcliff, Joshua, Janning, Dan, Thiele, Gary
Printed leaky-wave antennas offer the potential for a low-profile. wide-bandwidth antenna element that can be arrayed if desired. Microstrip leaky-wave antennas rely on the suppression of the...
Formal Analysis of a Non-Repudiation Protocol (1998)
This paper applies the theory of Communicating Sequential Processes (CSP) to the modelling and analysis of a non-repudiation protocol. Non-repudiation protocols differ from authentication and...
Timewise Refinement for Communicating Processes (1997)
A theory of timewise refinement is presented. This allows the translation of specifications and proofs of correctness between semantic models, permitting each stage in the verification of a system to...
CSP, PVS and a Recursive Authentication Protocol (1997)
Jeremy Bryans, Steve Schneider
this paper we consider the nature of machine proofs used in the CSP approach to the verification of authentication protocols. In [Sch96], a general method is presented for the analysis and...
Using a PVS Embedding of CSP to Verify Authentication Protocols (1997)
To Be, Bruno Dutertre, Steve Schneider
. This paper presents an application of PVS to the verification of security protocols. The objective is to provide mechanical support for a verification method described in [14]. The PVS...
Embedding CSP in PVS. An Application to Authentication Protocols (1997)
Bruno Dutertre, Steve Schneider
In [28], Schneider applies CSP to the modelling and analysis of authentication protocols and develops a general proof strategy for verifying authentication properties. This paper shows how the PVS...
Using a PVS Embedding of CSP to Verify Authentication Protocols (1997)
Bruno Dutertre, Steve Schneider
. This paper presents an application of PVS to the verification of security protocols. The objective is to provide mechanical support for a verification method described in [14]. The PVS...
Modelling security properties with CSP (1996)
Steve Schneider, Royal Holloway
Security properties such as confidentiality and authenticity may be considered in terms of the flow of messages within a network. To the extent that this characterisation is justified, the use of a...
Using CSP for protocol analysis: the Needham-Schroeder Public-Key Protocol (1996)
Steve Schneider, Royal Holloway
This paper presents a general approach for analysis and verification of authentication properties in CSP. It is illustrated by an examination of the Needham-Schroeder Public-Key protocol. The paper...
Steve Schneider, Abraham Sidiropoulos
. Security protocols are designed to meet particular security properties. In order to analyse such protocols formally, it is necessary to provide a formal definition of the property that they are...
Security properties and CSP (1995)
Steve Schneider, Royal Holloway
Security properties such as confidentiality and authenticity may be considered in terms of the flow of messages within a network. To the extent that this characterisation is justified, the use of a...
Towards a denotational semantics for ET-LOTOS (1995)
Jeremy Bryans, Jim Davies, Steve Schneider
The formal specification language LOTOS is an international standard for use in Open Systems Interconnection. A timed extension called ET-LOTOS has been proposed. This paper presents a fully-abstract...
Real-time CSP and ET-LOTOS (1995)
Jeremy Bryans, Jim Davies, Steve Schneider
This paper is intended to support and stimulate discussion at the COST 247 meeting in Brighton, 19th and 20th July 1994. It begins with a comprehensive introduction to the language of real-time CSP....
An Operational Semantics for Timed CSP (1995)
An operational semantics is defined for the language of timed CSP, in terms of two relations: an evolution relation, which describes when a process becomes another simply by allowing time to pass;...
Real-time LOTOS and timed observations (1995)
Jim Davies, Jeremy Bryans, Steve Schneider
This paper presents a new semantic model for real-time LOTOS, based upon a notion of timed observations. The novelty of the model is explained, as is its value. It di#ers from the usual operational...
A Comparison of Additivity Axioms in Timed Transition Systems (1993)
Frits Va, Alan Jeffrey, Alan Jeffrey, Steve Schneider, Steve Schneider, Frits Vaandrager
This paper discusses some axioms from the literature which have been used to define properties of timed transition systems. The additivity axiom proposed by (amongst others) Wang, and Nicollin and...
Alan Jeffrey, Steve Schneider, Frits Vaandrager
COMPUTER SCIENCE A comparison of additivity axioms in timed transition systems
Correctness and communication in real-time systems /--Steven A. Schneider. (1989)
Thesis (D.Phil.) -- University of Oxford, 1989.
Verifying authentication protocols with CSP
This paper presents a general approach for analysis and verification of authentication properties in the language of Communicating Sequential Processes (CSP). It is illustrated by an examination of...